aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/coqdoc.tex
blob: 7862c5c38fb048e4388fcaa9d089a1989907453a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476

%\newcommand{\Coq}{\textsf{Coq}}
\newcommand{\javadoc}{\textsf{javadoc}}
\newcommand{\ocamldoc}{\textsf{ocamldoc}}
\newcommand{\coqdoc}{\textsf{coqdoc}}
\newcommand{\texmacs}{\TeX{}macs}
\newcommand{\monurl}[1]{#1}
%HEVEA\renewcommand{\monurl}[1]{\ahref{#1}{#1}}
%HEVEA\newcommand{\lnot}{not}
%HEVEA\newcommand{\lor}{or}
%HEVEA\newcommand{\land}{\&}
%%% attention : -- dans un argument de \texttt est affiché comme un
%%% seul - d'où l'utilisation de la macro suivante
\newcommand{\mm}{\symbol{45}\symbol{45}}


\coqdoc\ is a documentation tool for the proof assistant
\Coq, similar to \javadoc\ or \ocamldoc. 
The task of \coqdoc\ is
\begin{enumerate}
\item to produce a nice \LaTeX\ and/or HTML document from the \Coq\ 
  sources, readable for a human and not only for the proof assistant;
\item to help the user navigating in his own (or third-party) sources.
\end{enumerate}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Principles}

Documentation is inserted into \Coq\ files as \emph{special comments}.  
Thus your files will compile as usual, whether you use \coqdoc\ or not.
\coqdoc\ presupposes that the given \Coq\ files are well-formed (at
least lexically).  Documentation starts with
\texttt{(**}, followed by a space, and ends with the pending \texttt{*)}. 
The documentation format is inspired
  by Todd~A.~Coram's \emph{Almost Free Text (AFT)} tool: it is mainly
ASCII text with some syntax-light controls, described below.
\coqdoc\ is robust: it shouldn't fail, whatever the input is. But
remember: ``garbage in, garbage out''.

\paragraph{\Coq\ material inside documentation.}
\Coq\ material is quoted between the
delimiters \texttt{[} and \texttt{]}. Square brackets may be nested,
the inner ones being understood as being part of the quoted code (thus
you can quote a term like $[x:T]u$ by writing
\texttt{[[x:T]u]}). Inside quotations, the code is pretty-printed in
the same way as it is in code parts.

Pre-formatted vernacular is enclosed by \texttt{[[} and
\texttt{]]}. The former must be followed by a newline and the latter
must follow a newline.

\paragraph{Pretty-printing.}
\coqdoc\ uses different faces for identifiers and keywords.  
The pretty-printing of \Coq\ tokens (identifiers or symbols) can be
controlled using one of the following commands:
\begin{alltt}
(** printing \emph{token} %...\LaTeX...% #...HTML...# *)
\end{alltt}
or
\begin{alltt}
(** printing \emph{token} $...\LaTeX\ math...$ #...HTML...# *)
\end{alltt}
It gives the \LaTeX\ and HTML texts to be produced for the given \Coq\
token. One of the \LaTeX\ or HTML text may be ommitted, causing the
default pretty-printing to be used for this token.

The printing for one token can be removed with
\begin{alltt}
(** remove printing \emph{token} *)
\end{alltt}

Initially, the pretty-printing table contains the following mapping:
\begin{center}
  \begin{tabular}{ll@{\qquad\qquad}ll@{\qquad\qquad}ll@{\qquad\qquad}}
    \verb!->!            & $\rightarrow$   &
    \verb!<-!            & $\leftarrow$    &
    \verb|*|             & $\times$        \\
    \verb|<=|            & $\le$           &
    \verb|>=|            & $\ge$           &
    \verb|=>|            & $\Rightarrow$   \\
    \verb|<>|            & $\not=$         &
    \verb|<->|           & $\leftrightarrow$ &
    \verb!|-!            & $\vdash$        \\
    \verb|\/|            & $\lor$          &
    \verb|/\|            & $\land$         &
    \verb|~|             & $\lnot$ 
  \end{tabular}
\end{center}
Any of these can be overwritten or suppressed using the
\texttt{printing} commands.

Important note: the recognition of tokens is done by a (ocaml)lex
automaton and thus applies the longest-match rule. For instance,
\verb!->~! is recognized as a single token, where \Coq\ sees two
tokens. It is the responsability of the user to insert space between
tokens \emph{or} to give pretty-printing rules for the possible
combinations, e.g. 
\begin{verbatim}
(** printing ->~ %\ensuremath{\rightarrow\lnot}% *)
\end{verbatim}


\paragraph{Sections.}
Sections are introduced by 1 to 4 leading stars (i.e. at the beginning of the
line). One star is a section, two stars a sub-section, etc.
The section title is given on the remaining of the line.
Example:
\begin{verbatim}
    (** * Well-founded relations
  
        In this section, we introduce...  *)
\end{verbatim}


%TODO \paragraph{Fonts.}


\paragraph{Lists.}
List items are introduced by 1 to 4 leading dashes.
Deepness of the list is indicated by the number of dashes.
List ends with a blank line.
Example:
\begin{verbatim}
    This module defines
        - the predecessor [pred]
        - the addition [plus]
        - order relations:
          -- less or equal [le]
          -- less [lt]
\end{verbatim}

\paragraph{Rules.}
More than 4 leading dashes produce an horizontal rule.


\paragraph{Escapings to \LaTeX\ and HTML.}
Pure \LaTeX\ or HTML material can be inserted using the following
escape sequences:
\begin{itemize}
\item \verb+$...LaTeX stuff...$+ inserts some \LaTeX\ material in math mode.
  Simply discarded in HTML output.

\item \verb+%...LaTeX stuff...%+ inserts some \LaTeX\ material.
  Simply discarded in HTML output.

\item \verb+#...HTML stuff...#+ inserts some HTML material. Simply
  discarded in \LaTeX\ output.
\end{itemize}


\paragraph{Verbatim.} 
Verbatim material is introduced by a leading \verb+<<+ and closed by
\verb+>>+. Example:
\begin{verbatim}
Here is the corresponding caml code:
<<
  let rec fact n = 
    if n <= 1 then 1 else n * fact (n-1)
>>
\end{verbatim}


\paragraph{Hyperlinks.}
Hyperlinks can be inserted into the HTML output, so that any
identifier is linked to the place of its definition.

In order to get hyperlinks you need to first compile your \Coq\ file
using \texttt{coqc \mm{}dump-glob \emph{file}}; this appends 
\Coq\ names resolutions done during the compilation to file
\texttt{\emph{file}}. Take care of erasing this file, if any, when
starting the whole compilation process.

Then invoke \texttt{coqdoc \mm{}glob-from \emph{file}} to tell
\coqdoc\ to look for name resolutions into the file \texttt{\emph{file}}.

Identifiers from the \Coq\ standard library are linked to the \Coq\
web site at \url{http://coq.inria.fr/library/}. This behavior can be
changed using command line options \url{--no-externals} and
\url{--coqlib}; see below.


\paragraph{Hiding / Showing parts of the source.}
Some parts of the source can be hidden using command line options
\texttt{-g} and \texttt{-l} (see below), or using such comments:
\begin{alltt}
(* begin hide *)
\emph{some Coq material}
(* end hide *)
\end{alltt}
Conversely, some parts of the source which would be hidden can be
shown using such comments: 
\begin{alltt}
(* begin show *)
\emph{some Coq material}
(* end show *)
\end{alltt}
The latter cannot be used around some inner parts of a proof, but can
be used around a whole proof.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Usage}

\coqdoc\ is invoked on a shell command line as follows:
\begin{displaymath}
  \texttt{coqdoc }<\textit{options and files}>
\end{displaymath}
Any command line argument which is not an option is considered to be a
file (even if it starts with a \verb!-!). \Coq\ files are identified
by the suffixes \verb!.v! and \verb!.g! and \LaTeX\ files by the
suffix \verb!.tex!. 

\begin{description}
\item[HTML output] ~\par
  This is the default output.
  One HTML file is created for each \Coq\ file given on the command line,
  together with a file \texttt{index.html} (unless option
  \texttt{-no-index} is passed). The HTML pages use a style sheet
  named \texttt{style.css}. Such a file is distributed with \coqdoc.

\item[\LaTeX\ output] ~\par
  A single \LaTeX\ file is created, on standard output. It can be
  redirected to a file with option \texttt{-o}. 
  The order of files on the command line is kept in the final
  document. \LaTeX\ files given on the command line are copied `as is'
  in the final document .
  DVI and PostScript can be produced directly with the options
  \texttt{-dvi} and \texttt{-ps} respectively.

\item[\texmacs\ output] ~\par
  To translate the input files to \texmacs\ format, to be used by
  the \texmacs\ Coq interface 
  (see \url{http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/}).
\end{description}


\subsubsection*{Command line options}


\paragraph{Overall options}

\begin{description}

\item[\texttt{\mm{}html}] ~\par
  
  Select a HTML output.

\item[\texttt{\mm{}latex}] ~\par
  
  Select a \LaTeX\ output.

\item[\texttt{\mm{}dvi}] ~\par
  
  Select a DVI output.

\item[\texttt{\mm{}ps}] ~\par
  
  Select a PostScript output.

\item[\texttt{\mm{}texmacs}] ~\par
  
  Select a \texmacs\ output.

\item[\texttt{-o }\textit{file}, \texttt{\mm{}output }\textit{file}] ~\par
  
  Redirect the output into the file `\textit{file}' (meaningless with
  \texttt{-html}).

\item[\texttt{-d }\textit{dir}, \texttt{\mm{}directory }\textit{dir}] ~\par

  Output files into directory `\textit{dir}' instead of current
  directory (option \texttt{-d} does not change the filename specified
  with option \texttt{-o}, if any).

\item[\texttt{-s }, \texttt{\mm{}short}] ~\par
  
  Do not insert titles for the files. The default behavior is to
  insert a title like ``Library Foo'' for each file.

\item[\texttt{-t }\textit{string}, 
      \texttt{\mm{}title }\textit{string}] ~\par
  
  Set the document title.      

\item[\texttt{\mm{}body-only}] ~\par

  Suppress the header and trailer of the final document. Thus, you can
  insert the resulting document into a larger one.

\item[\texttt{-p} \textit{string}, \texttt{\mm{}preamble} \textit{string}]~\par

  Insert some material in the \LaTeX\ preamble, right before
  \verb!\begin{document}! (meaningless with \texttt{-html}).

\item[\texttt{\mm{}vernac-file }\textit{file},
      \texttt{\mm{}tex-file }\textit{file}] ~\par
      
      Considers the file `\textit{file}' respectively as a \verb!.v!
      (or \verb!.g!) file or a \verb!.tex! file.

\item[\texttt{\mm{}files-from }\textit{file}] ~\par

  Read file names to process in file `\textit{file}' as if they were
  given on the command line. Useful for program sources splitted in
  several directories.
  
\item[\texttt{-q}, \texttt{\mm{}quiet}] ~\par

  Be quiet. Do not print anything except errors.

\item[\texttt{-h}, \texttt{\mm{}help}] ~\par

  Give a short summary of the options and exit.

\item[\texttt{-v}, \texttt{\mm{}version}] ~\par

  Print the version and exit.

\end{description}

\paragraph{Index options} ~\par

Default behavior is to build an index, for the HTML output only, into
\texttt{index.html}.

\begin{description}

\item[\texttt{\mm{}no-index}] ~\par
  
  Do not output the index.

\item[\texttt{\mm{}multi-index}] ~\par
  
  Generate one page for each category and each letter in the index,
  together with a top page \texttt{index.html}.

\end{description}

\paragraph{Table of contents option} ~\par

\begin{description}

\item[\texttt{-toc}, \texttt{\mm{}table-of-contents}] ~\par

  Insert a table of contents.
  For a \LaTeX\ output, it inserts a \verb!\tableofcontents! at the
  beginning of the document. For a HTML output, it builds a table of
  contents into \texttt{toc.html}.

\end{description}

\paragraph{Hyperlinks options}
\begin{description}

\item[\texttt{\mm{}glob-from }\textit{file}] ~\par
  
  Make references using \Coq\ globalizations from file \textit{file}. 
  (Such globalizations are obtained with \Coq\ option \texttt{-dump-glob}).

\item[\texttt{\mm{}no-externals}] ~\par
  
  Do not insert links to the \Coq\ standard library.

\item[\texttt{\mm{}coqlib }\textit{url}] ~\par

  Set base URL for the \Coq\ standard library (default is 
  \url{http://coq.inria.fr/library/}).

\item[\texttt{-R }\textit{dir }\textit{coqdir}] ~\par

  Map physical directory \textit{dir} to \Coq\ logical directory
  \textit{coqdir} (similarly to \Coq\ option \texttt{-R}).

  Note: option \texttt{-R} only has effect on the files
  \emph{following} it on the command line, so you will probably need
  to put this option first.

\end{description}

\paragraph{Contents options}
\begin{description}

\item[\texttt{-g}, \texttt{\mm{}gallina}] ~\par

  Do not print proofs.

\item[\texttt{-l}, \texttt{\mm{}light}] ~\par
  
  Light mode. Suppress proofs (as with \texttt{-g}) and the following commands:
  \begin{itemize}
  \item {}[\texttt{Recursive}] \texttt{Tactic Definition}
  \item \texttt{Hint / Hints} 
  \item \texttt{Require}
  \item \texttt{Transparent / Opaque}
  \item \texttt{Implicit Argument / Implicits}
  \item \texttt{Section / Variable / Hypothesis / End}
  \end{itemize}

\end{description}
The behavior of options \texttt{-g} and \texttt{-l} can be locally
overridden using the \texttt{(* begin show *)} \dots\ \texttt{(* end
  show *)} environment (see above).

\paragraph{Language options} ~\par

Default behavior is to assume ASCII 7 bits input files.

\begin{description}

\item[\texttt{-latin1}, \texttt{\mm{}latin1}] ~\par

  Select ISO-8859-1 input files. It is equivalent to
  \texttt{--inputenc latin1 --charset iso-8859-1}.

\item[\texttt{-utf8}, \texttt{\mm{}utf8}] ~\par

  Select UTF-8 (Unicode) input files. It is equivalent to
  \texttt{--inputenc utf8 --charset utf-8}.
  \LaTeX\ UTF-8 support can be found at
 \url{http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/}.

\item[\texttt{\mm{}inputenc} \textit{string}] ~\par

  Give a \LaTeX\ input encoding, as an option to \LaTeX\ package
  \texttt{inputenc}. 

\item[\texttt{\mm{}charset} \textit{string}] ~\par

  Specify the HTML character set, to be inserted in the HTML header.

\end{description}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{The coqdoc \LaTeX{} style file}
\label{section:coqdoc.sty}

In case you choose to produce a document without the default \LaTeX{}
preamble (by using option \verb|--no-preamble|), then you must insert
into your own preamble the command
\begin{quote}
  \verb|\usepackage{coqdoc}|
\end{quote}
Then you may alter the rendering of the document by
redefining some macros:
\begin{description}

\item[\texttt{coqdockw}, \texttt{coqdocid}] ~ 
  
  The one-argument macros for typesetting keywords and identifiers.
  Defaults are sans-serif for keywords and italic for identifiers.

  For example, if you would like a slanted font for keywords, you
  may insert  
\begin{verbatim}
     \renewcommand{\coqdockw}[1]{\textsl{#1}}
\end{verbatim}
  anywhere between \verb|\usepackage{coqdoc}| and
  \verb|\begin{document}|. 

\item[\texttt{coqdocmodule}] ~ 
  
  One-argument macro for typesetting the title of a \verb|.v| file.
  Default is
\begin{verbatim}
\newcommand{\coqdocmodule}[1]{\section*{Module #1}}
\end{verbatim}
  and you may redefine it using \verb|\renewcommand|.

\end{description}