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. About Dune ========== Coq can now be built using [Dune](https://github.com/ocaml/dune). ## Quick Start 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. 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. ## Per-User Custom Settings 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 binaries [coqtop / coqide] 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. ## Targets 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. ## Documentation and testing targets 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. ## Developer shell 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. ## ocamldebug 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 https://github.com/coq/coq/issues/8952 - OCaml >= 4.09 comes with `dynlink` already linked in so we need to modify the list of modules loaded. ## Dropping from coqtop: The following commands should work: ``` dune exec -- dev/shim/coqbyte-prelude > Drop. # #directory "dev";; # #use "include_dune";; ``` ## Compositionality, developer and release modes. 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. ## Stanzas `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". ## Workspaces and Profiles 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. ## Inlining reports The `ireport` profile will produce standard OCaml [inlining reports](https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html#sec488). 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 https://github.com/ocaml/dune/issues/1401 , we must perform a full rebuild each time as otherwise Dune will remove the files. We hope to solve this in the future. ## Planned and Advanced features 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. ## FAQ - 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.