coqdep(1)

1COQ(1)                      General Commands Manual                     COQ(1)
2
3
4

NAME

6       coqdep - Compute inter-module dependencies for Coq programs
7
8

SYNOPSIS

10       coqdep  [  -I directory ] [ -coqlib directory ] [ -i ] [ -slash ] file‐
11       name ...  directory ...
12
13

DESCRIPTION

15       coqdep computes inter-module dependencies for Coq programs, and  prints
16       the  dependencies  on the standard output in a format readable by make.
17       When a directory is given as argument, it is recursively looked at.
18
19       Dependencies of Coq modules are computed by looking at Require commands
20       (Require, Require Export, Require Import, possibly restricted by a From
21       clause), Declare ML Module commands, Add  LoadPath  commands  and  Load
22       commands. Dependencies relative to modules from the Coq library are not
23       printed except if -boot is given.
24
25

OPTIONS

27       -f file
28              Read filenames and options -I, -R  and  -Q  from  a  _CoqProject
29              FILE.
30
31       -I/-Q/-R options
32              Have  the  same  effects  on  load path and modules names as for
33              other Coq commands (coqtop, coqc).
34
35       -coqlib directory
36              Indicates where is the Coq library. The default value  has  been
37              determined  at  installation  time,  and  therefore  this option
38              should not be used under normal circumstances.
39
40       -exclude-dir dir
41              Skips subdirectory dir during -R/-Q search.
42
43       -sort  Output the given file name ordered by dependencies.
44
45       -vos   Output dependencies for .vos files (this is not the  default  as
46              it breaks dune's Coq mode)
47
48       -boot  For  coq  developers, prints dependencies over coq library files
49              (omitted by default).
50
51       -noinit
52              Currently no effect.
53
54       -vos   Includes dependencies about .vos files.
55
56       -dyndep (opt|byte|both|no|var)
57              Set how dependencies over ML modules are printed.  -m  META  Re‐
58              solve plugin names using the META file.
59
60

EXIT STATUS

62       1      A  file  given on the command line cannot be found, or some file
63              cannot be opened, or there is a syntax error in one of the  com‐
64              mands recognized by coqdep.
65
66       0      In  all  other cases. In particular, when a dependency cannot be
67              found or an invalid option is encountered, coqdep prints a warn‐
68              ing and exits with status 0.
69
70
71

NOTES

77       Lexers  (for  Coq  and  OCaml)  correctly  handle  nested  comments and
78       strings.
79
80       The treatment of symbolic links is primitive.
81
82       If two files have the same name, in two different directories, a  warn‐
83       ing is printed on standard error.
84
85       There is no way to limit the scope of the recursive search for directo‐
86       ries.
87
88

EXAMPLES

90       Consider the files (in the same directory):
91
92            a.mllib X.v Y.v and Z.v
93
94       where
95
96       +      a.mllib contains the module names `B' and `C';
97
98       +      Y.v contains the command `Require Foo.X' ;
99
100       +      Z.v contains the commands `From Foo Require X' and  `Declare  ML
101              Module "a"'.
102
103       To get the dependencies of the Coq files:
104
105              example% coqdep -I . -Q . Foo *.v
106              X.vo X.glob X.v.beautified X.required_vo: X.v
107              X.vio: X.v
108              Y.vo Y.glob Y.v.beautified Y.required_vo: Y.v X.vo
109              Y.vio: Y.v X.vio
110              Z.vo Z.glob Z.v.beautified Z.required_vo: Z.v X.vo ./a.cma ./a.cmxs
111              Z.vio: Z.v X.vio ./a.cma ./a.cmxs
112
113

BUGS

115       Please report any bug to https://github.com/coq/coq/issues
116
117
118
119                                                                        COQ(1)