Chapter 15 Utilities

The distribution provides utilities to simplify some tedious works beside proof development, tactics writing or documentation.

15.1 Building a toplevel extended with user tactics

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 coqmktop.

For example, one can build a native-code Coq toplevel extended with a tactic which source is in tactic.ml with the command

     % coqmktop -opt -o mytop.out tactic.cmx

where tactic.ml has been compiled with the native-code compiler ocamlopt. This command generates an executable called mytop.out. To use this executable to compile your Coq files, use coqc -image mytop.out.

A basic example is the native-code version of Coq (coqtop.opt), which can be generated by coqmktop -opt -o coqopt.opt.

Application: how to use the Objective Caml debugger with Coq.

One useful application of 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 INSTALL included in the distribution). Then, you must compile the Caml modules of your tactic with the option -g (with the bytecode compiler) and build a stand-alone bytecode toplevel with the following command:

% coqmktop -g -o coq-debug <your .cmo files>

To launch the Objective Caml debugger with the image you need to execute it in an environment which correctly sets the COQLIB variable. Moreover, you have to indicate the directories in which ocamldebug should search for Caml modules.

A possible solution is to use a wrapper around ocamldebug which detects the executables containing the word 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 dev/ subdirectory of the sources.

15.2 Modules dependencies

In order to compute modules dependencies (so to use make), Coq comes with an appropriate tool, coqdep.

coqdep computes inter-module dependencies for Coq and Objective Caml 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 Require commands (Require, Require Export, Require Import, but also at the command Declare ML Module.

Dependencies of Objective Caml modules are computed by looking at open commands and the dot notation module.value. However, this is done approximately and you are advised to use ocamldep instead for the Objective Caml modules dependencies.

See the man page of coqdep for more details and options.

15.3 Creating a Makefile for Coq modules

A project is a proof development split into several files, possibly including the sources of some Objective Caml plugins, that are located (in various sub-directories of) a certain directory. The coq_makefile command allows to generate generic and complete 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.

_CoqProject file as an argument to coq_Makefile.

In particular, a _CoqProject file contains the relevant arguments to be passed to the coq_makefile makefile generator using for instance the command:

% coq_makefile -f _CoqProject -o Makefile

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

The following command generates a minimal example of _CoqProject file:

% ( echo "-R . MyFancyLib" ; find . -name "*.v" -print ) > _CoqProject

when executed at the root of the directory containing the project. Here the _CoqProject lists all the .v files that are present in the current directory and its sub-directories. But no plugin sources is listed. If a Makefile is generated from this _CoqProject, the command make install will install the compiled project in a sub-directory MyFancyLib of the user-contrib directory (of the user’s Coq libraries location). This sub-directory is created if it does not already exist.

_CoqProject file as a configuration for IDEs.

A _CoqProject file can also be used to configure the options of the 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 ≥ 4.3pre) support configuration via _CoqProject files.

Remarks.

Every Coq files must use a .v file extension. The Objective Caml modules must use a .ml4 file extension if they require camlp preprocessing (and in .ml otherwise). The Objective Caml module signatures, library description and packing files must use respectively .mli, .mllib and .mlpack file extension.
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 Makefile.
The phony targets all and clean recursively call their target in every sub-directory.
-R and -Q options are for Coq files, -I for Objective Caml ones. A same directory can be passed to both nature of options, in the same _CoqProject.
Using -R or -Q is the appropriate way to obtain both a correct logical path and a correct installation location to the libraries of a given project.
Dependencies on external libraries to the project must be declared with care. If in the _CoqProject file an external library foo is passed to a -Q option, like in -Q foo, the subsequent make clean command can erase foo. It is hence safer to customize the COQPATH variable (see 14.3.2), to include the location of the required external libraries.
Using -extra-phony with no command adds extra dependencies on already defined rules. For example the following skeleton appends “something” to the install rule:
-extra-phony "install" "install-my-stuff" "" -extra-phony "install-my-stuff" "" "something"

15.4 Documenting Coq files with coqdoc

coqdoc is a documentation tool for the proof assistant Coq, similar to javadoc or ocamldoc. The task of coqdoc is

