Merge PR #6857: [build] Preliminary support for building with `dune`.

4 files changed, 129 insertions, 8 deletions

diff --git a/dev/ci/README.md b/dev/ci/README.md
index b4ea6838bf..95892ebe0a 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -156,6 +156,9 @@ Currently available artifacts are:
   architecture and OCaml version used to build Coq:
   https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base
 
+  Additionally, an experimental Dune build is provided:
+  https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune
+
 - the Coq documentation, built in the `doc:*` jobs. When submitting
   a documentation PR, this can help reviewers checking the rendered result:
 
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
index d22b9c8f7c..1a9a26843c 100755
--- a/dev/ci/ci-pidetop.sh
+++ b/dev/ci/ci-pidetop.sh
@@ -14,6 +14,6 @@ else
    COQLIB="$COQBIN/../"
 fi
 
-( cd "${CI_BUILD_DIR}/pidetop" && jbuilder build @install )
+( cd "${CI_BUILD_DIR}/pidetop" && dune build -p pidetop @install )
 
 echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index abba13428f..b0a2b04121 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -1,5 +1,3 @@
-
-
 HISTORY:
 -------
 
@@ -35,13 +33,41 @@ HISTORY:
   grammar.cma (and q_constr.cmo) directly, no need for a separate
   subcall to make nor awkward include-failed-and-retry.
 
-    
----------------------------------------------------------------------------
+* February - September 2018 (Emilio Jesús Gallego Arias)
+
+  Dune support added.
+
+  The build setup is mostly vanilla for the OCaml part, however the
+  `.v` to `.vo` compilation relies on `coq_dune` a `coqdep` wrapper
+  that will generate the necessary `dune` files.
+
+  As a developer, you should not have to deal with Dune configuration
+  files on a regular basis unless adding a new library or plugin.
 
+  The vanilla setup declares all the Coq libraries and binaries [we
+  must respect proper containment/module implementation rules as to
+  allow packing], and we build custom preprocessors (based on `camlp5`
+  and `coqpp`) that will process the `ml4`/`mlg` files.
+
+  This suffices to build `coqtop` and `coqide`, all that remains to
+  handle is `.vo` compilation.
+
+  To teach Dune about the `.vo`, we use a small utility `coq_dune`,
+  that will generate a `dune` file for each directory in `plugins` and
+  `theories`. The code is pretty straightforward and declares build
+  and install rules for each `.v` straight out of `coqdep`. Thus, our
+  build strategy looks like this:
+
+  1. Use `dune` to build `coqdep` and `coq_dune`.
+  2. Use `coq_dune` to generate `dune` files for each directory with `.v` files.
+  3. ?
+  4. Profit! [Seriously, at this point Dune has all the information to build Coq]
+
+---------------------------------------------------------------------------
 
-This file documents internals of the implementation of the build
-system. For what a Coq developer needs to know about the build system,
-see build-system.txt .
+This file documents internals of the implementation of the make-based
+build system. For what a Coq developer needs to know about the build
+system, see build-system.txt and build-system.dune.md .
 
 .ml4 files
 ----------
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
new file mode 100644
index 0000000000..0b3e414513
--- /dev/null
+++ b/dev/doc/build-system.dune.md
@@ -0,0 +1,92 @@
+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.
+
+## 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.