← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to man/coqdep.1

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
man/coqdep.1
 
1
.TH COQ 1 "28 March 1995" "Coq tools"
 
2
 
 
3
.SH NAME
 
4
coqdep \- Compute inter-module dependencies for Coq and Caml programs
 
5
 
 
6
.SH SYNOPSIS
 
7
.B coqdep
 
8
[
 
9
.BI \-w
 
10
]
 
11
[
 
12
.BI \-I \ directory
 
13
]
 
14
[
 
15
.BI \-coqlib \ directory
 
16
]
 
17
[
 
18
.BI \-c
 
19
]
 
20
[
 
21
.BI \-i
 
22
]
 
23
[
 
24
.BI \-D
 
25
]
 
26
[
 
27
.BI \-slash
 
28
]
 
29
.I filename ...
 
30
.I directory ...
 
31
 
 
32
.SH DESCRIPTION
 
33
 
 
34
.B coqdep
 
35
compute inter-module dependencies for Coq and Caml programs,
 
36
and prints the dependencies on the standard output in a format
 
37
readable by make.
 
38
When a directory is given as argument, it is recursively looked at.
 
39
 
 
40
Dependencies of Coq modules are computed by looking at
 
41
.IR Require \&
 
42
commands (Require, Require Export, Require Import, Require Implementation),
 
43
.IR Declare \& 
 
44
.IR ML \& 
 
45
.IR Module \&
 
46
commands and
 
47
.IR Load \&
 
48
commands. Dependencies relative to modules from the Coq library are not
 
49
printed.
 
50
 
 
51
Dependencies of Caml modules are computed by looking at
 
52
.IR open \&
 
53
directives and the dot notation
 
54
.IR module.value \&.
 
55
 
 
56
.SH OPTIONS
 
57
 
 
58
.TP
 
59
.BI \-c
 
60
Prints the dependencies of Caml modules.
 
61
(On Caml modules, the behaviour is exactly the same as ocamldep).
 
62
.TP
 
63
.BI \-w
 
64
Prints a warning if a Coq command
 
65
.IR Declare \& 
 
66
.IR ML \& 
 
67
.IR Module \&
 
68
is incorrect. (For instance, you wrote `Declare ML Module "A".',
 
69
but the module A contains #open "B"). The correct command is printed
 
70
(see option \-D). The warning is printed on standard error.
 
71
.TP
 
72
.BI \-i
 
73
Prints also the dependencies for .vi files (Coq specification modules).
 
74
.TP
 
75
.BI \-D
 
76
This commands looks for every command
 
77
.IR Declare \& 
 
78
.IR ML \& 
 
79
.IR Module \&
 
80
of each Coq file given as argument and complete (if needed)
 
81
the list of Caml modules. The new command is printed on
 
82
the standard output. No dependency is computed with this option.
 
83
.TP 
 
84
.BI \-slash
 
85
Prints paths using a slash instead of the OS specific separator. This
 
86
option is useful when developping under Cygwin.
 
87
.TP
 
88
.BI \-I \ directory
 
89
The files .v .ml .mli of the directory
 
90
.IR directory \&
 
91
are taken into account during the calculus of dependencies,
 
92
but their own dependencies are not printed.
 
93
.TP 
 
94
.BI \-coqlib \ directory
 
95
Indicates where is the Coq library. The default value has been
 
96
determined at installation time, and therefore this option should not
 
97
be used under normal circumstances.
 
98
 
 
99
 
 
100
.SH SEE ALSO
 
101
 
 
102
.BR ocamlc (1),
 
103
.BR coqc (1),
 
104
.BR make (1).
 
105
.br
 
106
 
 
107
.SH NOTES
 
108
 
 
109
Lexers (for Coq and Caml) correctly handle nested comments
 
110
and strings.
 
111
 
 
112
The treatment of symbolic links is primitive.
 
113
 
 
114
If two files have the same name, in two different directories,
 
115
a warning is printed on standard error.
 
116
 
 
117
There is no way to limit the scope of the recursive search for
 
118
directories.
 
119
 
 
120
.SH EXAMPLES
 
121
 
 
122
.LP
 
123
Consider the files (in the same directory):
 
124
 
 
125
        A.ml B.ml C.ml D.ml X.v Y.v and Z.v
 
126
 
 
127
where
 
128
.TP
 
129
.BI \+ 
 
130
D.ml contains the commands `open A', `open B' and `type t = C.t' ;
 
131
.TP
 
132
.BI \+
 
133
Y.v contains the command `Require X' ;
 
134
.TP
 
135
.BI \+
 
136
Z.v contains the commands `Require X' and `Declare ML Module "D"'.
 
137
.LP
 
138
To get the dependencies of the Coq files:
 
139
.IP
 
140
.B
 
141
example% coqdep \-I . *.v
 
142
.RS
 
143
.sp .5
 
144
.nf
 
145
.B Z.vo: Z.v ./X.vo ./D.cmo
 
146
.B Y.vo: Y.v ./X.vo
 
147
.B X.vo: X.v
 
148
.fi
 
149
.RE
 
150
.br
 
151
.ne 7
 
152
.LP
 
153
With a warning:
 
154
.IP
 
155
.B
 
156
example% coqdep \-w \-I . *.v
 
157
.RS
 
158
.sp .5
 
159
.nf
 
160
.B Z.vo: Z.v ./X.vo ./D.cmo
 
161
.B Y.vo: Y.v ./X.vo
 
162
.B X.vo: X.v
 
163
### Warning : In file Z.v, the ML modules declaration should be
 
164
### Declare ML Module "A" "B" "C" "D".
 
165
.fi
 
166
.RE
 
167
.br
 
168
.ne 7
 
169
.LP
 
170
To get only the Caml dependencies:
 
171
.IP
 
172
.B
 
173
example% coqdep \-c \-I . *.ml
 
174
.RS
 
175
.sp .5
 
176
.nf
 
177
.B D.cmo: D.ml ./A.cmo ./B.cmo ./C.cmo
 
178
.B D.cmx: D.ml ./A.cmx ./B.cmx ./C.cmx
 
179
.B C.cmo: C.ml
 
180
.B C.cmx: C.ml
 
181
.B B.cmo: B.ml
 
182
.B B.cmx: B.ml
 
183
.B A.cmo: A.ml
 
184
.B A.cmx: A.ml
 
185
.fi
 
186
.RE
 
187
.br
 
188
.ne 7
 
189
 
 
190
.SH BUGS
 
191
 
 
192
Please report any bug to
 
193
.B coq\-bugs@pauillac.inria.fr