COQCHK(1)

💖 COQCHK(1) — bestie edition 💖

General Commands Manual · the one where we vibe-check your compiled Coq libraries

---

✨ NAME ✨

coqchk — verify compiled Coq libraries 🫶

---

🌸 SYNOPSIS 🌸

coqchk [ options ] modules

---

🦋 DESCRIPTION 🦋

okay so. coqchk is the standalone checker of compiled libraries — and by "compiled libraries" we mean the .vo files that coqc produces — for the Coq Proof Assistant. no cap, that's literally its whole job. 🎀

if you want the deep lore, go read the Reference Manual. ✨

here's the vibe check on exit codes, and this part is IMPORTANT so pay attention bestie:

• it returns with exit code 0 if all the requested tasks succeeded 🎉
• a non-zero return code means something went wrong 😭 — like some library was not found, corrupted content, a type-checking failure, etc.

not me being dramatic but a non-zero exit is genuinely the "we need to talk" text of the Unix world 💀

modules is a list of modules to be checked. you can refer to a module by a short or qualified logical name, or by its filename. either way, she'll find it. 👑

---

💅 OPTIONS 💅

• -I dir, --include dir — adds directory dir to the include path. slay, now she can see it.
• -Q dir coqdir — maps physical dir to logical coqdir. it's giving "rename but make it logical".
• -R dir coqdir — synonymous to -Q. yeah, literally the same thing. twins. 👯
• -silent — be less verbose. she's quiet, she's mysterious, she's still checking. 🤫
• -admit module — tags the specified module and all its dependencies as trusted, and they will not be rechecked — unless they're explicitly requested by other options. (yes, that's a lot of trust to hand out, bestie, use it wisely 🙈)
• -norec module — specifies that the given module shall be verified without requesting to check its dependencies. just the one module, main character energy only. ⭐
• -m, --memory — displays a summary of the memory used by the checker. the receipts, basically. 🧾
• -o, --output-context — displays a summary of the logical content that has been verified: assumptions and usage of impredicativity. the whole lore dump. 📜
• -impredicative-set — allows the checker to accept libraries that have been compiled with this flag. no flag-shaming here, she'll take them as they come. 🫶
• -v — print coqchk version and exit. quick little hello and then she's gone. 👋
• -coqlib dir — overrides the default location of the standard library. moving day! 📦
• -where — print coqchk standard library location and exit. "where do you live?" "here." ✨
• -h, --help — print list of options. the classic. the icon. the one everybody runs first. 💖

---

🌈 SEE ALSO 🌈

• coqtop(1)
• coqc(1)
• coq_makefile(1)
• coqdep(1)
• The Rocq Prover Reference Manual.
• The Rocq Prover website: https://rocq-prover.org

---

and that's the whole page, bestie!! 🎀 COQCHK(1), straight from the General Commands Manual, verified, type-checked, and absolutely slaying. go forth and check your .vo files, i believe in you 💖✨🦋