Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 276 insertions, 0 deletions

diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
new file mode 100644
index 00000000..4d73b878
--- /dev/null
+++ b/doc/refman/RefMan-uti.tex
@@ -0,0 +1,276 @@
+\chapter{Utilities}\label{Utilities}
+
+The distribution provides utilities to simplify some tedious works
+beside proof development, tactics writing or documentation.
+
+\section{Building a toplevel extended with user tactics}
+\label{Coqmktop}\index{Coqmktop@{\tt coqmktop}}
+
+The native-code version of \Coq\ cannot dynamically load user tactics
+using Objective Caml code. It is possible to build a toplevel of \Coq,
+with Objective Caml code statically linked, with the tool {\tt
+  coqmktop}.
+
+For example, one can build a native-code \Coq\ toplevel extended with a tactic
+which source is in {\tt tactic.ml} with the command 
+\begin{verbatim}
+     % coqmktop -opt -o mytop.out tactic.cmx
+\end{verbatim}
+where {\tt tactic.ml} has been compiled with the native-code
+compiler {\tt ocamlopt}. This command generates an executable
+called {\tt mytop.out}. To use this executable to compile your \Coq\
+files, use {\tt coqc -image mytop.out}.
+
+A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}),
+which can be generated by {\tt coqmktop -opt -o coqopt.opt}.
+
+
+\paragraph{Application: how to use the Objective Caml debugger with Coq.}
+\index{Debugger}
+
+One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in
+order to debug your tactics with the Objective Caml debugger.
+You need to have configured and compiled \Coq\ for debugging
+(see the file \texttt{INSTALL} included in the distribution).
+Then, you must compile the Caml modules of your tactic with the
+option \texttt{-g} (with the bytecode compiler) and build a stand-alone
+bytecode toplevel with the following command:
+
+\begin{quotation}
+\texttt{\% coqmktop -g -o coq-debug}~\emph{<your \texttt{.cmo} files>}
+\end{quotation}
+
+
+To launch the \ocaml\ debugger with the image you need to execute it in
+an environment which correctly sets the \texttt{COQLIB} variable.
+Moreover, you have to indicate the directories in which
+\texttt{ocamldebug} should search for Caml modules.
+
+A possible solution is to use a wrapper around \texttt{ocamldebug}
+which detects the executables containing the word \texttt{coq}. In
+this case, the debugger is called with the required additional
+arguments. In other cases, the debugger is simply called without additional
+arguments. Such a wrapper can be found in the \texttt{dev/}
+subdirectory of the sources. 
+
+\section{Modules dependencies}\label{Dependencies}\index{Dependencies}
+  \index{Coqdep@{\tt coqdep}}
+
+In order to compute modules dependencies (so to use {\tt make}),
+\Coq\ comes with an appropriate tool, {\tt coqdep}.
+
+{\tt coqdep} computes inter-module dependencies for \Coq\ and
+\ocaml\ programs, and prints the dependencies on the standard
+output in a format readable by make.  When a directory is given as
+argument, it is recursively looked at.
+
+Dependencies of \Coq\ modules are computed by looking at {\tt Require}
+commands ({\tt Require}, {\tt Requi\-re Export}, {\tt Require Import},
+{\tt Require Implementation}), but also at the command {\tt Declare ML Module}.
+
+Dependencies of \ocaml\ modules are computed by looking at
+\verb!open! commands and the dot notation {\em module.value}. However,
+this is done approximatively and you are advised to use {\tt ocamldep}
+instead for the \ocaml\ modules dependencies.
+
+See the man page of {\tt coqdep} for more details and options.
+
+
+\section{Creating a {\tt Makefile} for \Coq\ modules}
+\label{Makefile}
+\index{Makefile@{\tt Makefile}}
+\index{CoqMakefile@{\tt coq\_Makefile}}
+
+When a proof development becomes large and is split into several files,
+it becomes crucial to use a tool like {\tt make} to compile \Coq\
+modules.
+
+The writing of a generic and complete {\tt Makefile} may be a tedious work
+and that's why \Coq\ provides a tool to automate its creation,
+{\tt coq\_makefile}. Given the files to compile, the command {\tt
+coq\_makefile} prints a 
+{\tt Makefile} on the standard output. So one has just to run the
+command:
+
+\begin{quotation}
+\texttt{\% coq\_makefile} {\em file$_1$.v \dots\ file$_n$.v} \texttt{> Makefile}
+\end{quotation}
+
+The resulted {\tt Makefile} has a target {\tt depend} which computes the
+dependencies and puts them in a separate file {\tt .depend}, which is
+included by the {\tt Makefile}. 
+Therefore, you should create such a file before the first invocation
+of make. You can for instance use the command 
+
+\begin{quotation}
+\texttt{\% touch .depend}
+\end{quotation}
+
+Then, to initialize or update the modules dependencies, type in:
+
+\begin{quotation}
+\texttt{\% make depend}
+\end{quotation}
+
+There is a target {\tt all} to compile all the files {\em file$_1$
+\dots\ file$_n$}, and a generic target to produce a {\tt .vo} file from
+the corresponding {\tt .v} file (so you can do {\tt make} {\em file}{\tt.vo}
+to compile the file {\em file}{\tt.v}).
+
+{\tt coq\_makefile} can also handle the case of ML files and
+subdirectories. For more options type
+
+\begin{quotation}
+\texttt{\% coq\_makefile --help}
+\end{quotation}
+
+\Warning To compile a project containing \ocaml{} files you must keep
+the sources of \Coq{} somewhere and have an environment variable named
+\texttt{COQTOP} that points to that directory.
+
+% \section{{\sf Coq\_SearchIsos}: information retrieval in a \Coq\ proofs
+% library}
+% \label{coqsearchisos}
+% \index{Coq\_SearchIsos@{\sf Coq\_SearchIsos}}
+
+% In the \Coq\ distribution, there is also a separated and independent tool,
+% called {\sf Coq\_SearchIsos}, which allows the search in accordance with {\tt
+% SearchIsos}\index{SearchIsos@{\tt SearchIsos}} (see section~\ref{searchisos})
+% in a \Coq\ proofs library. More precisely, this program begins, once launched
+% by {\tt coqtop -searchisos}\index{coqtopsearchisos@{\tt
+% coqtop -searchisos}}, loading lightly (by using specifications functions)
+% all the \Coq\ objects files ({\tt .vo}) accessible by the {\tt LoadPath} (see
+% section~\ref{loadpath}). Next, a prompt appears and four commands are then
+% available:
+
+% \begin{description}
+% \item [{\tt SearchIsos}]\ \\
+%   Scans the fixed context.
+% \item [{\tt Time}]\index{Time@{\tt Time}}\ \\
+%   Turns on the Time Search Display mode (see section~\ref{time}).
+% \item [{\tt Untime}]\index{Untime@{\tt Untime}}\ \\
+%   Turns off the Time Search Display mode (see section~\ref{time}).
+% \item [{\tt Quit}]\index{Quit@{\tt Quit}}\ \\
+%   Ends the {\tt coqtop -searchisos} session.
+% \end{description}
+
+% When running {\tt coqtop -searchisos} you can use the two options:
+
+% \begin{description}
+% \item[{\tt -opt}]\ \\
+%   Runs the native-code version of {\sf Coq\_SearchIsos}.
+
+% \item[{\tt -image} {\em file}]\ \\
+%   This option sets the binary image to be used to be {\em file}
+%   instead of the standard one. Not of general use.
+% \end{description}
+
+
+\section{Documenting \Coq\ files with coqdoc}
+\label{coqdoc}
+\index{Coqdoc@{\sf coqdoc}}
+
+\input{./coqdoc}
+
+\section{Exporting \Coq\ theories to XML}
+
+\input{./Helm}
+
+\section{Embedded \Coq\ phrases inside \LaTeX\ documents}\label{Latex}
+  \index{Coqtex@{\tt coq-tex}}\index{Latex@{\LaTeX}}
+
+When writing a documentation about a proof development, one may want
+to insert \Coq\ phrases inside a \LaTeX\ document, possibly together with
+the corresponding answers of the system. We provide a
+mechanical way to process such \Coq\ phrases embedded in \LaTeX\ files: the
+{\tt coq-tex} filter.  This filter extracts Coq phrases embedded in
+LaTeX files, evaluates them, and insert the outcome of the evaluation
+after each phrase.
+
+Starting with a file {\em file}{\tt.tex} containing \Coq\ phrases,
+the {\tt coq-tex} filter produces a file named {\em file}{\tt.v.tex} with
+the \Coq\ outcome. 
+
+There are options to produce the \Coq\ parts in smaller font, italic,
+between horizontal rules, etc.
+See the man page of {\tt coq-tex} for more details.
+
+\medskip\noindent {\bf Remark.} This Reference Manual and the Tutorial
+have been completely produced with {\tt coq-tex}.
+
+
+\section{\Coq\ and \emacs}\label{Emacs}\index{Emacs}
+
+\subsection{The \Coq\ Emacs mode}
+
+\Coq\ comes with a Major mode for \emacs, {\tt coq.el}. This mode provides
+syntax highlighting (assuming your \emacs\ library provides
+{\tt hilit19.el}) and also a rudimentary indentation facility
+in the style of the Caml \emacs\ mode.
+
+Add the following lines to your \verb!.emacs! file:
+
+\begin{verbatim}
+  (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
+  (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
+\end{verbatim}
+
+The \Coq\ major mode is triggered by visiting a file with extension {\tt .v},
+or manually with the command \verb!M-x coq-mode!.
+It gives you the correct syntax table for
+the \Coq\ language, and also a rudimentary indentation facility:
+\begin{itemize}
+  \item pressing {\sc Tab} at the beginning of a line indents the line like
+    the line above;
+
+  \item extra {\sc Tab}s increase the indentation level
+    (by 2 spaces by default);
+
+  \item M-{\sc Tab} decreases the indentation level.
+\end{itemize}
+
+An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also
+included in the distribution, in file \texttt{coq-inferior.el}.
+Instructions to use it are contained in this file.
+
+\subsection{Proof General}\index{Proof General}
+
+Proof General is a generic interface for proof assistants based on
+Emacs (or XEmacs). The main idea is that the \Coq\ commands you are
+editing are sent to a \Coq\ toplevel running behind Emacs and the
+answers of the system automatically inserted into other Emacs buffers. 
+Thus you don't need to copy-paste the \Coq\ material from your files
+to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
+files. 
+
+Proof General is developped and distributed independently of the
+system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
+
+
+\section{Module specification}\label{gallina}\index{Gallina@{\tt gallina}}
+
+Given a \Coq\ vernacular file, the {\tt gallina} filter extracts its
+specification (inductive types declarations, definitions, type of
+lemmas and theorems), removing the proofs parts of the file. The \Coq\
+file {\em file}{\tt.v} gives birth to the specification file
+{\em file}{\tt.g} (where the suffix {\tt.g} stands for \gallina).
+
+See the man page of {\tt gallina} for more details and options.
+
+
+\section{Man pages}\label{ManPages}\index{Man pages}
+
+There are man pages for the commands {\tt coqdep}, {\tt gallina} and
+{\tt coq-tex}. Man pages are installed at installation time
+(see installation instructions in file {\tt INSTALL}, step 6).
+
+%BEGIN LATEX
+\RefManCutCommand{ENDREFMAN=\thepage}
+%END LATEX
+
+% $Id: RefMan-uti.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: