2
%\newcommand{\Coq}{\textsf{Coq}}
3
\newcommand{\javadoc}{\textsf{javadoc}}
4
\newcommand{\ocamldoc}{\textsf{ocamldoc}}
5
\newcommand{\coqdoc}{\textsf{coqdoc}}
6
\newcommand{\texmacs}{\TeX{}macs}
7
\newcommand{\monurl}[1]{#1}
8
%HEVEA\renewcommand{\monurl}[1]{\ahref{#1}{#1}}
9
%HEVEA\newcommand{\lnot}{not}
10
%HEVEA\newcommand{\lor}{or}
11
%HEVEA\newcommand{\land}{\&}
12
%%% attention : -- dans un argument de \texttt est affich� comme un
13
%%% seul - d'o� l'utilisation de la macro suivante
14
\newcommand{\mm}{\symbol{45}\symbol{45}}
17
\coqdoc\ is a documentation tool for the proof assistant
18
\Coq, similar to \javadoc\ or \ocamldoc.
19
The task of \coqdoc\ is
21
\item to produce a nice \LaTeX\ and/or HTML document from the \Coq\
22
sources, readable for a human and not only for the proof assistant;
23
\item to help the user navigating in his own (or third-party) sources.
27
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
29
\subsection{Principles}
31
Documentation is inserted into \Coq\ files as \emph{special comments}.
32
Thus your files will compile as usual, whether you use \coqdoc\ or not.
33
\coqdoc\ presupposes that the given \Coq\ files are well-formed (at
34
least lexically). Documentation starts with
35
\texttt{(**}, followed by a space, and ends with the pending \texttt{*)}.
36
The documentation format is inspired
37
by Todd~A.~Coram's \emph{Almost Free Text (AFT)} tool: it is mainly
38
ASCII text with some syntax-light controls, described below.
39
\coqdoc\ is robust: it shouldn't fail, whatever the input is. But
40
remember: ``garbage in, garbage out''.
42
\paragraph{\Coq\ material inside documentation.}
43
\Coq\ material is quoted between the
44
delimiters \texttt{[} and \texttt{]}. Square brackets may be nested,
45
the inner ones being understood as being part of the quoted code (thus
46
you can quote a term like $[x:T]u$ by writing
47
\texttt{[[x:T]u]}). Inside quotations, the code is pretty-printed in
48
the same way as it is in code parts.
50
Pre-formatted vernacular is enclosed by \texttt{[[} and
51
\texttt{]]}. The former must be followed by a newline and the latter
52
must follow a newline.
54
\paragraph{Pretty-printing.}
55
\coqdoc\ uses different faces for identifiers and keywords.
56
The pretty-printing of \Coq\ tokens (identifiers or symbols) can be
57
controlled using one of the following commands:
59
(** printing \emph{token} %...\LaTeX...% #...HTML...# *)
63
(** printing \emph{token} $...\LaTeX\ math...$ #...HTML...# *)
65
It gives the \LaTeX\ and HTML texts to be produced for the given \Coq\
66
token. One of the \LaTeX\ or HTML text may be ommitted, causing the
67
default pretty-printing to be used for this token.
69
The printing for one token can be removed with
71
(** remove printing \emph{token} *)
74
Initially, the pretty-printing table contains the following mapping:
76
\begin{tabular}{ll@{\qquad\qquad}ll@{\qquad\qquad}ll@{\qquad\qquad}}
77
\verb!->! & $\rightarrow$ &
78
\verb!<-! & $\leftarrow$ &
79
\verb|*| & $\times$ \\
82
\verb|=>| & $\Rightarrow$ \\
84
\verb|<->| & $\leftrightarrow$ &
85
\verb!|-! & $\vdash$ \\
91
Any of these can be overwritten or suppressed using the
92
\texttt{printing} commands.
94
Important note: the recognition of tokens is done by a (ocaml)lex
95
automaton and thus applies the longest-match rule. For instance,
96
\verb!->~! is recognized as a single token, where \Coq\ sees two
97
tokens. It is the responsability of the user to insert space between
98
tokens \emph{or} to give pretty-printing rules for the possible
101
(** printing ->~ %\ensuremath{\rightarrow\lnot}% *)
105
\paragraph{Sections.}
106
Sections are introduced by 1 to 4 leading stars (i.e. at the beginning of the
107
line). One star is a section, two stars a sub-section, etc.
108
The section title is given on the remaining of the line.
111
(** * Well-founded relations
113
In this section, we introduce... *)
117
%TODO \paragraph{Fonts.}
121
List items are introduced by 1 to 4 leading dashes.
122
Deepness of the list is indicated by the number of dashes.
123
List ends with a blank line.
127
- the predecessor [pred]
128
- the addition [plus]
130
-- less or equal [le]
135
More than 4 leading dashes produce an horizontal rule.
138
\paragraph{Escapings to \LaTeX\ and HTML.}
139
Pure \LaTeX\ or HTML material can be inserted using the following
142
\item \verb+$...LaTeX stuff...$+ inserts some \LaTeX\ material in math mode.
143
Simply discarded in HTML output.
145
\item \verb+%...LaTeX stuff...%+ inserts some \LaTeX\ material.
146
Simply discarded in HTML output.
148
\item \verb+#...HTML stuff...#+ inserts some HTML material. Simply
149
discarded in \LaTeX\ output.
153
\paragraph{Verbatim.}
154
Verbatim material is introduced by a leading \verb+<<+ and closed by
157
Here is the corresponding caml code:
160
if n <= 1 then 1 else n * fact (n-1)
165
\paragraph{Hyperlinks.}
166
Hyperlinks can be inserted into the HTML output, so that any
167
identifier is linked to the place of its definition.
169
In order to get hyperlinks you need to first compile your \Coq\ file
170
using \texttt{coqc \mm{}dump-glob \emph{file}}; this appends
171
\Coq\ names resolutions done during the compilation to file
172
\texttt{\emph{file}}. Take care of erasing this file, if any, when
173
starting the whole compilation process.
175
Then invoke \texttt{coqdoc \mm{}glob-from \emph{file}} to tell
176
\coqdoc\ to look for name resolutions into the file \texttt{\emph{file}}.
178
Identifiers from the \Coq\ standard library are linked to the \Coq\
179
web site at \url{http://coq.inria.fr/library/}. This behavior can be
180
changed using command line options \url{--no-externals} and
181
\url{--coqlib}; see below.
184
\paragraph{Hiding / Showing parts of the source.}
185
Some parts of the source can be hidden using command line options
186
\texttt{-g} and \texttt{-l} (see below), or using such comments:
189
\emph{some Coq material}
192
Conversely, some parts of the source which would be hidden can be
193
shown using such comments:
196
\emph{some Coq material}
199
The latter cannot be used around some inner parts of a proof, but can
200
be used around a whole proof.
203
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
207
\coqdoc\ is invoked on a shell command line as follows:
209
\texttt{coqdoc }<\textit{options and files}>
211
Any command line argument which is not an option is considered to be a
212
file (even if it starts with a \verb!-!). \Coq\ files are identified
213
by the suffixes \verb!.v! and \verb!.g! and \LaTeX\ files by the
217
\item[HTML output] ~\par
218
This is the default output.
219
One HTML file is created for each \Coq\ file given on the command line,
220
together with a file \texttt{index.html} (unless option
221
\texttt{-no-index} is passed). The HTML pages use a style sheet
222
named \texttt{style.css}. Such a file is distributed with \coqdoc.
224
\item[\LaTeX\ output] ~\par
225
A single \LaTeX\ file is created, on standard output. It can be
226
redirected to a file with option \texttt{-o}.
227
The order of files on the command line is kept in the final
228
document. \LaTeX\ files given on the command line are copied `as is'
229
in the final document .
230
DVI and PostScript can be produced directly with the options
231
\texttt{-dvi} and \texttt{-ps} respectively.
233
\item[\texmacs\ output] ~\par
234
To translate the input files to \texmacs\ format, to be used by
235
the \texmacs\ Coq interface
236
(see \url{http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/}).
240
\subsubsection*{Command line options}
243
\paragraph{Overall options}
247
\item[\texttt{\mm{}html}] ~\par
249
Select a HTML output.
251
\item[\texttt{\mm{}latex}] ~\par
253
Select a \LaTeX\ output.
255
\item[\texttt{\mm{}dvi}] ~\par
259
\item[\texttt{\mm{}ps}] ~\par
261
Select a PostScript output.
263
\item[\texttt{\mm{}texmacs}] ~\par
265
Select a \texmacs\ output.
267
\item[\texttt{--stdout}] ~\par
269
Write output to stdout.
271
\item[\texttt{-o }\textit{file}, \texttt{\mm{}output }\textit{file}] ~\par
273
Redirect the output into the file `\textit{file}' (meaningless with
276
\item[\texttt{-d }\textit{dir}, \texttt{\mm{}directory }\textit{dir}] ~\par
278
Output files into directory `\textit{dir}' instead of current
279
directory (option \texttt{-d} does not change the filename specified
280
with option \texttt{-o}, if any).
282
\item[\texttt{-s }, \texttt{\mm{}short}] ~\par
284
Do not insert titles for the files. The default behavior is to
285
insert a title like ``Library Foo'' for each file.
287
\item[\texttt{-t }\textit{string},
288
\texttt{\mm{}title }\textit{string}] ~\par
290
Set the document title.
292
\item[\texttt{\mm{}body-only}] ~\par
294
Suppress the header and trailer of the final document. Thus, you can
295
insert the resulting document into a larger one.
297
\item[\texttt{-p} \textit{string}, \texttt{\mm{}preamble} \textit{string}]~\par
299
Insert some material in the \LaTeX\ preamble, right before
300
\verb!\begin{document}! (meaningless with \texttt{-html}).
302
\item[\texttt{\mm{}vernac-file }\textit{file},
303
\texttt{\mm{}tex-file }\textit{file}] ~\par
305
Considers the file `\textit{file}' respectively as a \verb!.v!
306
(or \verb!.g!) file or a \verb!.tex! file.
308
\item[\texttt{\mm{}files-from }\textit{file}] ~\par
310
Read file names to process in file `\textit{file}' as if they were
311
given on the command line. Useful for program sources splitted in
314
\item[\texttt{-q}, \texttt{\mm{}quiet}] ~\par
316
Be quiet. Do not print anything except errors.
318
\item[\texttt{-h}, \texttt{\mm{}help}] ~\par
320
Give a short summary of the options and exit.
322
\item[\texttt{-v}, \texttt{\mm{}version}] ~\par
324
Print the version and exit.
328
\paragraph{Index options} ~\par
330
Default behavior is to build an index, for the HTML output only, into
335
\item[\texttt{\mm{}no-index}] ~\par
337
Do not output the index.
339
\item[\texttt{\mm{}multi-index}] ~\par
341
Generate one page for each category and each letter in the index,
342
together with a top page \texttt{index.html}.
346
\paragraph{Table of contents option} ~\par
350
\item[\texttt{-toc}, \texttt{\mm{}table-of-contents}] ~\par
352
Insert a table of contents.
353
For a \LaTeX\ output, it inserts a \verb!\tableofcontents! at the
354
beginning of the document. For a HTML output, it builds a table of
355
contents into \texttt{toc.html}.
359
\paragraph{Hyperlinks options}
362
\item[\texttt{\mm{}glob-from }\textit{file}] ~\par
364
Make references using \Coq\ globalizations from file \textit{file}.
365
(Such globalizations are obtained with \Coq\ option \texttt{-dump-glob}).
367
\item[\texttt{\mm{}no-externals}] ~\par
369
Do not insert links to the \Coq\ standard library.
371
\item[\texttt{\mm{}coqlib }\textit{url}] ~\par
373
Set base URL for the \Coq\ standard library (default is
374
\url{http://coq.inria.fr/library/}).
376
\item[\texttt{-R }\textit{dir }\textit{coqdir}] ~\par
378
Map physical directory \textit{dir} to \Coq\ logical directory
379
\textit{coqdir} (similarly to \Coq\ option \texttt{-R}).
381
Note: option \texttt{-R} only has effect on the files
382
\emph{following} it on the command line, so you will probably need
383
to put this option first.
387
\paragraph{Contents options}
390
\item[\texttt{-g}, \texttt{\mm{}gallina}] ~\par
394
\item[\texttt{-l}, \texttt{\mm{}light}] ~\par
396
Light mode. Suppress proofs (as with \texttt{-g}) and the following commands:
398
\item {}[\texttt{Recursive}] \texttt{Tactic Definition}
399
\item \texttt{Hint / Hints}
400
\item \texttt{Require}
401
\item \texttt{Transparent / Opaque}
402
\item \texttt{Implicit Argument / Implicits}
403
\item \texttt{Section / Variable / Hypothesis / End}
407
The behavior of options \texttt{-g} and \texttt{-l} can be locally
408
overridden using the \texttt{(* begin show *)} \dots\ \texttt{(* end
409
show *)} environment (see above).
411
\paragraph{Language options} ~\par
413
Default behavior is to assume ASCII 7 bits input files.
417
\item[\texttt{-latin1}, \texttt{\mm{}latin1}] ~\par
419
Select ISO-8859-1 input files. It is equivalent to
420
\texttt{--inputenc latin1 --charset iso-8859-1}.
422
\item[\texttt{-utf8}, \texttt{\mm{}utf8}] ~\par
424
Select UTF-8 (Unicode) input files. It is equivalent to
425
\texttt{--inputenc utf8 --charset utf-8}.
426
\LaTeX\ UTF-8 support can be found at
427
\url{http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/}.
429
\item[\texttt{\mm{}inputenc} \textit{string}] ~\par
431
Give a \LaTeX\ input encoding, as an option to \LaTeX\ package
434
\item[\texttt{\mm{}charset} \textit{string}] ~\par
436
Specify the HTML character set, to be inserted in the HTML header.
441
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
443
\subsection{The coqdoc \LaTeX{} style file}
444
\label{section:coqdoc.sty}
446
In case you choose to produce a document without the default \LaTeX{}
447
preamble (by using option \verb|--no-preamble|), then you must insert
448
into your own preamble the command
450
\verb|\usepackage{coqdoc}|
452
Then you may alter the rendering of the document by
453
redefining some macros:
456
\item[\texttt{coqdockw}, \texttt{coqdocid}] ~
458
The one-argument macros for typesetting keywords and identifiers.
459
Defaults are sans-serif for keywords and italic for identifiers.
461
For example, if you would like a slanted font for keywords, you
464
\renewcommand{\coqdockw}[1]{\textsl{#1}}
466
anywhere between \verb|\usepackage{coqdoc}| and
467
\verb|\begin{document}|.
469
\item[\texttt{coqdocmodule}] ~
471
One-argument macro for typesetting the title of a \verb|.v| file.
474
\newcommand{\coqdocmodule}[1]{\section*{Module #1}}
476
and you may redefine it using \verb|\renewcommand|.
added
removed
refman/coqdoc.tex
