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

NAME

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

SYNOPSIS

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

DESCRIPTION

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

OPTIONS

30       -f file
31              Read  filenames  and  options  -I,  -R and -Q from a _CoqProject
32              FILE.
33
34       -I/-Q/-R options
35              Have the same effects on load path  and  modules  names  as  for
36              other coq commands (coqtop, coqc).
37
38       -coqlib directory
39              Indicates  where  is the Coq library. The default value has been
40              determined at  installation  time,  and  therefore  this  option
41              should not be used under normal circumstances.
42
43       -exclude-dir dir
44              Skips subdirectory dir during -R/-Q search.
45
46       -sort  Output the given file name ordered by dependencies.
47
48       -vos   Output  dependencies  for .vos files (this is not the default as
49              it breaks dune's Coq mode)
50
51       -boot  For coq developers, prints dependencies over coq  library  files
52              (omitted by default).
53
54
55

SEE ALSO

57       ocamlc(1), coqc(1), make(1).
58
59

NOTES

61       Lexers (for Coq and Caml) correctly handle nested comments and strings.
62
63       The treatment of symbolic links is primitive.
64
65       If  two files have the same name, in two different directories, a warn‐
66       ing is printed on standard error.
67
68       There is no way to limit the scope of the recursive search for directo‐
69       ries.
70
71

EXAMPLES

73       Consider the files (in the same directory):
74
75            A.ml B.ml C.ml D.ml X.v Y.v and Z.v
76
77       where
78
79       +      D.ml contains the commands `open A', `open B' and `type t = C.t'
80              ;
81
82       +      Y.v contains the command `Require X' ;
83
84       +      Z.v contains the commands `Require X'  and  `Declare  ML  Module
85              "D"'.
86
87       To get the dependencies of the Coq files:
88
89              example% coqdep -I . *.v
90              Z.vo: Z.v ./X.vo ./D.cmo
91              Y.vo: Y.v ./X.vo
92              X.vo: X.v
93
94       With a warning:
95
96              example% coqdep -I . *.v
97              Z.vo: Z.v ./X.vo ./D.cmo
98              Y.vo: Y.v ./X.vo
99              X.vo: X.v
100              ### Warning : In file Z.v, the ML modules declaration should be
101              ### Declare ML Module "A" "B" "C" "D".
102
103

BUGS

105       Please report any bug to https://github.com/coq/coq/issues
106
107
108
109                                                                        COQ(1)