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 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 possible
- `make -f Makefile.dune world` : build a complete Coq distribution
- `dune exec -- dev/shim/coqtop-prelude` : build and launch coqtop + prelude [equivalent to `make 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.

## 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.

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`).

## 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.

## Testing and documentation targets

There are two ways to run the test suite using Dune:

- After building Coq with `make -f Makefile.dune world`, you can run the test-suite
  in place, generating output files in the source tree
  by running `make -C test-suite` from the top directory of the source tree
  (equivalent to running `make test-suite` from the `test-suite` directory).
  This permits incremental usage since output files will be preserved.

- You can also run the test suite in a hygienic way using `make -f
  Makefile.dune test-suite` or `dune runtest`. This is convenient for
  full runs from scratch, for instance in CI.

  Since `dune` still invokes the test-suite makefile, the
  environment variable `NJOBS` is used to set the `-j` option
  that is passed to make (for example, with the command
  `NJOBS=8 dune runtest`). This use of `NJOBS` will be
  removed when the test suite is fully ported to Dune.

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](https://ocaml.org/learn/tutorials/debug.html#The-OCaml-debugger) with Dune; after a build, do:

```
dune exec -- dev/dune-dbg coqc foo.v
(ocd) source db
```

to start `coqc.byte foo.v`, other targets are `{checker,coqide,coqtop}`:

```
dune exec -- dev/dune-dbg checker foo.vo
(ocd) source 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`.

### Debugging hints

- To debug a failure/error/anomaly, add a breakpoint in
  `Vernacinterp.interp_gen` (in `vernac/vernacinterp.ml`) at the with
  clause of the "try ... with ..." block, then go "back" a few steps
  to find where the failure/error/anomaly has been raised

- Alternatively, for an error or an anomaly, add breakpoints where it
  was raised (eg in `user_err` or `anomaly` in `lib/cErrors.ml`, or
  the functions in `pretyping/pretype_errors.ml`, or other raises
  depending on the error)

- If there is a linking error (eg from "source db"), do a "dune
  build coq-core.install" and try again.

## Dropping from coqtop:

The following commands should work:
```
dune exec -- dev/shim/coqbyte-prelude
> Drop.
# #directory "dev";;
# #use "include";;
```

## 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.

## OPAM file generation

`.opam` files are automatically generated by Dune from the package
descriptions in the `dune-project` file; see Dune's manual for more
details.

## 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.

## Dune cheat sheet

- `dune build` build all targets in the current workspace
- `dune build @check` build all ML targets as fast as possible, setup merlin
- `dune 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 name
- `dune build _build/$context/$foo` build target `$foo$` in `$context`, with build dir layout
- `dune build _build/install/$context/foo` build target `$foo$` in `$context`, with install dir layout

### packaging:

- `dune subst` generate metadata for a package to be installed / distributed, necessary for opam
- `dune build -p $pkg` build a package in release mode