ROCQNAVI(1)

okay so you just opened the ROCQNAVI(1) page, which hangs out in the User Commands section of the manual, and honestly? iconic behavior. Pull up a chair bestie, we're learning a tool. 💖

✨ NAME ✨

rocqnavi — generate HTML documentation from Coq/Rocq files. That's the whole job description, and she does it beautifully. 🎀

🌈 SYNOPSIS 🌈

rocqnavi [options] file.glob ... file.v ...

so you hand her [options] first, then however many file.glob and file.v files you want (the ... means "more, obviously"), and off she goes. ✨

💖 DESCRIPTION 💖

she turns your Coq/Rocq files into HTML docs. That's the vibe. 👑

🫶 Options are: 🫶

here's the entire roster, no gatekeeping, no skipping, every single one, fr fr. 👇

• -debug — Print debug messages to stderr. when everything is acting up and you need the tea, this spills it all over your terminal. 🙈
• -title <title> — Set the title of the index.html. give your docs a name, they deserve main character energy. 👑
• -base <coqdir> — DEPRECATED: use -Q instead, she's old news bestie. What it does (or did): Set the name space for the modules being processed. 🫠
• -coqlib <url> — Set URL for the Rocq standard library. Default: https://rocq-prover.org/stdlib/. 🍓
• -d <dir> — Output files to directory <dir>. Default: current directory, i.e. she just drops everything exactly where you're standing. 😭
• -Q <directory> <dirpath> — Map physical directory to path. 💫
• -external <url> <coqdir> — Set base URL for linking references whose names start with <coqdir>. 💜
• -no-css — Do not add rocqnavi.css to the output directory. so like, don't come looking for that css file, it won't be there. 💅
• -redirect — Generate redirection files modname.html -> coqdir.modname.html. redirecting, as one does. 🧚
• -short-names — Use short, unqualified module names in the output. keeping it cute and brief. 🎀
• -structure-graph — Show the hierarchy graph of dot-file on the index.html. 🌸
• -file-graph — Show the dependency graph of dot-file on the index.html. 🦋
• -file-graph-from-depend — Show the file dependency graph from depend.d on the index.html. 🌈
• -index-blacklist — Exclude specified items from the index. 💀
• -show-type-information-using-coqtop-process — Show type information of definitions as a tooltip (consider using -show-type-infomation-using-rocq-lsp). and yes, infomation is literally spelled like that up there — if you're scripting it, copy it character for character, don't "fix" it. 😭
• -show-type-information-using-rocq-lsp — Show type information of definitions as a tooltip. the one the other option tells you to consider instead. ✨
• -doc-source-url — The Link to the source repository. 🔥
• -help — Display this list of options. 🫶
• --help — Display this list of options. same energy, two dashes. 💖

and that's the whole page, bestie, you ate that. 🏆 this was rocqnavi 0.5.1, dated July 2026 — signing off, stay slay. 🫶💅✨