1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
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.
Dune
====
Coq can now be built using
[Dune](https://github.com/ocaml/dune). 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 link order. You are
are not supposed to modify the `dune` files unless you are adding a
new binary, library, or plugin.
The current Dune setup also doesn't require a call to `configure`. The
auto-generated configuration files are properly included in the
dependency graph so it will be automatically generated by Dune with
reasonable developer defaults. You can still override the defaults by
manually calling `./configure`, but note that some configure options
such as install paths are not used by Dune.
Dune uses a separate directory `_build` to store build artifacts; it
will generate an `.install` file so artifacts in the build can be
properly installed by package managers.
## 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`.
In order to build a single package, you can do `dune build
$PACKAGE.install`. Dune also provides targets for documentation and
testing, see below.
## 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.
## 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.
## 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.
## Documentation and test targets
The documentation and test suite targets for Coq are still not
implemented in Dune.
## 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.
|
