ROCQCHK(1)

🦋 ROCQCHK — verify compiled Rocq libraries 💖

ok so bestie, welcome to rocqchk, a page straight out of the General Commands Manual (section 1, iykyk). she's the standalone vibe-checker for your compiled Rocq libraries, and she does not play around. let's get into it ✨

✨ NAME ✨

rocqchk — verify compiled Rocq libraries 🎀

🌸 SYNOPSIS 🌸

rocqchk [ options ] modules

💜 DESCRIPTION 💜

ok so rocqchk is literally the standalone checker of compiled libraries — we're talking .vo files, the ones produced by rocqcompile — for the Rocq Prover. 🦋 want more lore? the Reference Manual has you covered.

here's the deal with exit codes, and bestie, this part matters:

• if all the requested tasks succeeded, she returns with exit code 0. slay. ✨
• a non-zero return code means something went wrong: some library was not found, corrupted content, type-checking failure, etc. 💀 not the vibe.

and modules? that's a list of modules to be checked. you can refer to modules by a short or qualified logical name, or by their filename. flexible queen. 💅

🎀 OPTIONS 🎀

• -I dir, --include dir — add directory dir to the include path. 📁
• -Q dir rocqdir — map physical dir to logical rocqdir. 🗺️
• -R dir rocqdir — synonymous to -Q. (yes, literally the same thing, she's just got two names 💅)
• -silent — be less verbose. shhh. 🤫
• -admit module — tag the specified module and all its dependencies as trusted, and they will not be rechecked, unless explicitly requested by other options. 👑
• -norec module — specifies that the given module shall be verified without requesting to check its dependencies. 🦋
• -m, --memory — displays a summary of the memory used by the checker. 🧠
• -o, --output-context — displays a summary of the logical content that have been verified: assumptions and usage of impredicativity. 🔍
• -impredicative-set — allows the checker to accept libraries that have been compiled with this flag. ✨
• -v — print rocqchk version and exit. 📢
• -coqlib dir — overrides the default location of the standard library. 📚
• -where — print rocqchk standard library location and exit. 📍
• -h, --help — print list of options. 🫶

🌈 SEE ALSO 🌈

• rocq(1),
• The Rocq Reference Manual.
• The Rocq web site: http://coq.inria.fr 🌐

friendly reminder bestie: -Q and -R are the same option. don't let anyone tell you otherwise. 💅

mwah 💋 that's the whole page. this one comes to you from the General Commands Manual, page ROCQCHK(1), and it's dated like the little classic it is — go forth and verify, you absolute icon, and remember: exit code 0 or we riot. 🎀✨💖