This file documents what a Rocq developer needs to know about the
Dune-based build system.

About Dune
==========

Rocq uses the [Dune](https://github.com/ocaml/dune) build system.

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

It is strongly recommended that you use the helper targets available
in `Makefile`, `make` will display help. Note that dune will call
configure for you if needed, so no need to call `./configure` in the
regular development workflow, unless you want to tweak options.


2 common operations are:

- `make check` : build all ml targets as fast as possible
- `make world` : build a complete Rocq distribution

For more targeted builds, you can also call `dune` directly. First,
call `make dunestrap` to generate necessary build files (the `make`
targets above do it automatically). Then you can use:

- `dune exec -- dev/shim/coqtop` : build and launch coqtop + prelude
  [equivalent to `make states`].
- `dune exec -- dev/shim/coqc <args...>`: build and launch `coqc` with
  arguments of your choice
- `dune build $target`: where `$target` can refer to the build
  directory or the source directory [but will be placed under
  `_build`]

You need to run `make dunestrap` again if the dependencies between the
core library .v files have changed.

`dune build @install` will build all the public Rocq artifacts; `dune
build` builds the `@default` alias, defined in the top level `dune` file.

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.

## The bootstrap process / rule generation

Dune is able to build all the OCaml parts of Rocq in a pretty standard
way, using its built-in rule generation for OCaml. Public tools
written in OCaml are distributed in the `rocq-runtime` package.

The set of public `.v` files present in this repository, usually
referred as the "Rocq prelude" are distributed in the
`rocq-core` package. As of June 2022, Dune has a set of built-in
rules for `.v` files which is capable of building Rocq's core
library.

However, in order to have a bit more control, we generate ourselves a
set of custom rules using the `tools/dune_rule_gen` binary, which are
then stored in the `theories/dune` file. This allows us to have a
finer control over the build rules without having to bump the Dune
version. The generation of the `theories/dune` and
`user-contrib/*/dune` files is known as "bootstrap".

The rule generation code in `tools/dune_rule_gen` is mostly derived
from Dune's built-in rules, and it works in an straightforward way: it
will scan a directory with `.v` files in it, and output the
corresponding build rule. The script will look at some configuration
values such as whether native is enabled or not and adapt rule
generation accordingly.

In the case of native, the script supports two modes, `coqc
-native-compiler on` and `coqnative`. The default is the first, as
currently `coqnative` incurs a 33% build time overhead on a powerful
16-core machine.

There are several modes for the rule generation script to work,
depending on the parameter passed. As of today, it support `-async`.

`-async` will pass `-async-proofs on` to `coqc`.

## 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 / rocqide]

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 Rocq'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
`rocqide` in a fast build. In order to use them, do:

```
$ dune exec -- dev/shim/coqtop
```

or `quickide` / `dev/shim/rocqide` for RocqIDE, 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 core library with the `world` target,
then you can run the commands in the
`_build/install/default/bin` directories (including `coq_makefile`).

## Building custom toplevels

You can build custom toplevels by tweaking the `toplevel/dune` files,
for example, to add plugins to be linked statically using the
`(libraries ...)` field.

Note that Rocq relies on a hidden Dune hack, which will add `-linkall`
to binaries if they depend on the `findlib.dynload` library. As of
today, `rocq-runtime.vernac` uses `findlib.dynload`, so if your toplevel
hooks at the `rocq-runtime.vernac` or above level, you should be OK,
otherwise add `-linkall` to Dune's `(link_flags ...)` field for your
binary.

## Targets

The default dune target is `dune build` (or `dune build @install`),
which will scan all sources in the Rocq 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 Rocq with `make 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
  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.

## 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,rocqide,coqtop}`:

```
dune exec -- dev/dune-dbg checker foo.vo
(ocd) source db
```

More info in the [wiki](https://github.com/coq/coq/wiki/OCamldebug).

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 rocq-runtime.install" and try again.

## Dropping from coqtop:

The following commands should work:
```
dune exec -- dev/shim/coqtop.byte
> Drop.
```

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

This is very useful to develop plugins and Rocq 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 Rocq source tree contains two packages [Rocq and RocqIDE], and in
the OPAM RocqIDE package we don't want to build RocqIDE against the
local copy of Rocq. For this purpose, Dune supports the `-p` option, so
`dune build -p rocqide` will build RocqIDE against the system-installed
version of Rocq libs, and use a "release" profile that for example
enables stronger compiler optimizations.

## OPAM file generation

`.opam` files will be automatically generated by Dune from the package
descriptions in the `dune-project` file; see Dune's manual for more
details. For now we have disabled this due to some bugs.

## 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 Rocq
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 Rocq
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 Rocq, 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 / rocqide]" section above as to how to correctly call Rocq'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