Building Coq Projects¶
Coq configuration basics¶
Describes the basics of Coq configuration that affect running and compiling Coq scripts. It recommends preferred ways to install Coq, manage installed packages and structure your project directories for ease of use.
Installing Coq and Coq packages with opam¶
The easiest way to install Coq is with the Coq Platform, which relies on the opam package manager.
The Coq platform installation process provides options to automatically install some of the most frequently used packages at the same time. While there's currently no guarantee that user-developed packages will compile on the current version of Coq, all packages that Coq platform installs should compile without difficulty--this is part of the Coq platform release process.
Once you've installed Coq, you can search for additional user-developed packages from the package list or other opam repositories. These commands may be helpful:
opam list "coq-*"
to see the list of available and installed packagesopam list "coq-*" --installed
to see the list of installed packagesopam install <package name>
to install a package on your system.opam update
as needed to update the list of available packages
For example, this command shows the installed packages with the package name, its version and short description:
$ opam list "coq-*" --installed
coq-bignums 8.15.0 Bignums, the Coq library of arbitrary large numbers
Note that packages marked released
in the package list web page are more stable
than those marked extra-dev
. To install extra-dev
packages,
first add the coq-extra-dev
opam repository to your local opam installation
with this command:
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
While this is the easiest way to install packages, it is not the only way.
You will then need to find the logical name used to refer to the package
in Require
commands. There are a couple ways to do this:
If you installed with opam, use
opam show --list-files coq-bignums | head -n1
- the last component of the filename is the logical name (Bignums
).On Linux,
ls $(coqtop -where)/user-contrib
shows the logical names of all installed user-contributed packages. You should be able to guess which one you need.Use the
Print LoadPath
command when running Coq, which shows the mapping from logical paths to directories. Again, you should be able to guess.
The last two methods work even if you didn't install with opam. Perhaps in the future the package name to logical name mapping will be more readily available.
Once you know the logical name of the package, use it to load compiled
files from the package with the Require
command.
A package is a group of files in a top directory and its subdirectories that's installed as a unit. Packages are compiled from projects. These terms are virtually interchangeable.
Setup for working on your own projects¶
The working and master copies of source code for your own projects should not be in the directory tree where Coq is installed. In particular, when you upgrade to a new version of Coq, any directories you created in the old version won't be copied or moved.
We encourage you to use a source code control system for any non-trivial project because it makes it easy to track the history of your changes. git is the system most used by Coq projects. Typically, each project has its own git repository.
For a project that has only a single file, you can create the file wherever you like and then step through it in one of the IDEs for Coq, such as CoqIDE, ProofGeneral, vsCoq and Coqtail.
If your project has multiple files in a single directory that depend on each
other through Require
commands, they must be compiled in an order that
matches their dependencies.
Scripts in .v
files must be compiled to .vo
files using coqc
before they
can be Require
d in other files. Currently, the .vo
file is created in
the same directory as its .v
file. For example,
if B.v depends on A.v, then you should compile A.v before B.v. You can do this
with coqc A.v
followed by coqc B.v
, but you may find it tedious to
manage the dependencies, particularly as the number of files increases.
If your project files are in multiple directories, you would also need to pass additional command-line -Q and -R parameters to your IDE. More details to manage and keep track of.
Instead, by creating a _CoqProject
file, you can automatically generate
a makefile that applies the correct dependencies when it compiles your project.
In addition, the IDEs find and interpret _CoqProject
files, so project files
spread over multiple directories will work seamlessly. If you're editing dir/foo.v
,
the IDEs apply settings from the _CoqProject
file in dir
or the closest
ancestor directory.
The _CoqProject
file identifies the logical path to associate with the
directories containing your compiled files. The _CoqProject
file is normally
in the top directory of the project. Occasionally it may be useful to have
additional _CoqProject
files in subdirectories, for example in order to pass
different startup parameters to Coq for particular scripts.
Building a project with _CoqProject (overview)¶
Note: building with dune
is experimental. See Building a Coq project with Dune.
The _CoqProject
file contains the information needed to generate a makefile
for building your project. Your _CoqProject
file should be in
the top directory of your project's source tree. We recommend using the
logical name of the project as the name of the top directory.
Note: Make sure that _CoqProject
has no file extension. On Windows, some
tools such as Notepad invisibly append .txt
even when you ask to save the file
as _CoqProject
. Also, File Manager doesn't display file extensions. You may
be better off using a command line interface and an editor such as vi
that
always show file extensions.
For example, here is a minimal _CoqProject
file for the MyPackage
project
(the logical name of the package), which includes all the .v
files (and
other file types) in the theories
directory and its subdirectories:
-R theories MyPackage
theories
-R theories MyPackage
(see here) declares that theories
is a top
directory of MyPackage
. theories
on the second line declares that all .v
files
in theories
and its subdirectories are indeed included in the project.
In addition, you can list individual files, for example the two script files
theories/File1.v
and theories/SubDir/File2.v
whose logical paths are MyPackage.File1
and
MyPackage.SubDir.File2
:
-R theories MyPackage
theories/File1.v
theories/SubDir/File2.v
The generated makefile only processes the specified files. You can list multiple directories if you wish.
We suggest choosing a logical name that's different from those used for commonly
used packages, particularly if you plan to make your package available to others.
Or you can easily do a global replace, if necessary, on the package name
before it is (widely) used. After that, a name change may begin to impact
a large number of users. Alas, there's currently no easy way to discover what
logical names have already been used. The Print LoadPath
command helps
a bit; it shows the logical names defined in the Coq process.
Then:
Generate a makefile from
_CoqProject
withcoq_makefile -f _CoqProject -o CoqMakefile
andCompile your project with
make -f CoqMakefile
as needed.
If you add more files to your project that are not in directories listed
in _CoqProject
, update _CoqProject
and re-run coq_makefile
and make
.
We recommend checking CoqMakefile
and CoqMakefile.conf
into your source code
control system. Also we recommend updating them with coq_makefile
when you switch
to a new version of Coq.
In CoqIDE, you must explicitly save modified buffers before running make
and
restart the Coq interpreter in any buffers in which you're running code.
More details here.
See Building a Coq project with coq_makefile (details) for a complete description of coq_makefile
and the
files it generates.
Logical paths and the load path¶
Commands such as Require
identify files with logical paths rather
than file system paths so that scripts don't have to be modified to run on
different computers. The Print LoadPath
command displays the load path,
which is a list of (logical path, physical path) pairs for directories.
For example, you may see:
Logical Path / Physical path:
Bignums /home/jef/coq/lib/coq/user-contrib/Bignums
Bignums.BigZ /home/jef/coq/lib/coq/user-contrib/Bignums/BigZ
Ltac2 /home/jef/coq/lib/coq/user-contrib/Ltac2
Coq /home/jef/coq/lib/coq/theories
Coq.Numbers /home/jef/coq/lib/coq/theories/Numbers
Coq.Numbers.Natural /home/jef/coq/lib/coq/theories/Numbers/Natural
Coq.Numbers.Natural.Binary /home/jef/coq/lib/coq/theories/Numbers/Natural/Binary
Coq.Numbers.Integer /home/jef/coq/lib/coq/theories/Numbers/Integer
Coq.Arith /home/jef/coq/lib/coq/theories/Arith
<> /home/jef/myproj
The components of each pair share suffixes, e.g. Bignums.BigZ
and Bignums/BigZ
or
Coq.Numbers.Natural
and Numbers/Natural
. Physical pathnames should
always use /
rather than \
, even when running on Windows.
Packages with a physical path containing user-contrib
were installed
with the Coq binaries (e.g. Ltac2
), with the Coq Platform or with opam (e.g. Bignums
)
or perhaps by other means. Note that, for these entries, the entire logical path
appears in the directory name.
Packages that begin with Coq
were installed with the Coq binaries. Note
that the logical name Coq
doesn't appear in the physical path.
The <>
in the final entry represents an empty logical pathname, which
permits loading files from the
associated directory with just the basename of the script file,
e.g. specify Foo
to load Foo.vo
. This entry corresponds to the
current directory when Coq was started. Note that the Cd
command
doesn't change the associated directory--you would need to restart CoqIDE.
With some exceptions noted below, the load path is generated from files loaded
from the following directories and their subdirectories in the order shown. The
associated logical path is determined from the filesystem path, relative to the
directory, e.g. the file Foo/Bar/script.vo
becomes Foo.Bar.script
:
directories specified with -R and -Q command line options,
the current directory where the Coq process was launched (without including subdirectories),
the directories listed in the
COQPATH
environment variable (separated with colons, or, on Windows, with semicolons)
the
${XDG_DATA_HOME}/coq/
directory (see XDG base directory specification). However, CoqIDE relies on the default setting; therefore we recommend not setting this variable.installed packages from the
user-contrib
directory in the Coq installation,the Coq standard library from the
theories
directory in the Coq installation (withCoq
prepended to the logical path),
Each directory may contain multiple .v
/.vo
files. For example,
Require Import Stdlib.Numbers.Natural.Binary.NBinary
loads the file
NBinary.vo
from the associated directory. Note that a short name
is often sufficient in Require
instead of a fully qualified
name.
In Require
commands referring to the current package (if _CoqProject
uses -R
) or Coq's standard library can be referenced with a short name without
a From
clause provided that the logical path is unambiguous (as if they are
available through -R
). In contrast, Require
commands that load files from other
locations such as user-contrib
must either use an exact logical path
or include a From
clause (as if they are available through -Q
). This is done
to reduce the number of ambiguous logical paths. We encourage using From
clauses.
Note that if you use a _CoqProject
file, the COQPATH
environment variable is not helpful.
If you use COQPATH
without a _CoqProject
, a file in MyPackage/theories/SubDir/File.v
will be
loaded with the logical name MyPackage/theories/SubDir.File
, which may not be what you want.
If you associate the same logical name with more than one directory, Coq
looks for the .vo
file in the most recently added path first (i.e., the one
that appears earlier in the Print LoadPath
output).
Modifying multiple interdependent projects at the same time¶
If you want to modify multiple interdependent projects simultaneously,
good practice recommends that
all of them should be uninstalled. Since the IDEs only apply a single
_CoqProject
file for each script, the best way to make them work properly is to
temporarily edit the _CoqProject
for each project so it includes the other
uninstalled projects it depends on, then regenerate the makefile. This may
make your _CoqProject
system dependent. Such dependencies shouldn't be
present in published packages.
For example, if
project A
requires project B
, add -Q <directory path of B> B
to the
_CoqProject
in A
. This will override any installed version of B
only
when you're working on scripts in A
.
If you want to build all the related projects at once, you're on your own. There's currently no tooling to identify the internal dependencies between the projects (and thus the order in which to build them).
Installed and uninstalled packages¶
The directory structure of installed packages (i.e., in the user-contrib
directory
of the Coq installation) differs from that generally used for the project source tree.
The installed directory structure omits the pathname given in the -R
and -Q
parameters that aren't part of the logical name of a script. For example, the theories
pathname used in this _CoqProject
file is omitted from the installed pathname:
-R theories MyPackage
theories/File1.v
theories/SubDir/File2.v
theories/File1.v
appears in the directoryuser-contrib/MyPackage`and `theories/SubDir/File2.v
is in
user-contrib/MyPackage/SubDir
Use make -f CoqMakefile install
to install a project from a directory.
If you try to step through scripts in installed packages (e.g. to understand
the proofs therein), you may get unexpected failures for two reasons (which
don't apply to scripts in the standard library, which have logical paths
beginning with Coq
):
_CoqProject
files often have at least one-R
parameter, while installed packages are loaded with the less-permissive-Q
option described in theRequire
command, which may cause aRequire
to fail. One workaround is to create a_CoqProject
file containing the line-R . <project directory>
inuser-contrib/<project directory>
. In this case, the_CoqProject
doesn't need to list all the source files.Sometimes, the
_CoqProject
file specifies options that affect the behavior of Coq, such as-impredicative-set
. These can similarly be added in_CoqProject
files inuser-contrib
.
Another way to get around these problems is to download the source tree for the project in a new directory and compile it before stepping through its scripts.
Upgrading to a new version of Coq¶
.vo
files are specific to the version of Coq that compiled them. When you
upgrade to a new version of Coq, you must recompile all the projects
that you want to run in the new version. This is necessary to assure that
your proofs still work in the new version. Once their projects build on the
new version, most users no longer have a need to run on the old version.
If, however, you want to overlap working on your project on both the old and new
versions, you'll need to create separate source directories for your project
for the different Coq versions. Currently the compiled .vo
files are kept
in the same directory as their corresponding .v
file.
Building a Coq project with coq_makefile (details)¶
The coq_makefile
tool is included with Coq and is based on generating a makefile.
The majority of Coq projects are very similar: a collection of .v
files and possibly 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 _CoqProject
file may contain the following kinds of entries in any order,
separated by whitespace:
Selected options of coqc, which are forwarded directly to it. Currently these are
-Q
,-I
,-R
and-native-compiler
.-arg
options for other options of coqc that don’t fall in the above set.Options specific to
coq_makefile
. Currently there are two options:-generate-meta-for-package
(see below for details), and-docroot
.Directory names, which include all appropriate files in the directory and its subdirectories.
Comments, started with an unquoted
#
and continuing to the end of the line.
A simple example of a _CoqProject
file follows:
-R theories/ MyCode
-arg "-w all"
# include everything under "theories", e.g. foo.v and bar.v
theories
-I src/
# include everything under "src", e.g. baz.mlg bazaux.ml and qux_plugin.mlpack
src
-generate-meta-for-package my-package
Lines in the form -arg foo
pass the argument foo
to coqc
: in the
example, this passes the two-word option -w all
(see
command line options).
You must specify a -R/-Q
flag for your
project so its modules are properly qualified. Omitting it will
generate object files that are unusable except by experts.
Projects that include plugins (i.e. .ml
or .mlg
OCaml source files) must have a
META
file, as per findlib.
If the project has only a single plugin, the META
file can be
generated automatically when the option -generate-meta-for-package my-package
is given. The generated file makes the plugin available
to the Declare ML Module
as my-package.plugin
. If the generated file
doesn't suit your needs (for instance because it depends on some OCaml
packages) or your project has multiple plugins, then create a file named
META.my-package
and list it in the _CoqProject
file.
You can use ocamlfind lint META.my-package
to lint the hand written file.
Typically my-package
is the name of the OPAM
package for your
project (which conventionally starts with coq-
). If the project
includes a .mlg
file (to be pre-processed by coqpp
) that
declares a plugin, then the given name must match the findlib
plugin
name, e.g. DECLARE PLUGIN "my-package.plugin"
.
The -native-compiler
option given in the _CoqProject
file overrides
the global one passed at configure time.
CoqIDE, Proof General, VsCoq and Coqtail 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. We recommend
invoking coq_makefile
this way:
coq_makefile -f _CoqProject -o CoqMakefile
This command generates the following files:
- CoqMakefile
is a makefile for
GNU Make
with targets to build the project (e.g. generate .vo or .html files from .v or compile .ml* files) and install it in theuser-contrib
directory where the Coq library is installed.- CoqMakefile.conf
contains make variables assignments that reflect the contents of the
_CoqProject
file 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
in 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
.v
extensionOCaml files must use the
.ml
or.mli
extensionOCaml files that require pre processing for syntax extensions (like
VERNAC EXTEND
) must use the.mlg
extensionIn order to generate a plugin one has to list all OCaml modules (i.e.
Baz
forbaz.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.
Building a Coq project with Dune¶
Dune, the standard OCaml build tool, has supported building Coq libraries since version 1.9.
Note
Dune's Coq support is still experimental; we strongly recommend using Dune 3.2 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. The documentation below is up to date for Dune 3.2
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.3" 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 your 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.
Note that projects using Dune to build need to use the compatibility
syntax for Declare ML Module
, see example below:
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)
For now, each .v
file that loads the plugin must use
the following special syntax on its Declare ML Module
command for compatibility with current Dune versions (as of Coq 8.16):
Declare ML Module "equations_plugin:equations.plugin".
coqdep: 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
and Declare ML Module
commands.
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:
-R
and-Q
are equivalent-I
is a no-op that is accepted only for scripting convenience
Using Coq as a library¶
It is possible to build custom Coq executables - for example for better debugging or custom static linking.
The preferred method is to use dune
:
(executable
(name my_toplevel)
(libraries coq-core.toplevel))
in a directory with my_toplevel.ml
containing the main loop entry
point Coqc.main()
or Coqtop.(start_coq coqtop_toplevel)
(depending
on if you want coqc
or coqtop
behaviour).
For example, to statically link L
tac, you can do:
(executable
(name my_toplevel)
(libraries coq-core.toplevel coq-core.plugins.ltac))
and similarly for other plugins.
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).
Comments¶
#
outside of double quotes starts a comment that continues to the end of the line. Comments are ignored.Quoting arguments to coqc¶
Any string in a
_CoqProject
file may be enclosed in double quotes to include whitespace characters or#
. For example, use-arg "-w all"
to pass the argument-w all
to coqc. If the argument to coqc needs some quotes as well, use single-quotes inside the double-quotes. For example-arg "-set 'Default Goal Selector=!'"
gets passed to coqc as-set 'Default Goal Selector=!'
.But note, that single-quotes in a
_CoqProject
file are only special characters if they appear in the string following-arg
. And on their own they don't quote spaces. For example-arg 'foo bar'
in_CoqProject
is equivalent to-arg foo "bar'"
(in_CoqProject
notation).-arg "'foo bar'"
behaves differently and passes'foo bar'
to coqc.Forbidden filenames¶
The paths of files given in a
_CoqProject
file may not contain any of the following characters:\n
,\t
, space,\
,'
,"
,#
,$
,%
. These characters have special meaning in Makefiles andcoq_makefile
doesn't support encoding them correctly.Warning: No common logical root¶
When a
_CoqProject
file contains something like-R theories Foo theories/Bar.v
, theinstall-doc
target installs the documentation generated bycoqdoc
intouser-contrib/Foo/
, in the folder where Coq was installed.But if the
_CoqProject
file contains something like:the Coq files of the project don’t have a logical path in common and
coq_makefile
doesn’t know where to install the documentation. It will give a warning: "No common logical root" and generate a Makefile that installs the documentation in some folder beginning with "orphan", in the above example, it'd beuser-contrib/orphan_Foo_Bar
.In this case, specify the
-docroot
option in _CoqProject to override the automatically selected logical root.CoqMakefile.local¶
The optional file
CoqMakefile.local
is included by the generated fileCoqMakefile
. 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. These include: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
....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.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 exampleCOQ_SRC_SUBDIRS+=user-contrib/Unicoq
lets you build a plugin containing OCaml code that depends on the OCaml code ofUnicoq
override the flags passed to
coqc
. By default-q
.extend the flags passed to
coqc
override the flags passed to
coqchk
. By default-silent -o
.extend the flags passed to
coqchk
override the flags passed to
coqdoc
. By default-interpolate -utf8
.extend the flags passed to
coqdoc
specify where the Coq libraries, plugins and documentation will be installed. By default a combination of
$(DESTDIR)
(if defined) with$(COQLIB)/user-contrib
,$(COQCORELIB)/..
and$(DOCDIR)/coq/user-contrib
.Use CoqMakefile.local-late instead to access more variables.
Rule extension
The following makefile rules can be extended.
Example
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.CoqMakefile.local-late¶
The optional file
CoqMakefile.local-late
is included at the end of the generated fileCoqMakefile
. The following is a partial list of accessible variables:the version of
coqc
being used, which can be used to provide different behavior depending on the Coq versionthe version of Coq used to generate the Makefile, which can be used to detect version mismatches
the list of generated dependency files, which can be used, for example, to cause
make
to recompute dependencies when files change by writing$(ALLDFILES): myfiles
or to indicate that files must be generated before dependencies can be computed by writing$(ALLDFILES): | mygeneratedfiles
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 inCoqMakefile.local
, but are only accessible from top-level$(shell ...)
invocations inCoqMakefile.local-late
:compiler binaries
flags passed to the Coq or OCaml compilers
Timing targets and performance testing¶
The generated
Makefile
supports the generation of three kinds of timing data: per-file build-times, per-line times for individual files, and profiling data in Google trace format for individual files.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 installedgnu-time
.Example
For example, the output of
make TIMED=1
may look like this:pretty-timed
this target stores the output of
make TIMED=1
intotime-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 thelog
for 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
python
to 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.log
orrun 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=1
tomake pretty-timed
will use real times rather than user times in the table.Note
Passing
TIMING_INCLUDE_MEM=0
tomake
will result in the tables not including peak memory usage information. PassingTIMING_SORT_BY_MEM=1
tomake
will result in the tables be sorted by peak memory usage rather than by the time taken.Example
For example, the output of
make pretty-timed
may look like this: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 runmake make-pretty-timed-after
to 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
python
to build the table.Note
The
make-pretty-timed-before
andmake-pretty-timed-after
targets will append to the timing log; if you want a fresh start, you must remove the filestime-of-build-before.log
andtime-of-build-after.log
or runmake 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.
If you prefer a different sorting order, you can pass
TIMING_SORT_BY=absolute
to sort by the total time taken, orTIMING_SORT_BY=diff
to sort by the signed difference in time.Note
Just like
pretty-timed
, this table defaults to using user times. PassTIMING_REAL=1
tomake
on the command line to show real times instead.Note
Just like
pretty-timed
, passingTIMING_INCLUDE_MEM=0
tomake
will result in the tables not including peak memory usage information. PassingTIMING_SORT_BY_MEM=1
tomake
will 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-diff
may look like this:The following targets and
Makefile
variables allow collection of per- line timing data:TIMING=1
passing this variable will cause
make
to usecoqc -time-file
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:coqtimelog2html
this command produces a HTML file displaying the original
file.v
with highlights for each command indicating how much time the command used according to the given timing files. It supports between 1 and 3 timing files.There is currently no
coq_makefile
target that automatically invokes this tool.print-pretty-single-time-diff
this target will make a sorted table of the per-line timing differences between the timing logs in the
BEFORE
andAFTER
files, display it, and save it to the file specified by theTIME_OF_PRETTY_BUILD_FILE
variable, which defaults totime-of-build-pretty.log
. To generate the.v.before-timing
or.v.after-timing
files, you should passTIMING=before
orTIMING=after
rather thanTIMING=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.
Note
This target follows the same sorting order as the
print-pretty-timed-diff
target, and supports the same options for theTIMING_SORT_BY
variable.Note
By default, two lines are only considered the same if the character offsets and initial code strings are identical. Passing
TIMING_FUZZ=N
relaxes 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=0
tomake
will use user times rather than real times in the table.Example
For example, running
print-pretty-single-time-diff
might give a table like this: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 theprint-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 passingTIMING=before
andTIMING=after
. Theall.timing.diff
target will make such timing difference files for all of the.v
files that theMakefile
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.
PROFILE=1
passing this variable or setting it in the environment will causemake
to usecoqc -profile
to write to a.v.prof.json
file for each.v
file compiled, which contains Profiling information.The
.v.prof.json
is then compressed bygzip
to a.v.prof.json.gz
.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
ormake foo.vo bar.vo
.Precompiling for
native_compute
¶To compile files for
native_compute
, one can use the-native-compiler yes
option of Coq, by putting it in the_CoqProject
file.The generated installation target of
CoqMakefile
will then take care of installing the extra.coq-native
directories.Note
As an alternative to modifying
_CoqProject
, one can set an environment variable when callingmake
:This can be useful when files cannot be modified, for instance when installing via OPAM a package built with
coq_makefile
:Note
This requires all dependencies to be themselves compiled with
-native-compiler yes
.The grammar of _CoqProject¶
A
_CoqProject
file encodes a list of strings using the following syntax:where the following definitions apply:
space
,horizontal_tab
andnewline
stand for the corresponding ASCII characters.comment_char
is the set of all characters exceptnewline
.quoted_char
is the set of all characters except"
.string_start_char
is the set of all characters except those that matchblank
, or are"
or#
.unquoted_char
is the set of all characters except those that matchblank
or are#
.The parser produces a list of strings in the same order as they were encountered in
_CoqProject
. Blanks and comments are removed and the double quotes ofquoted_string
tokens are removed as well. The list is then treated as a list of command-line arguments ofcoq_makefile
.The semantics of
-arg
are as follows: the string given as argument is split on whitespace, but single quotes prevent splitting. The resulting list of strings is then passed to coqc.The current approach has a few limitations: Double quotes in a
_CoqProject
file are only special characters at the start of a string. For lack of an escaping mechanism, it is currently impossible to pass the following kinds of strings tocoq_makefile
using a_CoqProject
file:strings starting with
"
strings starting with
#
and containing"
strings containing both whitespace and
"
In addition, it is impossible to pass strings containing
'
to coqc via-arg
.