
# Utilities¶

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

## Using Coq as a library¶

In previous versions, coqmktop was used to build custom toplevels - for example for better debugging or custom static linking. Nowadays, the preferred method is to use ocamlfind.

The most basic custom toplevel is built using:

% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \
-package coq.toplevel \
toplevel/coqtop\_bin.ml -o my\_toplevel.native


For example, to statically link Ltac, you can just do:

% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \
-package coq.toplevel -package coq.ltac \
toplevel/coqtop\_bin.ml -o my\_toplevel.native


and similarly for other plugins.

## Building a Coq project with coq_makefile¶

The majority of Coq projects are very similar: a collection of .v files and eventually some .ml ones (a Coq plugin). The main piece of metadata needed in order to build the project are the command line options to coqc (e.g. -R, -I, see also: section By command line options). Collecting the list of files and options is the job of the _CoqProject file.

A simple example of a _CoqProject file follows:

-R theories/ MyCode
theories/foo.v
theories/bar.v
-I src/
src/baz.ml4
src/bazaux.ml
src/qux_plugin.mlpack


Currently, both CoqIDE and Proof-General (version ≥ 4.3pre) understand _CoqProject files and invoke Coq with the desired options.

The coq_makefile utility can be used to set up a build infrastructure for the Coq project based on makefiles. The recommended way of invoking coq_makefile is the following one:

coq_makefile -f _CoqProject -o CoqMakefile


Such command generates the following files:

CoqMakefile
is a generic makefile for GNU Make that provides targets to build the project (both .v and .ml* files), to install it system-wide in the coq-contrib directory (i.e. where Coq is installed) as well as to invoke coqdoc to generate HTML documentation.
CoqMakefile.conf
contains make variables assignments that reflect the contents of the _CoqProject file as well as the path relevant to Coq.

An optional file CoqMakefile.local can be provided by the user in order to extend CoqMakefile. In particular one can declare custom actions to be performed before or after the build process. Similarly one can customize the install target or even provide new targets. Extension points are documented in paragraph CoqMakefile.local.

The extensions of the files listed in _CoqProject is used in order to decide how to build them. In particular:

• Coq files must use the .v extension
• OCaml files must use the .ml or .mli extension
• OCaml files that require pre processing for syntax extensions (like VERNAC EXTEND) must use the .ml4 extension
• In order to generate a plugin one has to list all OCaml modules (i.e. Baz for baz.ml) in a .mlpack file (or .mllib file).

The use of .mlpack files has to be preferred over .mllib files, since it results in a “packed” plugin: All auxiliary modules (as Baz and Bazaux) are hidden inside the plugin’s "namespace" (Qux_plugin). This reduces the chances of begin unable to load two distinct plugins because of a clash in their auxiliary module names.

### CoqMakefile.local¶

The optional file CoqMakefile.local is included by the generated file CoqMakefile. It can contain two kinds of directives.

Variable assignment

The variable must belong to the variables listed in the Parameters section of the generated makefile. Here we describe only few of them.

CAMLPKGS: CAMLFLAGS: can be used to specify third party findlib packages, and is passed to the OCaml compiler on building or linking of modules. Eg: -package yojson. can be used to specify additional flags to the OCaml compiler, like -bin-annot or -w.... can be set in order to use alternative binaries (e.g. wrappers) can be extended by including other paths in which *.cm* files are searched. For example COQ_SRC_SUBDIRS+=user-contrib/Unicoq lets you build a plugin containing OCaml code that depends on the OCaml code of Unicoq.

Rule extension

The following makefile rules can be extended.

Example

pre-all::
echo "This line is print before making the all target"
install-extra::
cp ThisExtraFile /there/it/goes

pre-all::
run before the all target. One can use this to configure the project, or initialize sub modules or check dependencies are met.
post-all::
run after the all target. One can use this to run a test suite, or compile extracted code.
install-extra::
run after install. One can use this to install extra files.
install-doc::
One can use this to install extra doc.
uninstall::
uninstall-doc::
clean::
cleanall::
archclean::
merlin-hook::
One can append lines to the generated .merlin file extending this target.

