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