11 files changed, 79 insertions, 27 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 87f03aa99..dee3d2aff 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -96,7 +96,8 @@ PR by running GitLab CI on your private branches. To do so follow these steps:
 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. You are encouraged to go to the CI / CD general settings and increase the
+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.
 
 Now everytime you push (including force-push unless you changed the default
@@ -137,3 +138,27 @@ Currently, available artifacts are:
 
 As an exception to the above, jobs testing that compilation triggers
 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.
+
+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 93e7bd99a..c72705c7f 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -5,5 +5,5 @@ 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
 eval "$(opam config env)"
-opam install -y ocamlfind camlp5
+opam install -y 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 b7faea13e..5c882ee85 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
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 2a14ed352..f867fd189 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -71,11 +71,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
@@ -93,7 +88,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-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 845addb4c..5d96c2499 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -6,6 +6,8 @@ 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_TARGETS="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index bd1d88993..920272bcf 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-comp.sh b/dev/ci/ci-math-comp.sh
index 8c6b910bb..20328baf2 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-unimath.sh b/dev/ci/ci-unimath.sh
index 62a949f59..aa20fe1ff 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 79001c547..7a097eaab 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/doc/changes.md b/dev/doc/changes.md
index 6d7c0d368..fb3f751db 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -22,6 +22,11 @@ Proof engine
   should indicate what the canonical form is. An important change is
   the move of `Globnames.global_reference` to `Names.GlobRef.t`.
 
+### Unit testing
+
+  The test suite now allows writing unit tests against OCaml code in the Coq
+  code base. Those unit tests create a dependency on the OUnit test framework.
+
 ## Changes between Coq 8.7 and Coq 8.8
 
 ### Bug tracker
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 9dd12087a..70a9756e5 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -23,7 +23,7 @@
 
 ;; If you load this file from a git repository, checking out an old
 ;; commit will make it disappear and cause errors for your Emacs
-;; startup. To ignore those errors use (require 'coqdev nil t). If you
+;; startup.  To ignore those errors use (require 'coqdev nil t).  If you
 ;; check out a malicious commit Emacs startup would allow it to run
 ;; arbitrary code, to avoid this you can copy coqdev.el to any
 ;; location and adjust the load path accordingly (of course if you run
@@ -115,5 +115,36 @@ This does not enable `bug-reference-mode'."
       (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s"))))
 (add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode)
 
+(defun coqdev-sphinx-quote-coq-refman-region (left right &optional offset beg end)
+  "Add LEFT and RIGHT around the BEG..END.
+Leave the point after RIGHT.  BEG and END default to the bounds
+of the current region.  Leave point OFFSET characters after the
+left quote (if OFFSET is nil, leave the point after the right
+quote)."
+  (unless beg
+    (if (region-active-p)
+        (setq beg (region-beginning) end (region-end))
+      (setq beg (point) end nil)))
+  (save-excursion
+    (goto-char (or end beg))
+    (insert right))
+  (save-excursion
+    (goto-char beg)
+    (insert left))
+  (if (and end (not offset)) ;; Second test handles the ::`` case
+      (goto-char (+ end (length left) (length right)))
+    (goto-char (+ beg (or offset (length left))))))
+
+(defun coqdev-sphinx-rst-coq-action ()
+  "Insert a Sphinx role template or quote the current region."
+  (interactive)
+  (pcase (read-char "Command [gntm:`]?")
+    (?g (coqdev-sphinx-quote-coq-refman-region ":g:`" "`"))
+    (?n (coqdev-sphinx-quote-coq-refman-region ":n:`" "`"))
+    (?t (coqdev-sphinx-quote-coq-refman-region ":token:`" "`"))
+    (?m (coqdev-sphinx-quote-coq-refman-region ":math:`" "`"))
+    (?: (coqdev-sphinx-quote-coq-refman-region "::`" "`" 1))
+    (?` (coqdev-sphinx-quote-coq-refman-region "``" "``"))))
+
 (provide 'coqdev)
 ;;; coqdev ends here