### Timing targets and performance testing¶

The generated Makefile supports the generation of two kinds of timing data: per-file build-times, and per-line times for an individual file.

The following targets and Makefile variables allow collection of per- file timing data:

• TIMED=1

passing this variable will cause make to emit a line describing the user-space build-time and peak memory usage for each file built.

Note

On Mac OS, this works best if you’ve installed gnu-time.

Example

For example, the output of make TIMED=1 may look like this:

COQDEP Fast.v
COQDEP Slow.v
COQC Slow.v
Slow (user: 0.34 mem: 395448 ko)
COQC Fast.v
Fast (user: 0.01 mem: 45184 ko)

• pretty-timed

this target stores the output of make TIMED=1 into time-of-build.log, and displays a table of the times, sorted from slowest to fastest, which is also stored in time-of-build-pretty.log. If you want to construct the log for targets other than the default one, you can pass them via the variable TGTS, e.g., make pretty-timed TGTS="a.vo b.vo".

Note

This target will append to the timing log; if you want a fresh start, you must remove the filetime-of-build.log or run make cleanall.

Example

For example, the output of make pretty-timed may look like this:

COQDEP Fast.v
COQDEP Slow.v
COQC Slow.v
Slow (user: 0.36 mem: 393912 ko)
COQC Fast.v
Fast (user: 0.05 mem: 45992 ko)
Time     | File Name
--------------------
0m00.41s | Total
--------------------
0m00.36s | Slow
0m00.05s | Fast

• print-pretty-timed-diff

this target builds a table of timing changes between two compilations; run make make-pretty-timed-before to build the log of the “before” times, and run make make-pretty-timed-after to build the log of the “after” times. The table is printed on the command line, and stored in time-of-build-both.log. This target is most useful for profiling the difference between two commits in a repository.

Note

This target requires python to build the table.

Note

The make-pretty-timed-before and make-pretty-timed-after targets will append to the timing log; if you want a fresh start, you must remove the files time-of-build-before.log and time-of-build-after.log or run make cleanall before building either the “before” or “after” targets.

Note

The table will be sorted first by absolute time differences rounded towards zero to a whole-number of seconds, then by times in the “after” column, and finally lexicographically by file name. This will put the biggest changes in either direction first, and will prefer sorting by build-time over subsecond changes in build time (which are frequently noise); lexicographic sorting forces an order on files which take effectively no time to compile.

Example

For example, the output table from make print-pretty-timed-diff may look like this:

After    | File Name | Before   || Change    | % Change
--------------------------------------------------------
0m00.39s | Total     | 0m00.35s || +0m00.03s | +11.42%
--------------------------------------------------------
0m00.37s | Slow      | 0m00.01s || +0m00.36s | +3600.00%
0m00.02s | Fast      | 0m00.34s || -0m00.32s | -94.11%


The following targets and Makefile variables allow collection of per- line timing data:

• TIMING=1

passing this variable will cause make to use coqc -time to write to a .v.timing file for each .v file compiled, which contains line-by-line timing information.

Example

For example, running make all TIMING=1 may result in a file like this:

Chars 0 - 26 [Require~Coq.ZArith.BinInt.] 0.157 secs (0.128u,0.028s)
Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c...] 0. secs (0.u,0.s)
Chars 69 - 162 [Definition~foo0~:=~Eval~comp~i...] 0.153 secs (0.136u,0.019s)
Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s)

• print-pretty-single-time-diff

print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing


this target will make a sorted table of the per-line timing differences between the timing logs in the BEFORE and AFTER files, display it, and save it to the file specified by the TIME_OF_PRETTY_BUILD_FILE variable, which defaults to time-of-build-pretty.log. To generate the .v.before-timing or .v.after-timing files, you should pass TIMING=before or TIMING=after rather than TIMING=1.

Note

The sorting used here is the same as in the print-pretty-timed -diff target.

Note

This target requires python to build the table.

Example

For example, running print-pretty-single-time-diff might give a table like this:

