---
name: "coqdep"
section: "1"
platform: "linux"
package: "rocq"
version: "9.3.0-1"
release: "Arch Linux 2026-11-01"
platforms: ["linux"]
url: "https://new.carta.tech/coqdep"
---

# coqdep(1)

compute inter-module dependencies for Coq programs

## NAME

coqdep - compute inter-module dependencies for Coq programs

## SYNOPSIS

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

## DESCRIPTION

**coqdep** computes inter-module dependencies for Coq programs, and prints the dependencies on the standard output in a format readable by **make**. When a directory is given as argument, it is recursively looked at.

Dependencies of Coq modules are computed by looking at *Require* commands (Require, Require Export, Require Import, possibly restricted by a From clause), *Declare* *ML* *Module* commands, *Add* *LoadPath* commands and *Load* commands. Dependencies relative to modules from the Coq library are not printed except if **-boot** is given.

## OPTIONS

- **-f** *file*

  Read filenames and options **-I**, **-R** and **-Q** from a \_CoqProject *file.*

- **-I/-Q/-R** *options*

  Have the same effects on load path and modules names as for other Coq commands (**coqtop**, **coqc**).

- **-coqlib** *directory*

  Indicates where is the Coq library. The default value has been determined at installation time, and therefore this option should not be used under normal circumstances.

- **-exclude-dir** *dir*

  Skips subdirectory *dir* during **-R**/**-Q** search.

- **-sort**

  Output the given file name ordered by dependencies.

- **-vos**

  Output dependencies for .vos files (this is not the default as it breaks dune's Coq mode).

- **-boot**

  For Coq developers, prints dependencies over Coq library files (omitted by default).

- **-noinit**

  Currently no effect.

- **-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 as 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. In particular, when a dependency cannot be found or an invalid option is encountered, **coqdep** prints a warning and exits with status 0.

## SEE ALSO

[**ocamlc**(1)](/ocamlc/1.md), [**coqc**(1)](/coqc/1.md), [**make**(1)](/make/1.md)

## NOTES

Lexers (for Coq and OCaml) correctly handle nested comments and strings.

The treatment of symbolic links is primitive.

If two files have the same name, in two different directories, a warning is printed on standard error.

There is no way to limit the scope of the recursive search for directories.

## EXAMPLES

Consider the files (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:

```
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
```

## BUGS

Please report any bug to **https://github.com/rocq-prover/rocq/issues**.