to produce a nice L^AT_EX and/or HTML document from the Coq sources, readable for a human and not only for the proof assistant;
to help the user navigating in his own (or third-party) sources.

15.4.1 Principles

Documentation is inserted into Coq files as 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 (**, followed by a space, and ends with the pending *). The documentation format is inspired by Todd A. Coram’s 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”.

Coq material inside documentation.

Coq material is quoted between the delimiters [ and ]. Square brackets may be nested, the inner ones being understood as being part of the quoted code (thus you can quote a term like fun x => u by writing [fun x => u]). Inside quotations, the code is pretty-printed in the same way as it is in code parts.

Pre-formatted vernacular is enclosed by [[ and ]]. The former must be followed by a newline and the latter must follow a newline.

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:

(** printing token %...L^AT_EX...% #...HTML...# *)

(** printing token $...L^AT_EX math...$ #...HTML...# *)

It gives the L^AT_EX and HTML texts to be produced for the given Coq token. One of the L^AT_EX or HTML text may be omitted, causing the default pretty-printing to be used for this token.

The printing for one token can be removed with

(** remove printing token *)

Initially, the pretty-printing table contains the following mapping:

`->`	→	`<-`	←	`*`	×
`<=`	≤	`>=`	≥	`=>`	⇒
`<>`	≠	`<->`	↔	`\|-`	⊢
`\/`	∨	`/\`	∧	`~`	¬

Any of these can be overwritten or suppressed using the printing commands.

Important note: the recognition of tokens is done by a (ocaml)lex automaton and thus applies the longest-match rule. For instance, ->~ is recognized as a single token, where Coq sees two tokens. It is the responsibility of the user to insert space between tokens or to give pretty-printing rules for the possible combinations, e.g.

(** printing ->~ %\ensuremath{\rightarrow\lnot}% *)

Sections.

Sections are introduced by 1 to 4 leading stars (i.e. at the beginning of the line) followed by a space. One star is a section, two stars a sub-section, etc. The section title is given on the remaining of the line. Example:

    (** * Well-founded relations
  
        In this section, we introduce...  *)

Lists.

List items are introduced by a leading dash. coqdoc uses whitespace to determine the depth of a new list item and which text belongs in which list items. A list ends when a line of text starts at or before the level of indenting of the list’s dash. A list item’s dash must always be the first non-space character on its line (so, in particular, a list can not begin on the first line of a comment - start it on the second line instead).

Example:

     We go by induction on [n]:
     - If [n] is 0...
     - If [n] is [S n'] we require...

       two paragraphs of reasoning, and two subcases:

       - In the first case...
       - In the second case...

     So the theorem holds.

Rules.

More than 4 leading dashes produce a horizontal rule.

Emphasis.

Text can be italicized by placing it in underscores. A non-identifier character must precede the leading underscore and follow the trailing underscore, so that uses of underscores in names aren’t mistaken for emphasis. Usually, these are spaces or punctuation.

    This sentence contains some _emphasized text_.

Escaping to L^AT_EX and HTML.

Pure L^AT_EX or HTML material can be inserted using the following escape sequences:

$...LaTeX stuff...$ inserts some L^AT_EX material in math mode. Simply discarded in HTML output.
%...LaTeX stuff...% inserts some L^AT_EX material. Simply discarded in HTML output.
#...HTML stuff...# inserts some HTML material. Simply discarded in L^AT_EX output.

Note: to simply output the characters $, % and # and escaping their escaping role, these characters must be doubled.

Verbatim.

Verbatim material is introduced by a leading << and closed by >> at the beginning of a line. Example:

Here is the corresponding caml code:
<<
  let rec fact n = 
    if n <= 1 then 1 else n * fact (n-1)
>>

Hyperlinks.

Hyperlinks can be inserted into the HTML output, so that any identifier is linked to the place of its definition.

coqc file.v automatically dumps localization information in file.glob or appends it to a file specified using option --dump-glob file. Take care of erasing this global file, if any, when starting the whole compilation process.

Then invoke coqdoc or coqdoc --glob-from file to tell coqdoc to look for name resolutions into the file file (it will look in file.glob by default).

Identifiers from the Coq standard library are linked to the Coq web site at http://coq.inria.fr/library/. This behavior can be changed using command line options --no-externals and --coqlib; see below.

Hiding / Showing parts of the source.

Some parts of the source can be hidden using command line options -g and -l (see below), or using such comments:

(* begin hide *)
some Coq material
(* end hide *)

Conversely, some parts of the source which would be hidden can be shown using such comments:

(* begin show *)
some Coq material
(* end show *)

The latter cannot be used around some inner parts of a proof, but can be used around a whole proof.

15.4.2 Usage

coqdoc is invoked on a shell command line as follows:

coqdoc <options and files>

Any command line argument which is not an option is considered to be a file (even if it starts with a -). Coq files are identified by the suffixes .v and .g and L^AT_EX files by the suffix .tex.

HTML output: This is the default output. One HTML file is created for each Coq file given on the command line, together with a file index.html (unless option -no-index is passed). The HTML pages use a style sheet named style.css. Such a file is distributed with coqdoc.
L^AT_EX output: A single L^AT_EX file is created, on standard output. It can be redirected to a file with option -o. The order of files on the command line is kept in the final document. L^AT_EX files given on the command line are copied ‘as is’ in the final document . DVI and PostScript can be produced directly with the options -dvi and -ps respectively.
T_EXmacs output: To translate the input files to T_EXmacs format, to be used by the T_EXmacs Coq interface.

Command line options

Overall options

--html: Select a HTML output.
--latex: Select a L^AT_EX output.
--dvi: Select a DVI output.
--ps: Select a PostScript output.
--texmacs: Select a T_EXmacs output.
--stdout: Write output to stdout.
-o file, --output file: Redirect the output into the file ‘file’ (meaningless with -html).
-d dir, --directory dir: Output files into directory ‘dir’ instead of current directory (option -d does not change the filename specified with option -o, if any).
--body-only: Suppress the header and trailer of the final document. Thus, you can insert the resulting document into a larger one.
-p string, --preamble string: Insert some material in the L^AT_EX preamble, right before \begin{document} (meaningless with -html).
--vernac-file file, --tex-file file: Considers the file ‘file’ respectively as a .v (or .g) file or a .tex file.
--files-from file: Read file names to process in file ‘file’ as if they were given on the command line. Useful for program sources split up into several directories.
-q, --quiet: Be quiet. Do not print anything except errors.
-h, --help: Give a short summary of the options and exit.
-v, --version: Print the version and exit.

Index options

Default behavior is to build an index, for the HTML output only, into index.html.

--no-index: Do not output the index.
--multi-index: Generate one page for each category and each letter in the index, together with a top page index.html.
--index string: Make the filename of the index string instead of “index”. Useful since “index.html” is special.

Table of contents option

-toc, --table-of-contents: Insert a table of contents. For a L^AT_EX output, it inserts a \tableofcontents at the beginning of the document. For a HTML output, it builds a table of contents into toc.html.
--toc-depth int: Only include headers up to depth int in the table of contents.

Hyperlinks options

--glob-from file

Make references using Coq globalizations from file file. (Such globalizations are obtained with Coq option -dump-glob).

--no-externals

Do not insert links to the Coq standard library.

--external url coqdir

Use given URL for linking references whose name starts with prefix coqdir.

--coqlib url

Set base URL for the Coq standard library (default is http://coq.inria.fr/library/). This is equivalent to --external url Coq.

-R dir coqdir

Map physical directory dir to Coq logical directory coqdir (similarly to Coq option -R).

Note: option -R only has effect on the files following it on the command line, so you will probably need to put this option first.

Title options

-s , --short

Do not insert titles for the files. The default behavior is to insert a title like “Library Foo” for each file.

--lib-name string

Print “string Foo” instead of “Library Foo” in titles. For example “Chapter” and “Module” are reasonable choices.

--no-lib-name

Print just “Foo” instead of “Library Foo” in titles.

--lib-subtitles

Look for library subtitles. When enabled, the beginning of each file is checked for a comment of the form:

(** * ModuleName : text *)

where ModuleName must be the name of the file. If it is present, the text is used as a subtitle for the module in appropriate places.

-t string, --title string

Set the document title.

Contents options

-g, --gallina

Do not print proofs.

-l, --light

Light mode. Suppress proofs (as with -g) and the following commands:

[Recursive] Tactic Definition
Hint / Hints
Require
Transparent / Opaque
Implicit Argument / Implicits
Section / Variable / Hypothesis / End

The behavior of options -g and -l can be locally overridden using the (* begin show *) … (* end show *) environment (see above).

There are a few options to drive the parsing of comments:

--parse-comments: Parses regular comments delimited by (* and *) as well. They are typeset inline.
--plain-comments: Do not interpret comments, simply copy them as plain-text.
--interpolate: Use the globalization information to typeset identifiers appearing in Coq escapings inside comments.

Language options

Default behavior is to assume ASCII 7 bits input files.

-latin1, --latin1

Select ISO-8859-1 input files. It is equivalent to --inputenc latin1 --charset iso-8859-1.

-utf8, --utf8

Set --inputenc utf8x for L^AT_EX output and --charset utf-8 for HTML output. Also use Unicode replacements for a couple of standard plain ASCII notations such as → for -> and ∀ for forall. L^AT_EX UTF-8 support can be found at http://www.ctan.org/pkg/unicode.

For the interpretation of Unicode characters by L^AT_EX, extra packages which coqdoc does not provide by default might be required, such as textgreek for some Greek letters or stmaryrd for some mathematical symbols. If a Unicode character is missing an interpretation in the utf8x input encoding, add \DeclareUnicodeCharacter{code}{latex-interpretation}. Packages and declarations can be added with option -p.

--inputenc string

Give a L^AT_EX input encoding, as an option to L^AT_EX package inputenc.

--charset string

Specify the HTML character set, to be inserted in the HTML header.

15.4.3 The coqdoc L^AT_EX style file

In case you choose to produce a document without the default L^AT_EX preamble (by using option --no-preamble), then you must insert into your own preamble the command

\usepackage{coqdoc}

The package optionally takes the argument [color] to typeset identifiers with colors (this requires the xcolor package).

Then you may alter the rendering of the document by redefining some macros:

coqdockw, 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

     \renewcommand{\coqdockw}[1]{\textsl{#1}}

anywhere between \usepackage{coqdoc} and \begin{document}.

coqdocmodule

One-argument macro for typesetting the title of a .v file. Default is

\newcommand{\coqdocmodule}[1]{\section*{Module #1}}

and you may redefine it using \renewcommand.

15.5 Embedded Coq phrases inside L^AT_EX documents

When writing a documentation about a proof development, one may want to insert Coq phrases inside a L^AT_EX document, possibly together with the corresponding answers of the system. We provide a mechanical way to process such Coq phrases embedded in L^AT_EX files: the 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 file.tex containing Coq phrases, the coq-tex filter produces a file named file.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 coq-tex for more details.

Remark. This Reference Manual and the Tutorial have been completely produced with coq-tex.

15.6 Coq and GNU Emacs

15.6.1 The Coq Emacs mode

Coq comes with a Major mode for GNU Emacs, gallina.el. This mode provides syntax highlighting and also a rudimentary indentation facility in the style of the Caml GNU Emacs mode.

Add the following lines to your .emacs file:

  (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
  (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)

The Coq major mode is triggered by visiting a file with extension .v, or manually with the command M-x coq-mode. It gives you the correct syntax table for the Coq language, and also a rudimentary indentation facility:

pressing Tab at the beginning of a line indents the line like the line above;
extra Tabs increase the indentation level (by 2 spaces by default);
M-Tab decreases the indentation level.

An inferior mode to run Coq under Emacs, by Marco Maggesi, is also included in the distribution, in file coq-inferior.el. Instructions to use it are contained in this file.

15.6.2 Proof General

Proof General 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.

Proof General is developed and distributed independently of the system Coq. It is freely available at proofgeneral.inf.ed.ac.uk.

15.7 Module specification

Given a Coq vernacular file, the gallina filter extracts its specification (inductive types declarations, definitions, type of lemmas and theorems), removing the proofs parts of the file. The Coq file file.v gives birth to the specification file file.g (where the suffix .g stands for Gallina).

See the man page of gallina for more details and options.

15.8 Man pages

There are man pages for the commands coqdep, gallina and coq-tex. Man pages are installed at installation time (see installation instructions in file INSTALL, step 6).