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 \
topbin/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,coq.plugins.ltac \
topbin/coqtop_bin.ml -o my_toplevel.native
and similarly for other plugins.
Building a Coq project¶
As of today it is possible to build Coq projects using two tools:
coq_makefile, which is distributed by Coq and is based on generating a makefile,
Dune, the standard OCaml build tool, which, since version 1.9, supports building Coq libraries.
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, -Q, -I, see 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
-arg -w
-arg all
theories/foo.v
theories/bar.v
-I src/
src/baz.mlg
src/bazaux.ml
src/qux_plugin.mlpack
where options -R, -Q, -I and -native-compiler are natively recognized, as well as
file names. The lines of the form -arg foo are used in order to tell
to literally pass an argument foo to coqc: in the
example, this allows to pass the two-word option -w all (see
command line options).
Note that it is mandatory to specify a -R/-Q flag for your
project, so its modules are properly qualified. Omitting it will
generate object files that are not usable except for expert cases.
The -native-compiler option given in the _CoqProject file will override
the global one passed at configure time.
CoqIDE, Proof-General and VSCoq all
understand _CoqProject files and can be used to 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 makefile for
GNU Makewith targets to build the project (e.g. generate .vo or .html files from .v or compile .ml* files) and install it in theuser-contribdirectory where the Coq library is installed.- CoqMakefile.conf
contains make variables assignments that reflect the contents of the
_CoqProjectfile as well as the path relevant to Coq.
Run coq_makefile --help for a description of command line options.
The recommended approach is to invoke CoqMakefile from a standard
Makefile of the following form:
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
The advantage of a wrapper, compared to directly calling the generated
Makefile, is that it
provides a target independent of the version of Coq to regenerate a
Makefile specific to the current version of Coq. Additionally, the
master Makefile can be extended with targets not specific to Coq.
Including the generated makefile with an include directive is
discouraged, since the contents of this file, including variable names and
status of rules, may change in the future.
Use the optional file CoqMakefile.local to extend
CoqMakefile. In particular, you can declare custom actions to run
before or after the build process. Similarly you can customize the
install target or even provide new targets. See
CoqMakefile.local for extension-point documentation. Although
you can use all variables defined in CoqMakefile in the recipes
of rules that you write and in the definitions of any variables that
you assign with =, many variables are not available for use if you
assign variable values with := nor to define the targets of
rules nor in top-level conditionals such as ifeq. Additionally,
you must use secondary expansion
to make use of such variables in the prerequisites of rules. To access
variables defined in CoqMakefile in rule target computation,
top-level conditionals, and := variable assignment, for example to
add new dependencies to compiled outputs, use the optional file
CoqMakefile.local-late. See CoqMakefile.local-late for a
non-exhaustive list of variables.
The extensions of files listed in _CoqProject determine
how they are built. In particular:
Coq files must use the
.vextensionOCaml files must use the
.mlor.mliextensionOCaml files that require pre processing for syntax extensions (like
VERNAC EXTEND) must use the.mlgextensionIn order to generate a plugin one has to list all OCaml modules (i.e.
Bazforbaz.ml) in a.mlpackfile (or.mllibfile).
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. Use
CoqMakefile.local-late instead to access more variables. These include:
- CAMLPKGS
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.- CAMLFLAGS
can be used to specify additional flags to the OCaml compiler, like
-bin-annotor-w....- OCAMLWARN
it contains a default of
-warn-error +a-3, useful to modify this setting; beware this is not recommended for projects in Coq's CI.- COQC, COQDEP, COQDOC
can be set in order to use alternative binaries (e.g. wrappers)
- COQ_SRC_SUBDIRS
can be extended by including other paths in which
*.cm*files are searched. For exampleCOQ_SRC_SUBDIRS+=user-contrib/Unicoqlets you build a plugin containing OCaml code that depends on the OCaml code ofUnicoq- COQFLAGS
override the flags passed to
coqc. By default-q.- COQEXTRAFLAGS
extend the flags passed to
coqc- COQCHKFLAGS
override the flags passed to
coqchk. By default-silent -o.- COQCHKEXTRAFLAGS
extend the flags passed to
coqchk- COQDOCFLAGS
override the flags passed to
coqdoc. By default-interpolate -utf8.- COQDOCEXTRAFLAGS
extend the flags passed to
coqdoc- COQLIBINSTALL, COQDOCINSTALL
specify where the Coq libraries and documentation will be installed. By default a combination of
$(DESTDIR)(if defined) with$(COQLIB)/user-contriband$(DOCDIR)/user-contrib.
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
alltarget. One can use this to configure the project, or initialize sub modules or check dependencies are met.post-all::run after the
alltarget. 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
.merlinfile extending this target.
CoqMakefile.local-late¶
The optional file CoqMakefile.local-late is included at the end of the generated
file CoqMakefile. The following is a partial list of accessible variables:
- COQ_VERSION
the version of
coqcbeing used, which can be used to provide different behavior depending on the Coq version- COQMAKEFILE_VERSION
the version of Coq used to generate the Makefile, which can be used to detect version mismatches
- ALLDFILES
the list of generated dependency files, which can be used, for example, to cause
maketo recompute dependencies when files change by writing$(ALLDFILES): myfilesor to indicate that files must be generated before dependencies can be computed by writing$(ALLDFILES): | mygeneratedfiles- VOFILES, GLOBFILES, CMOFILES, CMXFILES, OFILES, CMAFILES, CMXAFILES, CMIFILES, CMXSFILES
lists of files that are generated by various invocations of the compilers
In addition, the following variables may be useful for
deciding what targets to present via $(shell ...); these
variables are already accessible in recipes for rules added in
CoqMakefile.local, but are only accessible from top-level $(shell
...) invocations in CoqMakefile.local-late:
- COQC, COQDEP, COQDOC, CAMLC, CAMLOPTC
compiler binaries
- COQFLAGS, CAMLFLAGS, COQLIBS, COQDEBUG, OCAMLLIBS
flags passed to the Coq or OCaml compilers
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=1passing this variable will cause
maketo 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 installedgnu-time.Example
For example, the output of
make TIMED=1may look like this:COQDEP Fast.v COQDEP Slow.v COQC Slow.v Slow.vo (user: 0.34 mem: 395448 ko) COQC Fast.v Fast.vo (user: 0.01 mem: 45184 ko)
pretty-timedthis target stores the output of
make TIMED=1intotime-of-build.log, and displays a table of the times and peak memory usages, sorted from slowest to fastest, which is also stored intime-of-build-pretty.log. If you want to construct thelogfor targets other than the default one, you can pass them via the variableTGTS, e.g.,make pretty-timed TGTS="a.vo b.vo".Note
This target requires
pythonto build the table.Note
This target will append to the timing log; if you want a fresh start, you must remove the file
time-of-build.logorrun make cleanall.Note
By default the table displays user times. If the build log contains real times (which it does by default), passing
TIMING_REAL=1tomake pretty-timedwill use real times rather than user times in the table.Note
Passing
TIMING_INCLUDE_MEM=0tomakewill result in the tables not including peak memory usage information. PassingTIMING_SORT_BY_MEM=1tomakewill result in the tables be sorted by peak memory usage rather than by the time taken.Example
For example, the output of
make pretty-timedmay look like this:COQDEP VFILES COQC Slow.v Slow.vo (real: 0.52, user: 0.39, sys: 0.12, mem: 394648 ko) COQC Fast.v Fast.vo (real: 0.06, user: 0.02, sys: 0.03, mem: 56980 ko) Time | Peak Mem | File Name -------------------------------------------- 0m00.41s | 394648 ko | Total Time / Peak Mem -------------------------------------------- 0m00.39s | 394648 ko | Slow.vo 0m00.02s | 56980 ko | Fast.vo
print-pretty-timed-diffthis target builds a table of timing changes between two compilations; run
make make-pretty-timed-beforeto build the log of the “before” times, and runmake make-pretty-timed-afterto build the log of the “after” times. The table is printed on the command line, and stored intime-of-build-both.log. This target is most useful for profiling the difference between two commits in a repository.Note
This target requires
pythonto build the table.Note
The
make-pretty-timed-beforeandmake-pretty-timed-aftertargets will append to the timing log; if you want a fresh start, you must remove the filestime-of-build-before.logandtime-of-build-after.logor runmake cleanallbefore 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.
If you prefer a different sorting order, you can pass
TIMING_SORT_BY=absoluteto sort by the total time taken, orTIMING_SORT_BY=diffto sort by the signed difference in time.Note
Just like
pretty-timed, this table defaults to using user times. PassTIMING_REAL=1tomakeon the command line to show real times instead.Note
Just like
pretty-timed, passingTIMING_INCLUDE_MEM=0tomakewill result in the tables not including peak memory usage information. PassingTIMING_SORT_BY_MEM=1tomakewill result in the tables be sorted by peak memory usage rather than by the time taken.Example
For example, the output table from
make print-pretty-timed-diffmay look like this:After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ----------------------------------------------------------------------------------------------------------------------------- 0m00.43s | 394700 ko | Total Time / Peak Mem | 0m00.41s | 394648 ko || +0m00.01s || 52 ko | +4.87% | +0.01% ----------------------------------------------------------------------------------------------------------------------------- 0m00.39s | 394700 ko | Fast.vo | 0m00.02s | 56980 ko || +0m00.37s || 337720 ko | +1850.00% | +592.69% 0m00.04s | 56772 ko | Slow.vo | 0m00.39s | 394648 ko || -0m00.35s || -337876 ko | -89.74% | -85.61%
The following targets and Makefile variables allow collection of per-
line timing data:
TIMING=1passing this variable will cause
maketo usecoqc -timeto write to a.v.timingfile for each.vfile compiled, which contains line-by-line timing information.Example
For example, running
make all TIMING=1may 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-diffprint-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing
this target will make a sorted table of the per-line timing differences between the timing logs in the
BEFOREandAFTERfiles, display it, and save it to the file specified by theTIME_OF_PRETTY_BUILD_FILEvariable, which defaults totime-of-build-pretty.log. To generate the.v.before-timingor.v.after-timingfiles, you should passTIMING=beforeorTIMING=afterrather thanTIMING=1.Note
The sorting used here is the same as in the
print-pretty-timed-difftarget.Note
This target requires python to build the table.
Note
This target follows the same sorting order as the
print-pretty-timed-difftarget, and supports the same options for theTIMING_SORT_BYvariable.Note
By default, two lines are only considered the same if the character offsets and initial code strings are identical. Passing
TIMING_FUZZ=Nrelaxes this constraint by allowing the character locations to differ by up toN, as long as the total number of characters and initial code strings continue to match. This is useful when there are small changes to a file, and you want to match later lines that have not changed even though the character offsets have changed.Note
By default the table picks up real times, under the assumption that when comparing line-by-line, the real time is a more accurate representation as it includes disk time and time spent in the native compiler. Passing
TIMING_REAL=0tomakewill use user times rather than real times in the table.Example
For example, running
print-pretty-single-time-diffmight 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.diffThe
path/to/file.v.timing.difftarget will make a.v.timing.difffile for the corresponding.vfile, with a table as would be generated by theprint-pretty-single-time-difftarget; it depends on having already made the corresponding.v.before-timingand.v.after-timingfiles, which can be made by passingTIMING=beforeandTIMING=after. Theall.timing.difftarget will make such timing difference files for all of the.vfiles that theMakefileknows about. It will fail if some.v.before-timingor.v.after-timingfiles don’t exist.Note
This target requires python to build the table.
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
makeon a subdirectory) one can hook in pre-all and post-all extension points.-extra-phonyand-extraare deprecated. To provide additional target (.PHONYor not) please useCoqMakefile.local.
Note
Due to limitations with the compilation chain, makefiles generated
by coq_makefile won't correctly compile OCaml plugins with OCaml
< 4.07.0 when using more than one job (-j N for N > 1).
Precompiling for native_compute¶
To compile files for native_compute, one can use the
-native-compiler yes option of Coq, for instance by putting the
following in a CoqMakefile.local file:
COQEXTRAFLAGS += -native-compiler yes
The generated CoqMakefile installation target will then take care
of installing the extra .coq-native directories.
Note
As an alternative to modifying any file, one can set the
environment variable when calling make:
COQEXTRAFLAGS="-native-compiler yes" make
This can be useful when files cannot be modified, for instance when
installing via OPAM a package built with coq_makefile:
COQEXTRAFLAGS="-native-compiler yes" opam install coq-package
Note
This requires all dependencies to be themselves compiled with
-native-compiler yes.
Building a Coq project with Dune¶
Note
Dune's Coq support is still experimental; we strongly recommend using Dune 2.3 or later.
Note
The canonical documentation for the Coq Dune extension is maintained upstream; please refer to the Dune manual for up-to-date information. This documentation is up to date for Dune 2.3.
Building a Coq project with Dune requires setting up a Dune project
for your files. This involves adding a dune-project and
pkg.opam file to the root (pkg.opam can be empty or generated
by Dune itself), and then providing dune files in the directories
your .v files are placed. For the experimental version "0.1" of
the Coq Dune language, Coq library stanzas look like:
(coq.theory
(name <module_prefix>)
(package <opam_package>)
(synopsis <text>)
(modules <ordered_set_lang>)
(libraries <ocaml_libraries>)
(flags <coq_flags>))
This stanza will build all .v files in the given directory, wrapping
the library under <module_prefix>. If you declare an
<opam_package>, an .install file for the library will be
generated; the optional (modules <ordered_set_lang>) field allows
you to filter the list of modules, and (libraries
<ocaml_libraries>) allows the Coq theory depend on ML plugins. For
the moment, Dune relies on Coq's standard mechanisms (such as
COQPATH) to locate installed Coq libraries.
By default Dune will skip .v files present in subdirectories. In
order to enable the usual recursive organization of Coq projects add
(include_subdirs qualified)
to you dune file.
Once your project is set up, dune build will generate the
pkg.install files and all the files necessary for the installation
of your project.
Example
A typical stanza for a Coq plugin is split into two parts. An OCaml build directive, which is standard Dune:
(library
(name equations_plugin)
(public_name equations.plugin)
(flags :standard -warn-error -3-9-27-32-33-50)
(libraries coq.plugins.cc coq.plugins.extraction))
(coq.pp (modules g_equations))
And a Coq-specific part that depends on it via the libraries field:
(coq.theory
(name Equations) ; -R flag
(package equations)
(synopsis "Equations Plugin")
(libraries coq.plugins.extraction equations.plugin)
(modules :standard \ IdDec NoCycle)) ; exclude some modules that don't build
(include_subdirs qualified)
Computing Module dependencies¶
In order to compute module dependencies (to be used by make or
dune), Coq provides the coqdep tool.
coqdep computes inter-module dependencies for Coq
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.
See the man page of coqdep for more details and options.
Both Dune and coq_makefile use coqdep to compute the
dependencies among the files part of a Coq project.
Split compilation of native computation files¶
Coq features a native_compute tactic to provide fast computation in the
kernel. This process performs compilation of Coq terms to OCaml programs using
the OCaml compiler, which may cause an important overhead. Hence native
compilation is an opt-in configure flag.
When native compilation is activated, Coq generates the compiled files upfront,
i.e. during the coqc invocation on the corresponding .v file. This is
impractical because it means one must chose in advance whether they will use
a native-capable Coq installation. In particular, activating native compilation
forces the recompilation of the whole Coq installation. See
command line options for more details.
Starting from Coq 8.14, a new binary coqnative is available. It allows
performing split native compilation by generating the native compute files out
of the compiled .vo file rather than out of the source .v file.
The coqnative command takes a name file.vo as argument and tries to
perform native compilation on it. It assumes that the Coq libraries on which
file.vo depends have been first compiled to their native files, and will fail
otherwise. It accepts the -R, -Q, -I and -nI arguments with the
same semantics as if the native compilation process had been performed through
coqc. In particular, it means that:
-Rand-Qare equivalent-Iis a no-op that is accepted only for scripting convenience
Embedded Coq phrases inside LaTeX documents¶
When writing 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 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.
Man pages¶
There are man pages for the commands coqdep and coq-tex. Man
pages are installed at installation time (see installation
instructions in file INSTALL, step 6).