1COQ(1) General Commands Manual COQ(1)
2
3
4
6 coqdep - Compute inter-module dependencies for Coq programs
7
8
10 coqdep [ -I directory ] [ -coqlib directory ] [ -i ] [ -slash ] file‐
11 name ... directory ...
12
13
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
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
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
73 ocamlc(1), coqc(1), make(1).
74
75
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
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
115 Please report any bug to https://github.com/coq/coq/issues
116
117
118
119 COQ(1)