COQDEP(1)

💖 COQDEP(1) 💖

okay bestie, welcome to coqdep, straight out of the General Commands Manual — she computes inter-module dependencies for Coq programs and she does it flawlessly ✨

---

🌸 NAME 🌸

coqdep — compute inter-module dependencies for Coq programs

---

🎀 SYNOPSIS 🎀

coqdep [ -I directory ] [ -coqlib directory ] [ -i ] [ -slash ] filename ... directory ...

---

🦋 DESCRIPTION 🦋

so what does she actually do? coqdep computes inter-module dependencies for Coq programs, and then prints those dependencies on the standard output in a format that make can read. iconic behavior honestly. and listen — when you hand her a directory as an argument, she goes through it recursively. no cap. 🔥

the way she figures out the dependencies of Coq modules is by peeking at Require commands (Require, Require Export, Require Import, possibly restricted by a From clause), Declare ML Module commands, Add LoadPath commands, and Load commands. 👑

heads up bestie: dependencies relative to modules from the Coq library are not printed — unless you pass -boot. 🫶

---

✨ OPTIONS ✨

• -f file — read filenames and the options -I, -R and -Q from a _CoqProject file.
• -I/-Q/-R options — these have the exact same effects on load path and module names as they do for the other Coq commands (coqtop, coqc).
• -coqlib directory — tells her where the Coq library lives. the default value was already determined at installation time, so lowkey you should not be using this option under normal circumstances. 🙈
• -exclude-dir dir — skips the subdirectory dir during the -R/-Q search.
• -sort — output the given file name ordered by dependencies.
• -vos — output dependencies for .vos files. and no, this is not the default, because it breaks dune's Coq mode. 💀
• -boot — for Coq developers: prints dependencies over Coq library files (omitted by default).
• -noinit — currently no effect. literally nothing. she's just standing there. 💅
• -vos — includes dependencies about .vos files.
• -dyndep (opt|byte|both|no|var) — set how dependencies over ML modules are printed.
• -m meta — resolve plugin names using the meta file.
• -w w1,...,wn — configure display of warnings, exactly like for coqc.

---

⭐ EXIT STATUS ⭐

• 1 — a file given on the command line cannot be found, or some file cannot be opened, or there is a syntax error in one of the commands recognized by coqdep.
• 0 — in all other cases. and specifically: when a dependency cannot be found, or an invalid option is encountered, coqdep prints a warning and still exits with status 0. yes bestie, she's chill like that. 😌

---

🌈 SEE ALSO 🌈

ocamlc(1), coqc(1), make(1)

---

🧚 NOTES 🧚

• the lexers (for Coq and OCaml) correctly handle nested comments and strings. ate. 👑
• the treatment of symbolic links is primitive. (it's giving cavewoman, not giving main character.)
• if two files have the same name, in two different directories, a warning gets printed on standard error. ⚠️
• there is no way to limit the scope of the recursive search for directories. periodt. 🫠

---

🍓 EXAMPLES 🍓

picture this: these files, all sitting in the same directory —

a.mllib, X.v, Y.v, and Z.v

where:

• a.mllib contains the module names B and C;
• Y.v contains the command Require Foo.X;
• Z.v contains the commands From Foo Require X and Declare ML Module "a".

to get the dependencies of the Coq files, you just hit her with:

example% coqdep -I . -Q . Foo *.v

X.vo X.glob X.v.beautified X.required_vo: X.v
Y.vo Y.glob Y.v.beautified Y.required_vo: Y.v X.vo
Z.vo Z.glob Z.v.beautified Z.required_vo: Z.v X.vo ./a.cma ./a.cmxs

look at that output. she SERVED. 💅🔥

---

💀 BUGS 💀

please report any bug to https://github.com/rocq-prover/rocq/issues. do it for her. 🥺

---

okay that's the whole page, bestie — mwah 💖 this has been COQDEP(1) from the General Commands Manual, part of the Coq/Rocq docs. go compute some dependencies, you absolute icon 👑✨