9 files changed, 191 insertions, 17 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 60108cda4f..8a49b97dac 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1448,10 +1448,10 @@ function make_addons {
     export CI_BRANCH=""
     export CI_PULL_REQUEST=""
   fi
-  . /build/ci-basic-overlay.sh
   for overlay in /build/user-overlays/*.sh; do
     . "$overlay"
   done
+  . /build/ci-basic-overlay.sh
 
   for addon in $COQ_ADDONS; do
     "make_addon_$addon"
diff --git a/dev/ci/README.md b/dev/ci/README.md
index a814e4914e..95892ebe0a 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -136,12 +136,38 @@ rebuilding Coq. In one job, Coq is built with `./configure -prefix _install_ci`
 and `make install` is run, then the `_install_ci` directory
 persists to and is used by the next jobs.
 
-Artifacts can also be downloaded from the GitLab repository.
-Currently, available artifacts are:
+### Artifacts
+
+Build artifacts from GitLab can be linked / downloaded in a systematic
+way, see [GitLab's documentation](https://docs.gitlab.com/ce/user/project/pipelines/job_artifacts.html#downloading-the-latest-job-artifacts)
+for more information. For example, to access the documentation of the
+`master` branch, you can do:
+
+https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman
+
+Browsing artifacts is also possible:
+https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base
+
+Above, you can replace `master` and `job` by the desired GitLab branch and job name.
+
+Currently available artifacts are:
+
 - the Coq executables and stdlib, in four copies varying in
-  architecture and OCaml version used to build Coq.
-- the Coq documentation, built in the `documentation` job. When submitting
-  a documentation PR, this can help reviewers checking the rendered result.
+  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:
+
+  + Coq's Reference Manual [master branch]
+    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman
+  + Coq's Standard Library Documentation [master branch]
+    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=doc:refman
+  + Coq's ML API Documentation [master branch]
+    https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api
 
 ### GitLab and Windows
 
@@ -168,6 +194,6 @@ but if you wish to save more time you can skip the job by setting
 
 This means you will need to change its value when the Docker image
 needs to be updated. You can do so for a single pipeline by starting
-it through the web interface..
+it through the web interface.
 
 See also [`docker/README.md`](docker/README.md).
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 3536cc70b2..7af648f0a6 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -37,12 +37,12 @@ ls "$COQBIN"
 # Where we download and build external developments
 CI_BUILD_DIR="$PWD/_build_ci"
 
-# shellcheck source=ci-basic-overlay.sh
-. "${ci_dir}/ci-basic-overlay.sh"
 for overlay in "${ci_dir}"/user-overlays/*.sh; do
     # shellcheck source=/dev/null
     . "${overlay}"
 done
+# shellcheck source=ci-basic-overlay.sh
+. "${ci_dir}/ci-basic-overlay.sh"
 
 # [git_download project] will download [project] and unpack it
 # in [$CI_BUILD_DIR/project] if the folder does not exist already;
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/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh
new file mode 100644
index 0000000000..575df07425
--- /dev/null
+++ b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh
@@ -0,0 +1,8 @@
+_OVERLAY_BRANCH=pure-sharing-flag
+
+if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
+
+    mtac2_CI_BRANCH="$_OVERLAY_BRANCH"
+    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh
new file mode 100644
index 0000000000..3a6480a5a1
--- /dev/null
+++ b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "7288" ] || [ "$CI_BRANCH" = "master+new-module-pretyping-id-management" ]; then
+
+    ltac2_CI_BRANCH=master+globenv-coq-pr7288
+    ltac2_CI_GITURL=https://github.com/herbelin/ltac2
+
+fi
diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh
new file mode 100644
index 0000000000..76aa37d380
--- /dev/null
+++ b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh
@@ -0,0 +1,5 @@
+if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then
+    HoTT_CI_REF=fix-for-numeral-notations
+    HoTT_CI_GITURL=https://github.com/JasonGross/HoTT
+    HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive
+fi
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..85aaf317ef
--- /dev/null
+++ b/dev/doc/build-system.dune.md
@@ -0,0 +1,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.