summaryrefslogtreecommitdiff
path: root/doc/refman/coqdoc.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/coqdoc.tex')
-rw-r--r--doc/refman/coqdoc.tex561
1 files changed, 561 insertions, 0 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
new file mode 100644
index 00000000..271a13f7
--- /dev/null
+++ b/doc/refman/coqdoc.tex
@@ -0,0 +1,561 @@
+
+%\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}{\&}
+%%% 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) 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 an 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{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}
+
+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 \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{--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 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}
+
+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{--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]{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}
+
+