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.
58
59

EXIT STATUS

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

SEE ALSO

72       ocamlc(1), coqc(1), make(1).
73
74

NOTES

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

EXAMPLES

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

BUGS

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