After     | Code                                                | Before    || Change    | % Change
---------------------------------------------------------------------------------------------------
0m00.50s  | Total                                               | 0m04.17s  || -0m03.66s | -87.96%
---------------------------------------------------------------------------------------------------
0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47%
0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.]        | 0m00.143s || -0m00.01s | -11.88%
N/A    | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s    || +0m00.00s | N/A
0m00.s    | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] |    N/A    || +0m00.00s | N/A
0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97%

• all.timing.diff, path/to/file.v.timing.diff

The path/to/file.v.timing.diff target will make a .v.timing.diff file for the corresponding .v file, with a table as would be generated by the print-pretty-single-time-diff target; it depends on having already made the corresponding .v.before-timing and .v.after-timing files, which can be made by passing TIMING=before and TIMING=after. The all.timing.diff target will make such timing difference files for all of the .v files that the Makefile knows about. It will fail if some .v.before-timing or .v.after-timing files don’t exist.

Note

This target requires python to build the table.

### Reusing/extending the generated Makefile¶

Including the generated makefile with an include directive is discouraged. The contents of this file, including variable names and status of rules shall change in the future. Users are advised to include Makefile.conf or call a target of the generated Makefile as in make -f Makefile target from another Makefile.

One way to get access to all targets of the generated CoqMakefile is to have a generic target for invoking unknown targets.

Example

# KNOWNTARGETS will not be passed along to CoqMakefile
KNOWNTARGETS := CoqMakefile extra-stuff extra-stuff2
# KNOWNFILES will not get implicit targets from the final rule, and so
# depending on them won't invoke the submake
# Warning: These files get declared as PHONY, so any targets depending
# on them always get rebuilt
KNOWNFILES   := Makefile _CoqProject

.DEFAULT_GOAL := invoke-coqmakefile

CoqMakefile: Makefile _CoqProject
$(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile invoke-coqmakefile: CoqMakefile$(MAKE) --no-print-directory -f CoqMakefile $(filter-out$(KNOWNTARGETS),$(MAKECMDGOALS)) .PHONY: invoke-coqmakefile$(KNOWNFILES)

####################################################################
##                      Your targets here                         ##
####################################################################

# This should be the last rule, to handle any targets not declared above
%: invoke-coqmakefile
@true


### Building a subset of the targets with -j¶

To build, say, two targets foo.vo and bar.vo in parallel one can use make only TGTS="foo.vo bar.vo" -j.

Note

make foo.vo bar.vo -j has a different meaning for the make utility, in particular it may build a shared prerequisite twice.

Note

For users of coq_makefile with version < 8.7

• Support for "subdirectory" is deprecated. To perform actions before or after the build (like invoking make on a subdirectory) one can hook in pre-all and post-all extension points.
• -extra-phony and -extra are deprecated. To provide additional target (.PHONY or not) please use CoqMakefile.local.

## Module dependencies¶

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

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 Require commands (Require, Require Export, Require Import), but also at the command Declare ML Module.

Dependencies of OCaml 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 OCaml module dependencies.

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

The build infrastructure generated by coq_makefile uses coqdep to automatically compute the dependencies among the files part of the project.

## 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

1. to produce a nice LaTeX and/or HTML document from Coq source files, readable for a human and not only for the proof assistant;
2. to help the user navigate his own (or third-party) sources.

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

Preformatted 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* %...LATEX...% #...html...# *)


or

(** printing  *token* $...LATEX math...$ #...html...# *)


It gives the LaTeX and HTML texts to be produced for the given Coq token. Either the LaTeX or the HTML rule 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.

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 asterisks at the beginning of a line followed by a space and the title of the section. One asterisk is a section, two a subsection, etc.

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 enclosing 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 LaTeX and HTML.¶

Pure LaTeX or HTML material can be inserted using the following escape sequences:

• $...LATEX stuff...$ inserts some LaTeX material in math mode. Simply discarded in HTML output.
• %...LATEX stuff...% inserts some LaTeX material. Simply discarded in HTML output.
• #...HTML stuff...# inserts some HTML material. Simply discarded in LaTeX output.

Note

(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 tabulations 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 inferior-coq.el. Instructions to use it are contained in this file.

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

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

## 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).