11 files changed, 256 insertions, 45 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index bb13587e9..87f03aa99 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,24 +71,38 @@ 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:
+
+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. 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
+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.
 
 You can also run one CI target locally (using `make ci-somedev`).
 
@@ -97,36 +111,29 @@ 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.
+as part of your PR.
 
 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.
+backward-compatible), and merge the PR on Coq then.
 
 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
----------------------------
+Advanced GitLab CI 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
+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.
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5566a5117..b7faea13e 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -19,13 +19,13 @@
 : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}"
 
 ########################################################################
-# Unicoq + Metacoq
+# Unicoq + Mtac2
 ########################################################################
 : "${unicoq_CI_BRANCH:=master}"
 : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}"
 
-: "${metacoq_CI_BRANCH:=master}"
-: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}"
+: "${mtac2_CI_BRANCH:=master-sync}"
+: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2.git}"
 
 ########################################################################
 # Mathclasses + Corn
@@ -91,6 +91,12 @@
 : "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}"
 
 ########################################################################
+# cross-crypto
+########################################################################
+: "${cross_crypto_CI_BRANCH:=master}"
+: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto.git}"
+
+########################################################################
 # fiat_parsers
 ########################################################################
 : "${fiat_parsers_CI_BRANCH:=master}"
@@ -156,3 +162,9 @@
 ########################################################################
 : "${fcsl_pcm_CI_BRANCH:=master}"
 : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}"
+
+########################################################################
+# pidetop
+########################################################################
+: "${pidetop_CI_BRANCH:=v8.9}"
+: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}"
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index fbdeff20c..8d490591b 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")"
 
 CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert"
 
-opam install -j "$NJOBS" -y menhir
 git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}"
 
 ( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh
new file mode 100755
index 000000000..a0d3aa655
--- /dev/null
+++ b/dev/ci/ci-cross-crypto.sh
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+cross_crypto_CI_DIR="${CI_BUILD_DIR}/cross-crypto"
+
+git_checkout "${cross_crypto_CI_BRANCH}" "${cross_crypto_CI_GITURL}" "${cross_crypto_CI_DIR}"
+( cd "${cross_crypto_CI_DIR}" && git submodule update --init --recursive )
+
+( cd "${cross_crypto_CI_DIR}" && make )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-mtac2.sh
index a66dc1e76..1372acb8e 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-mtac2.sh
@@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
 unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
+mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2
 
 # Setup UniCoq
 
@@ -14,6 +14,6 @@ git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
 
 # Setup MetaCoq
 
-git_checkout "${metacoq_CI_BRANCH}" "${metacoq_CI_GITURL}" "${metacoq_CI_DIR}"
+git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}"
 
-( cd "${metacoq_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
+( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
new file mode 100755
index 000000000..d04b9637c
--- /dev/null
+++ b/dev/ci/ci-pidetop.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+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 )
+
+echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 3c0044bfe..79001c547 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -8,6 +8,6 @@ VST_CI_DIR="${CI_BUILD_DIR}/VST"
 # opam install -j ${NJOBS} -y menhir
 git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}"
 
-# Targets are: msl veric floyd progs , we remove progs to save time
-# Patch to avoid the upper version limit
-( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true .loadpath version.vo msl veric floyd )
+# 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 )
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
new file mode 100644
index 000000000..8e677f6f2
--- /dev/null
+++ b/dev/ci/docker/README.md
@@ -0,0 +1,65 @@
+## 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`
+
+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.
+
+## Manual Building
+
+You can also manually build and push any image:
+
+- Build the image `docker build -t base:$VERSION .`
+
+To upload/push to your hub:
+
+- Create a https://hub.docker.com account.
+- Login into your space `docker login --username=$USER`
+- Push the image:
+  + `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>`
+
+Each `RUN` command creates an "layer", thus a Docker build is
+incremental and it always help to put things updated more often at the
+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
new file mode 100644
index 000000000..689d203a1
--- /dev/null
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -0,0 +1,46 @@
+FROM ubuntu:bionic
+LABEL maintainer="e@x80.org"
+
+ENV DEBIAN_FRONTEND="noninteractive"
+
+RUN apt-get update -qq && apt-get install -y -qq m4 wget time gcc-multilib opam \
+        libgtk2.0-dev libgtksourceview2.0-dev \
+        texlive-latex-extra texlive-fonts-recommended hevea \
+        python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip
+
+RUN pip3 install antlr4-python3-runtime
+
+# Basic OPAM setup
+ENV NJOBS="2" \
+    OPAMROOT=/root/.opamcache \
+    OPAMROOTISOK="true"
+
+# Base opam is the set of base packages required by Coq
+ENV COMPILER="4.02.3" \
+    BASE_OPAM="num ocamlfind jbuilder ounit"
+
+RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update
+
+# Setup of the base switch; CI_OPAM contains Coq's CI dependencies.
+ENV CAMLP5_VER="6.14" \
+    COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" \
+    CI_OPAM="menhir elpi ocamlgraph"
+
+RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \
+    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
+
+# base+32bit switch
+RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \
+    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER
+
+# BE switch
+ENV COMPILER_BE="4.06.1" \
+    CAMLP5_VER_BE="7.05" \
+    COQIDE_OPAM_BE="lablgtk.2.18.6 conf-gtksourceview.2"
+
+RUN opam switch -y -j $NJOBS $COMPILER_BE && eval $(opam config env) && \
+    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE
+
+# BE+flambda switch
+RUN opam switch -y -j $NJOBS "${COMPILER_BE}+flambda" && eval $(opam config env) && \
+    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE $CI_OPAM
diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push
new file mode 100755
index 000000000..307680aa5
--- /dev/null
+++ b/dev/ci/docker/bionic_coq/hooks/post_push
@@ -0,0 +1,8 @@
+#!/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 000000000..70278e6d0
--- /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