This file documents what a Coq developer needs to know about the Dune-based build system. If you want to enhance the build system itself (or are curious about its implementation details), see build-system.dev.txt, and in particular its initial HISTORY section.
Coq can now be built using Dune.
Usually, using the latest version of Dune is recommended, see the
first line of the dune-project
file for the minimum required
version.
If you set COQ_USE_DUNE=1
, then you don't need to explicitly add -f Makefile.dune
in any of the commands below. However, you will then
need an explicit -f Makefile.make
if you want to use one of the
legacy targets.
It is strongly recommended that you use the helper targets available
in Makefile.dune
, make -f Makefile.dune
will display help. Note
that dune will call configure for you if needed, so no need to call
./configure
in the regular development workflow.
4 common operations targets are:
make -f Makefile.dune check
: build all ml targets as fast as possiblemake -f Makefile.dune world
: build a complete Coq distributiondune exec -- dev/shim/coqtop-prelude
: build and launch coqtop + prelude [equivalent tomake states
].dune build $target
: where$target
can refer to the build directory or the source directory [but will be placed under_build
]
dune build @install
will build all the public Coq artifacts; dune build
will build all the targets in the workspace, including tests
and documentation (so this is usually not what you want).
Dune puts build artifacts in a separate directory _build/$context
;
usual context
is default
; dune also produces an "install" layout
under _build/install/$context/
. Depending on whether you want refer
to the source layout or to the install layout, you may refer to
targets in one or the other directory. It will also generate an
.install
file so files can be properly installed by package
managers.
Dune doesn't allow leftovers of object files it may generate in-tree [as to avoid conflicts], so please be sure your tree is clean from objects files generated by the make-based system or from manual compilation.
Contrary to other systems, Dune doesn't use a global Makefile
but
local build files named dune
which are later composed to form a
global build, for example plugins/ltac/dune
or kernel/dune
.
As a developer, Dune should take care of all OCaml-related build tasks
including library management, merlin
setup, linking order,
etc... You should not have to modify dune
files in regular workflow
unless you are adding a new binary, library, or plugin, or want to
tweak some low-level option.
Dune will read the file ~/.config/dune/config
; see man dune-config
. Among others, you can set in this file the custom number
of build threads (jobs N)
and display options (display _mode_)
.
Running coqtop
directly with dune exec -- coqtop
won't in general
work well unless you are using dune exec -- coqtop -noinit
. The
coqtop
binary doesn't depend itself on Coq's prelude, so plugins /
vo files may go stale if you rebuild only coqtop
.
Instead, you should use the provided "shims" for running coqtop
and
coqide
in a fast build. In order to use them, do:
$ dune exec -- dev/shim/coqtop-prelude
or quickide
/ dev/shim/coqide-prelude
for CoqIDE, etc.... See
dev/shim/dune
for a complete list of targets. These targets enjoy
quick incremental compilation thanks to -opaque
so they tend to be
very fast while developing.
Note that for a fast developer build of ML files, the check
target
is faster, as it doesn't link the binaries and uses the non-optimizing
compiler.
If you built the full standard library with the world
target,
then you can run the commands in the
_build/install/default/bin
directories (including coq_makefile
).
The default dune target is dune build
(or dune build @install
),
which will scan all sources in the Coq tree and then build the whole
project, creating an "install" overlay in _build/install/default
.
You can build some other target by doing dune build $TARGET
, where
$TARGET
can be a .cmxa
, a binary, a file that Dune considers a
target, an alias, etc...
In order to build a single package, you can do dune build $PACKAGE.install
.
A very useful target is dune build @check
, that will compile all the
ml files in quick mode.
Dune also provides targets for documentation, testing, and release builds, please see below.
Coq's test-suite can be run with dune runtest
; given that dune
still invokes the test-suite makefile, the environment variable
NJOBS
will control the value of the -j
option that is passed to
make; common call NJOBS=8 dune runtest
. This will be resolved in the
future once the test suite is ported to Dune rules.
There is preliminary support to build the API documentation and
reference manual in HTML format, use dune build {@doc,@refman-html}
to generate them.
So far these targets will build the documentation artifacts, however no install rules are generated yet.
You can create a developer shell with dune utop $library
, where
$library
can be any directory in the current workspace. For example,
dune utop engine
or dune utop plugins/ltac
will launch utop
with
the right libraries already loaded.
Note that you must invoke the #rectypes;;
toplevel flag in order to
use Coq libraries. The provided .ocamlinit
file does this
automatically.
You can use ocamldebug
with Dune; after a build, do:
dune exec -- dev/dune-dbg coqc foo.v
(ocd) source dune_db
to start coqc.byte foo.v
, other targets are {checker,coqide,coqtop}
:
dune exec -- dev/dune-dbg checker foo.vo
(ocd) source dune_db
Unfortunately, dependency handling is not fully refined / automated, you may find the occasional hiccup due to libraries being renamed, etc... Please report any issue.
For running in emacs, use coqdev-ocamldebug
from coqdev.el
.
Note: If you are using OCaml >= 4.08 you need to use
(ocd) source dune_db_408
or
(ocd) source dune_db_409
depending on your OCaml version. This is due to several factors:
- OCaml >= 4.08 doesn't allow doubly-linking modules, however
source
is not re entrant and seems to doubly-load in the default setup, see coq#8952 - OCaml >= 4.09 comes with
dynlink
already linked in so we need to modify the list of modules loaded.
The following commands should work:
dune exec -- dev/shim/coqbyte-prelude
> Drop.
# #directory "dev";;
# #use "include";;
By default [in "developer mode"], Dune will compose all the packages
present in the tree and perform a global build. That means that for
example you could drop the ltac2
folder under plugins
and get a
build using ltac2
, that will use the current Coq version.
This is very useful to develop plugins and Coq libraries as your plugin will correctly track dependencies and rebuild incrementally as needed.
However, it is not always desirable to go this way. For example, the
current Coq source tree contains two packages [Coq and CoqIDE], and in
the OPAM CoqIDE package we don't want to build CoqIDE against the
local copy of Coq. For this purpose, Dune supports the -p
option, so
dune build -p coqide
will build CoqIDE against the system-installed
version of Coq libs, and use a "release" profile that for example
enables stronger compiler optimizations.
.opam
files are automatically generated by Dune from the package
descriptions in the dune-project
file; see Dune's manual for more
details.
dune
files contain the so-called "stanzas", that may declare:
- libraries,
- executables,
- documentation, arbitrary blobs.
The concrete options for each stanza can be seen in the Dune manual, but usually the default setup will work well with the current Coq sources. Note that declaring a library or an executable won't make it installed by default, for that, you need to provide a "public name".
Dune provides support for tree workspaces so the developer can set global options --- such as flags --- on all packages, or build Coq with different OPAM switches simultaneously [for example to test compatibility]; for more information, please refer to the Dune manual.
The ireport
profile will produce standard OCaml inlining
reports. These
are to be found under _build/default/$lib/$lib.objs/$module.$round.inlining.org
and are in Emacs org-mode
format.
Note that due to ocaml/dune#1401 , we must perform a full rebuild each time as otherwise Dune will remove the files. We hope to solve this in the future.
Dune supports or will support extra functionality that may result very useful to Coq, some examples are:
- Cross-compilation.
- Automatic Generation of OPAM files.
- Multi-directory libraries.
-
I get "Error: Dynlink error: Interface mismatch":
You are likely running a partial build which doesn't include implicitly loaded plugins / vo files. See the "Running binaries [coqtop / coqide]" section above as to how to correctly call Coq's binaries.
dune build
build all targets in the current workspacedune build @check
build all ML targets as fast as possible, setup merlindune utop $dir
open a shell for libraries in$dir
dune exec -- $file
build and execute binary$file
, can be in path or be an specific namedune build _build/$context/$foo
build target$foo$
in$context
, with build dir layoutdune build _build/install/$context/foo
build target$foo$
in$context
, with install dir layout
dune subst
generate metadata for a package to be installed / distributed, necessary for opamdune build -p $pkg
build a package in release mode