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
dune-project for the minimum required version; type dune build to
build the base Coq libraries. No call to ./configure is needed.
Dune will get confused if it finds leftovers of in-tree compilation, so please be sure your tree is clean from objects files generated by the make-based system.
If you want to build the standard libraries and plugins you should
call make -f Makefile.dune voboot. It is usually enough to do that
once per-session.
More helper targets are available in Makefile.dune, make -f Makefile.dune will display some help.
Dune places build artifacts in a separate directory _build; it will
also generate an .install file so files can be properly installed by
package managers.
Contrary to other systems, Dune doesn't use a global Makefile but
local build files named dune that are later composed to form a
global build.
As a developer, Dune should take care of all OCaml-related build tasks
including library management, merlin files, and linking order. You are
are not supposed to modify the dune files unless you are adding a
new binary, library, or plugin.
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_).
There are two special targets states and quickide that will
generate "shims" for running coqtop and coqide in a fast build. In
order to use them, do:
$ make -f Makefile.dune voboot # Only once per session
$ dune exec -- dev/shim/coqtop-preludeor quickide / dev/shim/coqide-prelude for CoqIDE. 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
will be faster.
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.
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 /path/to/foo.v
(ocd) source dune_dbor
dune exec -- dev/dune-dbg checker Foo
(ocd) source dune_dbfor the checker. Unfortunately, dependency handling here is not fully refined, so you need to build enough of Coq once to use this target [it will then correctly compute the deps and rebuild if you call the script again] This will be fixed in the future.
For running in emacs, use coqdev-ocamldebug from coqdev.el.
After doing make -f Makefile.dune voboot, the following commands should work:
dune exec -- dev/shim/coqbyte-prelude
> Drop.
# #directory "dev";;
# #use "include_dune";;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.
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.