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}
\ttindex{\_CoqProject}}

A project is a proof development split into several files, possibly
including the sources of some {\ocaml} plugins, that are located (in
various sub-directories of) a certain directory. The
\texttt{coq\_makefile} command allows to generate generic and complete
\texttt{Makefile} files, that can be used to compile the different
components of the project. A \_CoqProject file
specifies both the list of target files relevant to the project
and the common options that should be passed to each executable at
compilation times, for the IDE, etc.

\paragraph{\_CoqProject file as an argument to  coq\_Makefile.}
In particular, a \_CoqProject file contains the relevant
arguments to be passed to the \texttt{coq\_makefile} makefile
generator using for instance the command:

\begin{quotation}
\texttt{\% coq\_makefile -f \_CoqProject -o Makefile}
\end{quotation}

This command generates a file \texttt{Makefile} that can be used to
compile all the sources of the current project. It follows the
syntax described by the output of \texttt{\% coq\_makefile -{}-help}.
Once the \texttt{Makefile} file has been generated a first time, it
can be used by the \texttt{make} command to compile part or all of
the project. Note that once it has been generated once, as soon as
\texttt{\_CoqProject} file is updated, the \texttt{Makefile} file is
automatically regenerated by an invocation of \texttt{make}.

The following command generates a minimal example of
\texttt{\_CoqProject} file:
\begin{quotation}
\texttt{\% ( echo "-R .\ }\textit{MyFancyLib}\texttt{" ; find .\ -name
  "*.v" -print ) > \_CoqProject}
\end{quotation}
when executed at the root of the directory containing the
project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files
that are present in the current directory and its sub-directories. But no
plugin sources is listed. If a \texttt{Makefile} is generated from
this \texttt{\_CoqProject}, the command \texttt{make install} will
install the compiled project in a sub-directory \texttt{MyFancyLib} of
the \texttt{user-contrib} directory  (of the user's {\Coq} libraries
location). This sub-directory is created if it does not already exist.

\paragraph{\_CoqProject file as a configuration for IDEs.}

A \texttt{\_CoqProject} file can also be used to configure the options
of the \texttt{coqtop} process executed by a user interface. This
allows to import the libraries of the project under a correct name,
both as a developer of the project, working in the directory
containing its sources, and as a user, using the project after
the installation of its libraries. Currently, both \CoqIDE{} and Proof
General (version $\geq$ 4.3pre) support configuration via
\texttt{\_CoqProject} files.

\paragraph{Remarks.}

\begin{itemize}
\item Every {\Coq} files must use a \texttt{.v} file extension.
 The {\ocaml} modules must use a \texttt{.ml4} file extension
 if they require camlp preprocessing (and in \texttt{.ml} otherwise).
 The {\ocaml} module signatures, library
 description and packing files must use respectively \texttt{.mli},
 \texttt{.mllib} and \texttt{.mlpack} file extension.

\item Any argument that is not a valid option is considered as a
  sub-directory. Any sub-directory specified in the list of targets must
  itself contain a \texttt{Makefile}.

\item The phony targets \texttt{all} and \texttt{clean} recursively
  call their target in every sub-directory.

\item \texttt{-R} and \texttt{-Q} options are for {\Coq} files, \texttt{-I}
  for {\ocaml} ones. A same directory can be passed to both nature of
  options, in the same \texttt{\_CoqProject}.

\item Using \texttt{-R} or \texttt{-Q} is the appropriate way to
  obtain both a correct logical path and a correct installation location to
  the libraries of a given project.

\item Dependencies on external libraries to the project must be
  declared with care. If in the \texttt{\_CoqProject} file an external
  library \texttt{foo} is passed to a \texttt{-Q} option, like in
  \texttt{-Q foo}, the subsequent \textit{make clean} command can
  erase \textit{foo}. It is hence safer to customize the
  \texttt{COQPATH} variable (see \ref{envars}), to include the
  location of the required external libraries.

\item Using \texttt{-extra-phony} with no command adds 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}


\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!https://proofgeneral.github.io/!.


\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: