1 files changed, 292 insertions, 0 deletions
diff --git a/doc/RefMan-uti.tex b/doc/RefMan-uti.tex
new file mode 100755
index 000000000..cd266d4cf
--- /dev/null
+++ b/doc/RefMan-uti.tex
@@ -0,0 +1,292 @@
+\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 image of \Coq\ 
+called {\tt mytop.out}. One can run this new toplevel with the command
+{\tt coqtop -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.out}.
+
+See the man page of {\tt coqmktop} for more details and options.
+
+
+\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{tools/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}.
+
+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{DoMakefile@{\tt do\_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 seem tedious
+and that's why \Coq\ provides a tool to automate its creation,
+{\tt do\_Makefile}. Given the files to compile, the command {\tt
+do\_Makefile} prints a 
+{\tt Makefile} on the standard output. So one has just to run the
+command:
+
+\begin{quotation}
+\texttt{\% do\_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 do\_Makefile} can also handle the case of ML files and
+subdirectories. For more options type
+
+\begin{quotation}
+\texttt{\% do\_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{\Coq\ and \LaTeX}\label{Latex}
+  \index{Latex@{\LaTeX}}
+
+\subsection{Embedded \Coq\ phrases inside \LaTeX\ documents}
+  \index{Coqtex@{\tt coq-tex}}
+
+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}.
+
+
+\subsection{Pretty printing \Coq\ listings with \LaTeX}
+  \index{Coq2latex@{\tt coq2latex}}
+
+\verb!coq2latex! is a tool for printing \Coq\ listings using \LaTeX\ : 
+keywords are printed in bold face, comments in italic, some tokens
+are printed in a nicer way (\verb!->! becomes $\rightarrow$, etc.)
+and indentations are kept at the beginning of lines.
+Line numbers are printed in the right margin, every 10 lines.
+
+In regular mode, the command 
+
+\begin{flushleft}
+~~~~~\texttt{\% coq2latex {\rm\em file}}
+\end{flushleft}
+
+\noindent produces a \LaTeX\ file which is sent to the \verb!latex! command,
+and the result to the \verb!dvips! command. 
+
+It is also possible to  get the \LaTeX\  file, DVI file or  PostSCript
+file,  on the standard output or  in a file.  See the man page of {\tt
+coq2latex} for more details and options.
+
+
+\section{\Coq\ and HTML}\label{Html}\index{HTML}
+  \index{Coq2html@{\tt coq2html}}
+
+As for \LaTeX, it is also possible to pretty print \Coq\ listing with
+HTML. The document looks like the \LaTeX\ one, with links added when
+possible : links to other \Coq\ modules in {\tt Require} commands, and
+links to identifiers defined in other modules (when they are found in a
+path given with {\tt -I} options).
+
+In regular mode, the command 
+
+\begin{flushleft}
+~~~~~\texttt{\% coq2html {\rm\em file}.v}
+\end{flushleft}
+
+\noindent produces an HTML document {{\em file}{\tt .html}}.
+
+See the man page of {\tt coq2html} for more details and options.
+
+
+\section{\Coq\ and \emacs}\label{Emacs}\index{Emacs}
+
+\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}
+
+
+\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 {\sf 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 coqtop}, {\tt coqc}, {\tt coqmktop},
+{\tt coqdep}, {\tt gallina},\linebreak{} {\tt coq-tex}, {\tt
+coq2latex} and {\tt coq2html}. Man pages are installed at installation time
+(see installation instructions in file {\tt INSTALL}, step 6).
+
+\addtocontents{sh}{ENDREFMAN=\thepage}
+
+% $Id$
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: