22 files changed, 305 insertions, 119 deletions

diff --git a/dev/ci/README.md b/dev/ci/README.md
index bb13587e94..697a160ca9 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -36,9 +36,8 @@ On the condition that:
 - You do not push, to the branches that we test, commits that haven't been
   first tested to compile with the corresponding branch(es) of Coq.
 
-- Your development compiles in less than 35 minutes with just two threads.
-  If this is not the case, consider adding a "lite" target that compiles just
-  part of it.
+- You maintain a reasonable build time for your development, or you provide
+  a "lite" target that we can use.
 
 In case you forget to comply with these last three conditions, we would reach
 out to you and give you a 30-day grace period during which your development
@@ -54,9 +53,10 @@ Add a new `ci-mydev.sh` script to [`dev/ci`](/dev/ci) (have a look at
 set the corresponding variables in
 [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh); add the corresponding
 target to [`Makefile.ci`](/Makefile.ci); add new jobs to
-[`.travis.yml`](/.travis.yml) and [`.gitlab-ci.yml`](/.gitlab-ci.yml) so that
-this new target is run. **Do not hesitate to submit an incomplete pull request
-if you need help to finish it.**
+[`.gitlab-ci.yml`](/.gitlab-ci.yml),
+[`.circleci/config.yml`](/.circleci/config.yml) and
+[`.travis.yml`](/.travis.yml) so that this new target is run. **Do not
+hesitate to submit an incomplete pull request if you need help to finish it.**
 
 You may also be interested in having your development tested in our
 performance benchmark. Currently this is done by providing an OPAM package
@@ -71,62 +71,110 @@ When you submit a pull request (PR) on Coq GitHub repository, this will
 automatically launch a battery of CI tests. The PR will not be integrated
 unless these tests pass.
 
-Currently, we have two CI platforms:
+We are currently running tests on the following platforms:
 
-- Travis is the main CI platform. It tests the compilation of Coq, of the
+- GitLab CI is the main CI platform. It tests the compilation of Coq, of the
   documentation, and of CoqIDE on Linux with several versions of OCaml /
   camlp5, and with warnings as errors; it runs the test-suite and tests the
-  compilation of several external developments. It also tests the compilation
-  of Coq on OS X.
+  compilation of several external developments.
+
+- Circle CI runs tests that are redundant with GitLab CI and may be removed
+  eventually.
+
+- Travis CI is used to test the compilation of Coq and run the test-suite on
+  macOS. It also runs a linter that checks whitespace discipline. A
+  [pre-commit hook](/dev/tools/pre-commit) is automatically installed by
+  `./configure`. It should allow complying with this discipline without pain.
 
 - AppVeyor is used to test the compilation of Coq and run the test-suite on
   Windows.
 
-You can anticipate the results of these tests prior to submitting your PR
-by having them run of your fork of Coq, on GitHub or GitLab. This can be
-especially helpful given that our Travis platform is often overloaded and
-therefore there can be a significant delay before these tests are actually
-run on your PR. To take advantage of this, simply create a Travis account
-and link it to your GitHub account, or activate the pipelines on your GitLab
-fork.
+You can anticipate the results of most of these tests prior to submitting your
+PR by running GitLab CI on your private branches. To do so follow these steps:
 
-You can also run one CI target locally (using `make ci-somedev`).
+1. Log into GitLab CI (the easiest way is to sign in with your GitHub account).
+2. Click on "New Project".
+3. Choose "CI / CD for external repository" then click on "GitHub".
+4. Find your fork of the Coq repository and click on "Connect".
+5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project).
+6. You are encouraged to go to the CI / CD general settings and increase the
+   timeout from 1h to 2h for better reliability.
 
-Whenever your PR breaks tested developments, you should either adapt it
-so that it doesn't, or provide a branch fixing these developments (or at
-least work with the author of the development / other Coq developers to
-prepare these fixes). Then, add an overlay in
-[`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there)
-in a separate commit in your PR.
+Now everytime you push (including force-push unless you changed the default
+GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and
+CI will be run. You will receive an e-mail with a report of the failures if
+there are some.
 
-The process to merge your PR is then to submit PRs to the external
-development repositories, merge the latter first (if the fixes are
-backward-compatible), drop the overlay commit and merge the PR on Coq then.
+You can also run one CI target locally (using `make ci-somedev`).
 
 See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
 
-
-Travis specific information
----------------------------
-
-Travis rebuilds all of Coq's executables and stdlib for each job. Coq
-is built with `./configure -local`, then used for the job's test.
-
-
-GitLab specific information
----------------------------
-
-GitLab is set up to use the "build artifact" feature to avoid
-rebuilding Coq. In one job, Coq is built with `./configure -prefix
-install` and `make install` is run, then the `install` directory
+### Breaking changes
+
+When your PR breaks an external project we test in our CI, you must prepare a
+patch (or ask someone to prepare a patch) to fix the project:
+
+1. Fork the external project, create a new branch, push a commit adapting
+   the project to your changes.
+2. Test your pull request with your adapted version of the external project by
+   adding an overlay file to your pull request (cf.
+   [`dev/ci/user-overlays/README.md`](/dev/ci/user-overlays/README.md)).
+3. Fixes to external libraries (pure Coq projects) *must* be backward
+   compatible (i.e. they should also work with the development version of Coq,
+   and the latest stable version). This will allow you to open a PR on the
+   external project repository to have your changes merged *before* your PR on
+   Coq can be integrated.
+
+   On the other hand, patches to plugins (projects linking to the Coq ML API)
+   can very rarely be made backward compatible and plugins we test will
+   generally have a dedicated branch per Coq version.
+   You can still open a pull request but the merging will be requested by the
+   developer who merges the PR on Coq. There are plans to improve this, cf.
+   [#6724](https://github.com/coq/coq/issues/6724).
+
+Moreover your PR must absolutely update the [`CHANGES`](/CHANGES) file.
+
+Advanced GitLab CI information
+------------------------------
+
+GitLab CI is set up to use the "build artifact" feature to avoid
+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:
 - the Coq executables and stdlib, in three copies varying in
-  architecture and Ocaml version used to build Coq.
-- the Coq documentation, in two different copies varying in the OCaml
-  version used to build Coq
+  architecture and OCaml version used to build Coq.
+- the Coq documentation, built only in the `build:base` job. When submitting
+  a documentation PR, this can help reviewers checking the rendered result.
 
 As an exception to the above, jobs testing that compilation triggers
-no Ocaml warnings build Coq in parallel with other tests.
+no OCaml warnings build Coq in parallel with other tests.
+
+### GitLab and Windows
+
+If your repository has access to runners tagged `windows`, setting the
+secret variable `WINDOWS` to `enabled` will add jobs building Windows
+versions of Coq (32bit and 64bit).
+
+The Windows jobs are enabled on Coq's repository, where pipelines for
+pull requests run.
+
+### GitLab and Docker
+
+System and opam packages are installed in a Docker image. The image is
+automatically built and uploaded to your GitLab registry, and is
+loaded by subsequent jobs.
+
+**IMPORTANT**: When updating Coq's CI docker image, you must modify
+the `CACHEKEY` variable in `.gitlab-ci.yml`, `.circleci/config.yml`,
+and `Dockerfile`.
+
+The Docker building job reuses the uploaded image if it is available,
+but if you wish to save more time you can skip the job by setting
+`SKIP_DOCKER` to `true`.
+
+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.
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index 93e7bd99ab..7bf9ad8c9b 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -1,9 +1,15 @@
 #!/bin/bash
+
 set -e -x
+
+APPVEYOR_OPAM_SWITCH=4.06.1+mingw64c
+
 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz
 tar -xf opam64.tar.xz
 bash opam64/install.sh
-opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
+
+opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH
 eval "$(opam config env)"
-opam install -y ocamlfind camlp5
+opam install -y num ocamlfind camlp5 ounit
+
 cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index b7faea13ed..87d837b387 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -11,6 +11,8 @@
 ########################################################################
 : "${mathcomp_CI_BRANCH:=master}"
 : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}"
+: "${oddorder_CI_BRANCH:=master}"
+: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order.git}"
 
 ########################################################################
 # UniMath
@@ -168,3 +170,15 @@
 ########################################################################
 : "${pidetop_CI_BRANCH:=v8.9}"
 : "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}"
+
+########################################################################
+# ext-lib
+########################################################################
+: "${ext_lib_CI_BRANCH:=master}"
+: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib.git}"
+
+########################################################################
+# quickchick
+########################################################################
+: "${quickchick_CI_BRANCH:=master}"
+: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick.git}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 189734a0bc..5b5cbd11ae 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -8,8 +8,13 @@ export NJOBS
 
 if [ -n "${GITLAB_CI}" ];
 then
+    export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH"
     export COQBIN="$PWD/_install_ci/bin"
     export CI_BRANCH="$CI_COMMIT_REF_NAME"
+    if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]
+    then
+        export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
+    fi
 else
     if [ -n "${TRAVIS}" ];
     then
@@ -23,6 +28,7 @@ else
         CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
         export CI_BRANCH
     fi
+    export OCAMLPATH="$PWD:$OCAMLPATH"
     export COQBIN="$PWD/bin"
 fi
 export PATH="$COQBIN:$PATH"
@@ -67,11 +73,6 @@ git_checkout()
     echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
 }
 
-checkout_mathcomp()
-{
-  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}"
-}
-
 make()
 {
     # +x: add x only if defined
@@ -89,7 +90,8 @@ install_ssreflect()
 {
   echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
 
-  checkout_mathcomp "${mathcomp_CI_DIR}"
+  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+
   ( cd "${mathcomp_CI_DIR}/mathcomp" && \
     sed -i.bak '/ssrtest/d'     Make && \
     sed -i.bak '/odd_order/d'   Make && \
diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext-lib.sh
new file mode 100755
index 0000000000..cf212c2fb5
--- /dev/null
+++ b/dev/ci/ci-ext-lib.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+
+# This script could be included inside other ones
+# Let's avoid to source ci-common twice in this case
+if [ -z "${CI_BUILD_DIR}" ];
+then
+    . "${ci_dir}/ci-common.sh"
+fi
+
+ext_lib_CI_DIR="${CI_BUILD_DIR}/ExtLib"
+
+git_checkout "${ext_lib_CI_BRANCH}" "${ext_lib_CI_GITURL}" "${ext_lib_CI_DIR}"
+
+( cd "${ext_lib_CI_DIR}" && make && make install)
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 845addb4cd..48a1366aba 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -6,6 +6,9 @@ ci_dir="$(dirname "$0")"
 fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto"
 
 git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}"
+
 ( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
 
-( cd "${fiat_crypto_CI_DIR}" && make lite lite-display )
+fiat_crypto_CI_TARGETS1="printlite lite lite-display"
+fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index bd1d88993c..920272bcfb 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -7,6 +7,4 @@ GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq"
 
 git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}"
 
-( cd "${GeoCoq_CI_DIR}"                                     && \
-  ./configure-ci.sh                                       && \
-  make )
+( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 4fc06e8956..6a064b2971 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -7,4 +7,4 @@ math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes"
 
 git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}"
 
-( cd "${math_classes_CI_DIR}" && make && make install )
+( cd "${math_classes_CI_DIR}" && ./configure.sh && make && make install )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 8c6b910bbb..20328baf2a 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -5,11 +5,10 @@ ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
 mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
+oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order"
 
-checkout_mathcomp "${mathcomp_CI_DIR}"
+git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}"
 
-# odd_order takes too much time for travis.
-( cd "${mathcomp_CI_DIR}/mathcomp"                  && \
-  sed -i.bak '/PFsection/d'                  Make && \
-  sed -i.bak '/stripped_odd_order_theorem/d' Make && \
-  make Makefile.coq && make -f Makefile.coq all )
+( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install )
+( cd "${oddorder_CI_DIR}/" && make )
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
index d04b9637c0..32cba0808e 100755
--- a/dev/ci/ci-pidetop.sh
+++ b/dev/ci/ci-pidetop.sh
@@ -8,6 +8,15 @@ pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop"
 
 git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}"
 
-( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top )
+# Travis / Gitlab have different filesystem layout due to use of
+# `-local`. We need to improve this divergence but if we use Dune this
+# "local" oddity goes away automatically so not bothering...
+if [ -d "$COQBIN/../lib/coq" ]; then
+   COQLIB="$COQBIN/../lib/coq/"
+else
+   COQLIB="$COQBIN/../"
+fi
 
-echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop
+( cd "${pidetop_CI_DIR}" && jbuilder build @install )
+
+echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh
new file mode 100755
index 0000000000..fc39e2685d
--- /dev/null
+++ b/dev/ci/ci-quickchick.sh
@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+
+# This script could be included inside other ones
+# Let's avoid to source ci-common twice in this case
+if [ -z "${CI_BUILD_DIR}" ];
+then
+    . "${ci_dir}/ci-common.sh"
+fi
+
+quickchick_CI_DIR="${CI_BUILD_DIR}/Quickchick"
+
+install_ssreflect
+
+git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}"
+
+( cd "${quickchick_CI_DIR}" && make && make install)
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 62a949f59a..aa20fe1ff0 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -7,7 +7,4 @@ UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath"
 
 git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}"
 
-( cd "${UniMath_CI_DIR}"                        && \
-  sed -i.bak '/Folds/d'              Makefile && \
-  sed -i.bak '/HomologicalAlgebra/d' Makefile && \
-  make BUILD_COQ=no )
+( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no )
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 79001c547b..7a097eaab4 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -5,9 +5,6 @@ ci_dir="$(dirname "$0")"
 
 VST_CI_DIR="${CI_BUILD_DIR}/VST"
 
-# opam install -j ${NJOBS} -y menhir
 git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}"
 
-# We have to omit progs as otherwise we timeout on Travis; on Gitlab
-# we will be able to just use `make`
-( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true -o progs )
+( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true )
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
index 8e677f6f2b..919e2a735f 100644
--- a/dev/ci/docker/README.md
+++ b/dev/ci/docker/README.md
@@ -1,37 +1,13 @@
 ## Overall Docker Setup for Coq's CI.
 
 This directory provides Docker images to be used by Coq's CI. The
-images do support Docker autobuild on `hub.docker.com`
+images do support Docker autobuild on `hub.docker.com` and Gitlab's
+private registry.
 
-Autobuild is the preferred build method [see below]; if you are a
-member of the `coqci` organization, the automated build will push the
-image to the `coqci/name:$VERSION` tag using a Docker hub hook.
-
-## Updating the Image and Syncronization with CI files
-
-Unfortunately, at this point some manual synchronization is needed
-between the `Dockerfile` and `.gitlab-ci.yml`. In particular, the
-checklist is:
-
-- check the name and version of the image setup in `hooks/post_push`
-  have to match.
-- check `COMPILER` variables do match.
-
-Once you are sure the variables are right, then proceed to trigger an
-autobuild or do a manual build, et voilà !
-
-## Docker Autobuilding.
-
-We provide basic support for auto-building, see:
-
-https://docs.docker.com/docker-cloud/builds/advanced/
-
-If you are member of the `coqci` Docker organization, trigger an
-autobuild in your account and the image will be pushed to it as we
-set the proper tag in `hooks/post_push`.
-
-We still need to figure out how properly setup a more automated,
-organization-wide auto-building process.
+Gitlab CI will build and tag a Docker by default for every job if the
+`SKIP_DOCKER` variable is not set to `false`. In Coq's CI, this
+variable is usually set to `false` indeed to avoid booting a useless
+job.
 
 ## Manual Building
 
@@ -47,10 +23,6 @@ To upload/push to your hub:
   + `docker tag base:$VERSION $USER/base:$VERSION`
   + `docker push $USER/base:$VERSION`
 
-Now your docker image is ready to be used. To upload to `coqci`:
-- `docker tag base:$VERSION coqci/base:$VERSION`
-- `docker push coqci/base:$VERSION`
-
 ## Debugging / Misc
 
 To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>`
@@ -62,4 +34,3 @@ end.
 ## Possible Improvements:
 
 - Use ARG for customizing versions, centralize variable setup;
-- Learn more about Docker registry for GITLAB https://gitlab.com/coq/coq/container_registry .
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 689d203a16..a1178ee2a0 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,3 +1,6 @@
+# CACHEKEY: "bionic_coq-V2018-05-07-V2"
+# ^^ Update when modifying this file.
+
 FROM ubuntu:bionic
 LABEL maintainer="e@x80.org"
 
diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push
deleted file mode 100755
index 307680aa51..0000000000
--- a/dev/ci/docker/bionic_coq/hooks/post_push
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-COQCI_VERSION=V2018-05-07-V2
-docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION
-docker push $DOCKER_REPO:$COQCI_VERSION
-
-docker tag $IMAGE_NAME coqci/base:$COQCI_VERSION
-docker push coqci/base:$COQCI_VERSION
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
new file mode 100644
index 0000000000..70278e6d09
--- /dev/null
+++ b/dev/ci/gitlab.bat
@@ -0,0 +1,50 @@
+@ECHO OFF
+
+REM This script builds and signs the Windows packages on Gitlab
+
+if %ARCH% == 32 (
+  SET ARCHLONG=i686
+  SET CYGROOT=C:\cygwin
+  SET SETUP=setup-x86.exe
+)
+
+if %ARCH% == 64 (
+  SET ARCHLONG=x86_64
+  SET CYGROOT=C:\cygwin64
+  SET SETUP=setup-x86_64.exe
+)
+
+powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
+SET CYGCACHE=%CYGROOT%\var\cache\setup
+SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
+SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
+SET DESTCOQ=C:\coq%ARCH%_inst
+SET COQREGTESTING=Y
+SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
+
+if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
+if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
+
+call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
+  -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
+  -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+  -addon=bignums -make=N ^
+  -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorExit
+
+copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
+7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+
+REM DO NOT echo the signing command below, as this would leak secrets in the logs
+IF DEFINED WIN_CERTIFICATE_PATH (
+  IF DEFINED WIN_CERTIFICATE_PASSWORD (
+    ECHO Signing package
+    @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe
+    signtool verify /pa dev\nsis\*.exe
+  )
+)
+
+GOTO :EOF
+
+:ErrorExit
+  ECHO ERROR %0 failed
+  EXIT /b 1
diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
new file mode 100644
index 0000000000..b22ab36302
--- /dev/null
+++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
@@ -0,0 +1,9 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top"   ] ||     \
+   [ "$CI_PULL_REQUEST" = "7543" ] || [ "$CI_BRANCH" = "ide+split" ] ; then
+
+    pidetop_CI_BRANCH=stm+top
+    pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git
+
+fi
diff --git a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh
new file mode 100644
index 0000000000..ea9cd8ee07
--- /dev/null
+++ b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh
@@ -0,0 +1,21 @@
+if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then
+
+    # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550
+    #
+    # equations
+    # ltac2
+
+    # The below developments should instead use a backwards compatible fix.
+    #
+    # color
+    # iris-lambda-rust
+    # math-classes
+    # formal-topology
+
+    ltac2_CI_BRANCH=tactics+push_fix_naming_out
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    Equations_CI_BRANCH=tactics+push_fix_naming_out
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh
new file mode 100644
index 0000000000..517088a247
--- /dev/null
+++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then
+
+    ltac2_CI_BRANCH=fast-constr-match-no-context
+    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
+
+fi
diff --git a/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh
new file mode 100644
index 0000000000..115f29f1ee
--- /dev/null
+++ b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh
@@ -0,0 +1,14 @@
+if [ "$CI_PULL_REQUEST" = "7558" ] || [ "$CI_BRANCH" = "vernac+move_parser" ]; then
+
+    _OVERLAY_BRANCH=vernac+move_parser
+
+    Equations_CI_BRANCH="$_OVERLAY_BRANCH"
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    ltac2_CI_BRANCH="$_OVERLAY_BRANCH"
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    mtac2_CI_BRANCH="$_OVERLAY_BRANCH"
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index a7474e3248..aec2dfe0a6 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -1,8 +1,21 @@
 # Add overlays for your pull requests in this directory
 
-An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh).
+When your pull request breaks an external project we test in our CI and you
+have prepared a branch with the fix, you can add an "overlay" to your pull
+request to test it with the adapted version of the external project.
 
-The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`.
+An overlay is a file which defines where to look for the patched version so that
+testing is possible. It redefines some variables from
+[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh):
+give the name of your branch using a `_CI_BRANCH` variable and the location of
+your fork using a `_CI_GITURL` variable.
+
+Moreover, the file contains very simple logic to test the pull request number
+or branch name and apply it only in this case.
+
+The name of your overlay file should start with a five-digit pull request
+number, followed by a dash, anything (for instance your GitHub nickname
+and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`).
 
 Example: `00669-maximedenes-ssr-merge.sh` containing