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 [ -w ] [ -I directory ] [ -coqlib directory ] [ -c ] [ -i ] [ -D
11       ] [ -slash ] filename ...  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,  Require  Implementation),
22       Declare  ML Module commands and Load commands. Dependencies relative to
23       modules from the Coq library are not printed.
24
25       Dependencies of Caml modules are computed by looking at open directives
26       and the dot notation module.value.
27
28

OPTIONS

30       -c     Prints  the dependencies of Caml modules.  (On Caml modules, the
31              behaviour is exactly the same as ocamldep).
32
33       -w     Prints a warning if a Coq command Declare ML  Module  is  incor‐
34              rect. (For instance, you wrote `Declare ML Module "A".', but the
35              module A contains #open "B"). The  correct  command  is  printed
36              (see option -D). The warning is printed on standard error.
37
38       -i     Prints  also  the  dependencies for .vi files (Coq specification
39              modules).
40
41       -D     This commands looks for every command Declare ML Module of  each
42              Coq  file given as argument and complete (if needed) the list of
43              Caml modules. The new command is printed on the standard output.
44              No dependency is computed with this option.
45
46       -slash Prints paths using a slash instead of the OS specific separator.
47              This option is useful when developping under Cygwin.
48
49       -I directory
50              The files .v .ml .mli of the directory directory are taken  into
51              account  during  the  calculus  of  dependencies,  but their own
52              dependencies are not printed.
53
54       -coqlib directory
55              Indicates where is the Coq library. The default value  has  been
56              determined  at  installation  time,  and  therefore  this option
57              should not be used under normal circumstances.
58
59
60

SEE ALSO

62       ocamlc(1), coqc(1), make(1).
63
64

NOTES

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

EXAMPLES

78       Consider the files (in the same directory):
79
80            A.ml B.ml C.ml D.ml X.v Y.v and Z.v
81
82       where
83
84       +      D.ml contains the commands `open A', `open B' and `type t = C.t'
85              ;
86
87       +      Y.v contains the command `Require X' ;
88
89       +      Z.v  contains  the  commands  `Require X' and `Declare ML Module
90              "D"'.
91
92       To get the dependencies of the Coq files:
93
94              example% coqdep -I . *.v
95              Z.vo: Z.v ./X.vo ./D.cmo
96              Y.vo: Y.v ./X.vo
97              X.vo: X.v
98
99       With a warning:
100
101              example% coqdep -w -I . *.v
102              Z.vo: Z.v ./X.vo ./D.cmo
103              Y.vo: Y.v ./X.vo
104              X.vo: X.v
105              ### Warning : In file Z.v, the ML modules declaration should be
106              ### Declare ML Module "A" "B" "C" "D".
107
108       To get only the Caml dependencies:
109
110              example% coqdep -c -I . *.ml
111              D.cmo: D.ml ./A.cmo ./B.cmo ./C.cmo
112              D.cmx: D.ml ./A.cmx ./B.cmx ./C.cmx
113              C.cmo: C.ml
114              C.cmx: C.ml
115              B.cmo: B.ml
116              B.cmx: B.ml
117              A.cmo: A.ml
118              A.cmx: A.ml
119
120

BUGS

122       Please report any bug to coq-bugs@pauillac.inria.fr
123
124
125
126Coq tools                        28 March 1995                          COQ(1)