aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/coqdoc.tex
blob: 26dbd59e7643311e48dbc2f9b84dc2f4c0e27ea6 (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
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573

%\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}}
%\newcommand{\lnot}{not} % Hevea handles these symbols nicely
%\newcommand{\lor}{or}
%\newcommand{\land}{\&}
%%% Beware : in a \texttt, -- is displayed as a unique - hence
%%% the following macro:
\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 \texttt{fun x => u} by writing
\texttt{[fun x => 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 omitted, 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 responsibility 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) followed by a space. 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 a leading dash.  \coqdoc\ uses whitespace
to determine the depth of a new list item and which text belongs in
which list items.  A list ends when a line of text starts at or before
the level of indenting of the list's dash.  A list item's dash must
always be the first non-space character on its line (so, in
particular, a list can not begin on the first line of a comment -
start it on the second line instead).

Example:
\begin{verbatim}
     We go by induction on [n]:
     - If [n] is 0...
     - If [n] is [S n'] we require...

       two paragraphs of reasoning, and two subcases:

       - In the first case...
       - In the second case...

     So the theorem holds.
\end{verbatim}

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

\paragraph{Emphasis.}
Text can be italicized by placing it in underscores.  A non-identifier
character must precede the leading underscore and follow the trailing
underscore, so that uses of underscores in names aren't mistaken for
emphasis.  Usually, these are spaces or punctuation.

\begin{verbatim}
    This sentence contains some _emphasized text_.
\end{verbatim}

\paragraph{Escaping 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}

Note: to simply output the characters \verb+$+, \verb+%+ and \verb+#+
and escaping their escaping role, these characters must be doubled.

\paragraph{Verbatim.} 
Verbatim material is introduced by a leading \verb+<<+ and closed by
\verb+>>+ at the beginning of a line. 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.

\texttt{coqc \emph{file}.v} automatically dumps localization information
in \texttt{\emph{file}.glob} or appends it to a file specified using option
\texttt{\mm{}dump-glob \emph{file}}. Take care of erasing this global file, if
any, when starting the whole compilation process.

Then invoke \texttt{coqdoc} or \texttt{coqdoc \mm{}glob-from \emph{file}} to tell
\coqdoc\ to look for name resolutions into the file \texttt{\emph{file}}
(it will look in \texttt{\emph{file}.glob} by default).

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 \texttt{\mm{}no-externals} and
\texttt{\mm{}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.
  %broken link:
  %(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{\mm{}stdout}] ~\par

  Write output to stdout.

\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{\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 split up into
  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}

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}.

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

  Make the filename of the index \textit{string} instead of ``index''.
  Useful since ``index.html'' is special.

\end{description}

\paragraph{Table of contents option}

\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}.

\item[\texttt{\mm{}toc-depth }\textit{int}] ~\par

  Only include headers up to depth \textit{int} in the table of
  contents.

\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{}external }\textit{url}~\textit{coqdir}] ~\par
  
  Use given URL for linking references whose name starts with prefix
  \textit{coqdir}.

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

  Set base URL for the \Coq\ standard library (default is 
  \url{http://coq.inria.fr/library/}). This is equivalent to
  \texttt{\mm{}external }\textit{url}~\texttt{Coq}.

\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{Title options}
\begin{description}
\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{\mm{}lib-name }\textit{string}] ~\par

  Print ``\textit{string} Foo'' instead of ``Library Foo'' in titles.
  For example ``Chapter'' and ``Module'' are reasonable choices.

\item[\texttt{\mm{}no-lib-name}] ~\par

  Print just ``Foo'' instead of ``Library Foo'' in titles.

\item[\texttt{\mm{}lib-subtitles}] ~\par

  Look for library subtitles.  When enabled, the beginning of each
  file is checked for a comment of the form:
\begin{alltt}
(** * ModuleName : text *)
\end{alltt}
  where \texttt{ModuleName} must be the name of the file.  If it is
  present, the \texttt{text} is used as a subtitle for the module in
  appropriate places.

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

\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).

There are a few options to drive the parsing of comments:
\begin{description}
\item[\texttt{\mm{}parse-comments}] ~\par

  Parses regular comments delimited by \texttt{(*} and \texttt{*)} as 
  well. They are typeset inline.

\item[\texttt{\mm{}plain-comments}] ~\par

  Do not interpret comments, simply copy them as plain-text.

\item[\texttt{\mm{}interpolate}] ~\par

  Use the globalization information to typeset identifiers appearing in
  \Coq{} escapings inside comments.
\end{description}


\paragraph{Language options}

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{\mm{}inputenc latin1 \mm{}charset iso-8859-1}.

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

  Set \texttt{\mm{}inputenc utf8x} for \LaTeX\ output and
  \texttt{\mm{}charset utf-8} for HTML output. Also use Unicode
  replacements for a couple of standard plain ASCII notations such
  as $\rightarrow$ for \texttt{->} and $\forall$ for
  \texttt{forall}. \LaTeX\ UTF-8 support can be found at
  \url{http://www.ctan.org/pkg/unicode}.

  For the interpretation of Unicode characters by \LaTeX, extra
  packages which {\coqdoc} does not provide by default might be
  required, such as \texttt{textgreek} for some Greek letters or
  \texttt{stmaryrd} for some mathematical symbols. If a Unicode
  character is missing an interpretation in the \texttt{utf8x} input
  encoding, add
  \verb=\DeclareUnicodeCharacter{=\textit{code}\verb=}{=\textit{latex-interpretation}\verb=}=. Packages
  and declarations can be added with option \texttt{-p}.

\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]{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}

The package optionally takes the argument \verb|[color]| to typeset
identifiers with colors (this requires the \verb|xcolor| package).

Then you may alter the rendering of the document by
redefining some macros:
\begin{description}

\item[\texttt{coqdockw}, \texttt{coqdocid}, \ldots] ~ 
  
  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}