diff options
Diffstat (limited to 'doc/refman/coqdoc.tex')
| -rw-r--r-- | doc/refman/coqdoc.tex | 476 |
1 files changed, 476 insertions, 0 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex new file mode 100644 index 00000000..7862c5c3 --- /dev/null +++ b/doc/refman/coqdoc.tex @@ -0,0 +1,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} + + |