path: root/doc/refman/RefMan-uti.tex

\chapter[Utilities]{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]{Building a toplevel extended with user tactics\label{Coqmktop}\ttindex{coqmktop}}

The native-code version of \Coq\ cannot dynamically load user tactics
using {\ocaml} code. It is possible to build a toplevel of \Coq,
with {\ocaml} 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 {\ocaml} debugger with Coq.]{Application: how to use the {\ocaml} 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 {\ocaml} 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]{Modules dependencies\label{Dependencies}\index{Dependencies}
  \ttindex{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},
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 approximately 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]{Creating a {\tt Makefile} for \Coq\ modules\label{Makefile}
\ttindex{Makefile}
\ttindex{coq\_Makefile}}

\paragraph{\_CoqProject}
When a proof development becomes a larger project, split into several
files or containing {\ocaml} plugins, files share common options that
must be specified to all the executables used during the development
of the project. It is therefore convenient to write a file that could
be read all the components (the IDE, the compiler, etc.) that
specify all the files and the common options of the project.

An attempt to set up a format to write project files has been made
from the command line option of the {\Coq} makefile generator
\texttt{coq\_makefile}. It is described by \texttt{\% coq\_makefile
  --help}. The default name for the project file understood by
\texttt{coq\_makefile}, \texttt{coqide} and \texttt{Proof General} is
\texttt{\_CoqProject}.

A minimal usable project file can probably be obtained by the
invocation
\begin{quotation}
\texttt{\% \{ echo '-R .} \textit{MyFancyLib} \texttt{' ; find . -name
  '*.v' -print \} > \_CoqProject}
\end{quotation}

While customizing a project file, mind the following requirements:
\begin{itemize}
\item {\Coq} files must end in \texttt{.v}, {\ocaml} modules in
  \texttt{.ml4} if they require camlp preprocessing (and in
  \texttt{.ml} otherwise), {\ocaml} module signatures, library
  description and packing files respectively in \texttt{.mli},
  \texttt{.mllib} and \texttt{.mlpack}.

Any other argument that is not a valid option will be considered as a
subdirectory. A specified subdirectory must have an inner
\texttt{Makefile}. The phony targets \texttt{all} and \texttt{clean}
will recursively call this target in all the subdirectories.

\item \texttt{-R} and \texttt{-Q} options are for {\Coq}, \texttt{-I}
  for {\ocaml}. The same directory may be ``included'' by both.

  Using \texttt{-R} or \texttt{-Q} gives a correct logical path
  and a correct installation location to your coq files.
\item dependency on an external library must not be declared using a
  \texttt{-Q \dots} in the \texttt{\_CoqProject} to include it in the
  path, as the \textit{make clean} command would erase it! Instead,
  install your dependency in a place automatically included by
  {\Coq}. You can take advantage of the \texttt{COQPATH} variable
  (see \ref{envars}) without installation if necessary.
\item Use \texttt{-extra-phony} with no command to add an extra
  dependencies on already defined rules. For example the following
  skeleton appends something to the \texttt{install} rule:
\begin{quotation}
\texttt{-extra-phony "install" "install-my-stuff" ""
  -extra-phony "install-my-stuff" "" "something"}
\end{quotation}
\end{itemize}

\paragraph{Coq\_makefile}
The writing of a generic and complete \texttt{Makefile} may be tedious
work and that's why {\Coq} provides a tool to automate its creation
from the \texttt{\_CoqProject} file, \texttt{coq\_makefile}.

Use
\begin{quotation}
\texttt{coq\_makefile -f \_CoqProject -o Makefile}
\end{quotation}
to generate a \texttt{Makefile} the first time. \texttt{Makefile} will be
automatically regenerated when \texttt{\_CoqProject} is updated afterward.

\section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc}
\ttindex{coqdoc}}

\input{./coqdoc}

\section[Embedded \Coq\ phrases inside \LaTeX\ documents]{Embedded \Coq\ phrases inside \LaTeX\ documents\label{Latex}
  \ttindex{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]{\Coq\ and \emacs\label{Emacs}\index{Emacs}}

\subsection{The \Coq\ Emacs mode}

\Coq\ comes with a Major mode for \emacs, {\tt gallina.el}. This mode provides
syntax highlighting
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 "gallina" "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[{\ProofGeneral}]{{\ProofGeneral}\index{Proof General@{\ProofGeneral}}}

{\ProofGeneral} is a generic interface for proof assistants based on
Emacs. 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. 

{\ProofGeneral} is developed and distributed independently of the
system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.


\section[Module specification]{Module specification\label{gallina}\ttindex{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]{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

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: