ROCQIDE(1)

📦 version 9.3.0, in alpine 3.24, arch rolling, fedora 44, nixpkgs unstable, ubuntu stonking

💖 ROCQIDE(1) — the Rocq IDE glow-up 💖

okay so bestie, welcome to the General Commands Manual page for rocqide, and I'm literally so excited to walk you through it 🫶 this is the whole thing, every flag, every path, no gatekeeping, no cap.

✨ NAME ✨

rocqide — graphical interface for the Rocq Prover 🌈

🎀 SYNOPSIS 🎀

rocqide [ options ]

that's it. that's the whole vibe. you give it options, it gives you a GUI 💅

🦋 DESCRIPTION 🦋

rocqide is a gtk graphical interface for the Rocq Prover. she's pretty, she's clickable, she's got windows ✨

if you're more of a command-line girlie, or you're doing batch-oriented use of Rocq, you want rocq(1) instead — that's the terminal one, iykyk.

👑 OPTIONS 👑

every single one, fr fr, nothing skipped, we don't do that here 💜

  • -h — show the complete list of options accepted by rocqide. the classic "wait what else can u do" move 🙈
  • -I dir, -include dir — add directory dir in the include path. let her know where the good stuff lives 💖
  • -R dir rocqdir — recursively map physical dir to logical rocqdir. it's giving "this folder is now this name, recursively, periodt" 🔥
  • -src — add source directories in the include path.
  • -nois — start with an empty state. blank slate, fresh start, main character energy ✨
  • -load-ml-object f — load ML object file f.
  • -load-ml-source f — load ML file f.
  • -l f, -load-vernac-source f — load Rocq file f.v (Load f.). yes, the .v gets added, don't come for me 🎀
  • -lv f, -load-vernac-source-verbose f — load Rocq file f.v (Load Verbose f.). same but louder, she's talking in all caps 💅
  • -load-vernac-object path — load Rocq library path (Require path.).
  • -require-import path — load Rocq library path and import it (Require Import path.). load AND import, she's committed 💖
  • -compile f — compile Rocq file f.v (implies -batch). lowkey this one drags -batch along with it whether you asked or not 😭
  • -compile-verbose f — verbosely compile Rocq file f.v (implies -batch). same deal, -batch is coming too, no discussion.
  • -where — print Rocq's standard library location and exit. quick lil peek, then she's gone 🦋
  • -v — print Rocq version and exit. "who am i? version number. bye." ✨
  • -q — skip loading of rcfile. not loading the rcfile today, bestie, we're going rogue 🙈
  • -init-file f — set the rcfile to f. if you're not skipping it, you're picking it 👑
  • -emacs — tells Rocq it is executed under Emacs. she's an Emacs girl now, she needs to know 🌸
  • -dump-glob f — dump globalizations in file f (to be used by rocq(1)doc). note that rocq(1)doc — that's literally how it's written, character for character, don't @ me 💀
  • -impredicative-set — set sort Set impredicative.
  • -dont-load-proofs — don't load opaque proofs in memory. she's on a memory diet, the proofs stay home 🎀

🌈 SEE ALSO 🌈

💜 AUTHOR 💜

This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>, for the Debian project (but may be used by others). shoutout to Samuel, absolute icon, we love a contributor 🫶

and that's the page, bestie!! 🎀 this is the ROCQIDE(1) page from the General Commands Manual section, and it signs off with ROCQIDE(1) at the bottom too — so if you ever forget where you are, she'll remind you twice 💖✨ slay, go load some vernac files, mwah 😭💅

📦 where this page comes from