5 files changed, 48 insertions, 9 deletions
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/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