22 files changed, 138 insertions, 73 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 6663fbecf8..98ea594366 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -16,14 +16,9 @@ We are currently running tests on the following platforms:
   `./configure`. It should allow complying with this discipline
   without pain.
 
-- Travis CI is used to test the compilation of Coq and run the test-suite on
-  macOS.
-
-- AppVeyor is used to test the compilation of Coq and run the test-suite on
-  Windows.
-
 - Azure Pipelines is used to test the compilation of Coq and run the
-  test-suite on Windows. It is expected to replace appveyor eventually.
+  test-suite on Windows and on macOS. It is expected to be used to build
+  macOS and Windows packages eventually.
 
 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:
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
deleted file mode 100644
index 341b875edc..0000000000
--- a/dev/ci/appveyor.bat
+++ /dev/null
@@ -1,42 +0,0 @@
-REM This script either runs the test suite with OPAM (if USEOPAM is true) or
-REM builds the Coq binary packages for windows (if USEOPAM is false).
-
-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
-)
-
-SET CYGCACHE=%CYGROOT%\var\cache\setup
-SET APPVEYOR_BUILD_FOLDER_MFMT=%APPVEYOR_BUILD_FOLDER:\=/%
-SET APPVEYOR_BUILD_FOLDER_CFMT=%APPVEYOR_BUILD_FOLDER_MFMT:C:/=/cygdrive/c/%
-SET DESTCOQ=C:\coq%ARCH%_inst
-SET COQREGTESTING=Y
-
-if %USEOPAM% == false (
-  call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-    -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
-    -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
-    -addon=bignums -make=N ^
-    -setup %CYGROOT%\%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
-)
-
-if %USEOPAM% == true (
-  %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^
-    -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time
-  %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit
-)
-
-GOTO :EOF
-
-:ErrorExit
-  ECHO ERROR %0 failed
-  EXIT /b 1
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 8dee465cf4..74e8d3bbaa 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -35,7 +35,7 @@
 : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}"
 : "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}"
 
-: "${mtac2_CI_REF:=master-sync}"
+: "${mtac2_CI_REF:=master}"
 : "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}"
 : "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}"
 
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
index 12a70176c2..9ca8f76054 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -6,13 +6,6 @@
 
 set -eo pipefail
 
-function travis_fold {
-    if [ -n "${TRAVIS}" ];
-    then
-	echo "travis_fold:$1:$2"
-    fi
-}
-
 CI_NAME="$1"
 CI_SCRIPT="ci-${CI_NAME}.sh"
 
@@ -22,6 +15,5 @@ cd "${DIR}/../.."
 
 export TIMED=1
 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
-travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...'
+echo 'Aggregating timing log...'
 python ./tools/make-one-time-file.py time-of-build.log
-travis_fold 'end' 'coq.test.timing'
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index baf470e021..4cd7faf757 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-12-14-V1"
+# CACHEKEY: "bionic_coq-V2019-01-28-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -38,7 +38,7 @@ ENV COMPILER="4.05.0"
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
 ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.3.0" \
-    CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
+    CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix
index 4c5cfd83da..3fcf177aec 100644
--- a/dev/ci/nix/CoLoR.nix
+++ b/dev/ci/nix/CoLoR.nix
@@ -1,5 +1,5 @@
 { bignums }:
 
 {
-  buildInputs = [ bignums ];
+  coqBuildInputs = [ bignums ];
 }
diff --git a/dev/ci/nix/Corn.nix b/dev/ci/nix/Corn.nix
index 18c7750279..0d22a6b91b 100644
--- a/dev/ci/nix/Corn.nix
+++ b/dev/ci/nix/Corn.nix
@@ -1,5 +1,5 @@
 { bignums, math-classes }:
 
 {
-  buildInputs = [ bignums math-classes ];
+  coqBuildInputs = [ bignums math-classes ];
 }
diff --git a/dev/ci/nix/GeoCoq.nix b/dev/ci/nix/GeoCoq.nix
index a86fb2c44a..45d688285e 100644
--- a/dev/ci/nix/GeoCoq.nix
+++ b/dev/ci/nix/GeoCoq.nix
@@ -1,5 +1,5 @@
 { mathcomp }:
 {
-  buildInputs = [ mathcomp ];
+  coqBuildInputs = [ mathcomp ];
   configure = "./configure.sh";
 }
diff --git a/dev/ci/nix/README.md b/dev/ci/nix/README.md
index 1685b084e9..6f32abef95 100644
--- a/dev/ci/nix/README.md
+++ b/dev/ci/nix/README.md
@@ -17,3 +17,10 @@ build-system of that project: `configure`, `make`, and `clean`. Therefore, after
 changing the working directory to the root of the sources of that project, the
 contents of these variables can be evaluated to respectively set-up, build, and
 clean the project.
+
+## Variant: nocoq
+
+The dependencies of the third-party developments are split into `buildInputs`
+and `coqBuildInputs`. The second list gathers the Coq libraries. In case you
+only want the non-coq dependencies (because you want to use Coq from your `PATH`),
+set the environment variable `NOCOQ` to some non-empty value.
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 4acfae48e4..277e9ee08f 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -2,7 +2,8 @@
 , branch
 , wd
 , project ? "xyz"
-, bn ? "release"
+, withCoq ? true
+, bn ? "master"
 }:
 
 with pkgs;
@@ -16,6 +17,11 @@ let mathcomp = coqPackages.mathcomp.overrideAttrs (o: {
     name = "coq-git-mathcomp-git";
     src = fetchTarball https://github.com/math-comp/math-comp/archive/master.tar.gz;
   }); in
+let ssreflect = coqPackages.ssreflect.overrideAttrs (o: {
+  inherit (mathcomp) src;
+  }); in
+let coq-ext-lib = coqPackages.coq-ext-lib; in
+let simple-io = coqPackages.simple-io; in
 let bignums = coqPackages.bignums.overrideAttrs (o:
     if bn == "release" then {} else
     if bn == "master" then { src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz; } else
@@ -28,9 +34,17 @@ let math-classes =
     src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz";
   }); in
 
-let unicoq = callPackage ./unicoq.nix { inherit coq; }; in
+let corn = (coqPackages.corn.override { inherit coq bignums math-classes; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz";
+  }); in
+
+let unicoq = callPackage ./unicoq { inherit coq; }; in
 
-let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in
+let callPackage = newScope { inherit coq
+  bignums coq-ext-lib coqprime corn math-classes
+  mathcomp simple-io ssreflect unicoq;
+}; in
 
 # Environments for building CI libraries with this Coq
 let projects = {
@@ -45,12 +59,14 @@ let projects = {
   fiat_crypto = callPackage ./fiat_crypto.nix {};
   fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {};
   flocq = callPackage ./flocq.nix {};
+  formal-topology = callPackage ./formal-topology.nix {};
   GeoCoq = callPackage ./GeoCoq.nix {};
   HoTT = callPackage ./HoTT.nix {};
   math_classes = callPackage ./math_classes.nix {};
   mathcomp = {};
   mtac2 = callPackage ./mtac2.nix {};
   oddorder = callPackage ./oddorder.nix {};
+  quickchick = callPackage ./quickchick.nix {};
   VST = callPackage ./VST.nix {};
 }; in
 
@@ -60,10 +76,16 @@ else
 
 let prj = projects."${project}"; in
 
+let inherit (stdenv.lib) optional optionals; in
+
 stdenv.mkDerivation {
   name = "shell-for-${project}-in-${branch}";
 
-  buildInputs = [ coq ] ++ (prj.buildInputs or []);
+  buildInputs =
+    optional withCoq coq
+  ++ (prj.buildInputs or [])
+  ++ optionals withCoq (prj.coqBuildInputs or [])
+  ;
 
   configure = prj.configure or "true";
   make = prj.make or "make";
diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix
index 7b37e6e8e4..0f0ee91387 100644
--- a/dev/ci/nix/fiat_crypto.nix
+++ b/dev/ci/nix/fiat_crypto.nix
@@ -1,6 +1,6 @@
 { coqprime }:
 {
-  buildInputs = [ coqprime ];
+  coqBuildInputs = [ coqprime ];
   configure = "git submodule update --init --recursive && ulimit -s 32768";
   make = "make new-pipeline c-files";
 }
diff --git a/dev/ci/nix/formal-topology.nix b/dev/ci/nix/formal-topology.nix
new file mode 100644
index 0000000000..53b9b1182b
--- /dev/null
+++ b/dev/ci/nix/formal-topology.nix
@@ -0,0 +1,4 @@
+{ corn }:
+{
+  coqBuildInputs = [ corn ];
+}
diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix
index b0fa2fe795..8edc3c8358 100644
--- a/dev/ci/nix/math_classes.nix
+++ b/dev/ci/nix/math_classes.nix
@@ -1,6 +1,6 @@
 { bignums }:
 
 {
-  buildInputs = [ bignums ];
+  coqBuildInputs = [ bignums ];
   configure = "./configure.sh";
 }
diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix
index 9a2353c5cf..4acc326c02 100644
--- a/dev/ci/nix/mtac2.nix
+++ b/dev/ci/nix/mtac2.nix
@@ -1,5 +1,6 @@
 { coq, unicoq }:
 {
-  buildInputs = [ unicoq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
+  buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ];
+  coqBuildInputs = [ unicoq ];
   configure = "./configure.sh";
 }
diff --git a/dev/ci/nix/oddorder.nix b/dev/ci/nix/oddorder.nix
index 3b8fdbab51..2341bb3173 100644
--- a/dev/ci/nix/oddorder.nix
+++ b/dev/ci/nix/oddorder.nix
@@ -1,4 +1,4 @@
 { mathcomp }:
 {
-  buildInputs = [ mathcomp ];
+  coqBuildInputs = [ mathcomp ];
 }
diff --git a/dev/ci/nix/quickchick.nix b/dev/ci/nix/quickchick.nix
new file mode 100644
index 0000000000..46bf02ae3c
--- /dev/null
+++ b/dev/ci/nix/quickchick.nix
@@ -0,0 +1,5 @@
+{ ocamlPackages, ssreflect, coq-ext-lib, simple-io }:
+{
+  buildInputs = with ocamlPackages; [ ocaml findlib ocamlbuild num ];
+  coqBuildInputs = [ ssreflect coq-ext-lib simple-io ];
+}
diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell
index 2e4462ed40..a5f8ee8f54 100755
--- a/dev/ci/nix/shell
+++ b/dev/ci/nix/shell
@@ -17,4 +17,10 @@ else
   BN=""
 fi
 
-nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN
+if [ "$NOCOQ" ]; then
+    NOCOQ="--arg withCoq false"
+else
+    NOCOQ=""
+fi
+
+nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN $NOCOQ
diff --git a/dev/ci/nix/unicoq/META b/dev/ci/nix/unicoq/META
new file mode 100644
index 0000000000..30dd8b5559
--- /dev/null
+++ b/dev/ci/nix/unicoq/META
@@ -0,0 +1,2 @@
+archive(native) = "unicoq.cmxa"
+plugin(native) = "unicoq.cmxs"
diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq/default.nix
index 093c262cde..36f40dbe33 100644
--- a/dev/ci/nix/unicoq.nix
+++ b/dev/ci/nix/unicoq/default.nix
@@ -4,8 +4,16 @@ stdenv.mkDerivation {
   name = "coq${coq.coq-version}-unicoq-0.0-git";
   src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz;
 
+  patches = [ ./unicoq-num.patch ];
+
   buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]);
 
   configurePhase = "coq_makefile -f Make -o Makefile";
   installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+
+  postInstall = ''
+    install -d $OCAMLFIND_DESTDIR
+    ln -s $out/lib/coq/${coq.coq-version}/user-contrib/Unicoq $OCAMLFIND_DESTDIR/
+    install -m 0644 ${./META} src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq
+  '';
 }
diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch
new file mode 100644
index 0000000000..6d96d94dfc
--- /dev/null
+++ b/dev/ci/nix/unicoq/unicoq-num.patch
@@ -0,0 +1,44 @@
+commit f29bc64ee3d8b36758d17e1f5d50812e0c93063b
+Author: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
+Date:   Thu Nov 29 08:59:22 2018 +0000
+
+    Make explicit dependency to num
+
+diff --git a/Make b/Make
+index 550dc6a..8aa1309 100644
+--- a/Make
++++ b/Make
+@@ -9,7 +9,7 @@ src/logger.ml
+ src/munify.mli
+ src/munify.ml
+ src/unitactics.mlg
+-src/unicoq.mllib
++src/unicoq.mlpack
+ theories/Unicoq.v
+ test-suite/munifytest.v
+ test-suite/microtests.v
+diff --git a/Makefile.local b/Makefile.local
+new file mode 100644
+index 0000000..88be365
+--- /dev/null
++++ b/Makefile.local
+@@ -0,0 +1 @@
++CAMLPKGS += -package num
+diff --git a/src/unicoq.mllib b/src/unicoq.mllib
+deleted file mode 100644
+index 2b84e2d..0000000
+--- a/src/unicoq.mllib
++++ /dev/null
+@@ -1,3 +0,0 @@
+-Logger
+-Munify
+-Unitactics
+diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack
+new file mode 100644
+index 0000000..2b84e2d
+--- /dev/null
++++ b/src/unicoq.mlpack
+@@ -0,0 +1,3 @@
++Logger
++Munify
++Unitactics
diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
new file mode 100644
index 0000000000..6e89741e29
--- /dev/null
+++ b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then
+
+    bignums_CI_REF=primitive-integers
+    bignums_CI_GITURL=https://github.com/vbgl/bignums
+
+    mtac2_CI_REF=primitive-integers
+    mtac2_CI_GITURL=https://github.com/vbgl/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
new file mode 100644
index 0000000000..ebd1b524da
--- /dev/null
+++ b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then
+
+    mtac2_CI_REF=proof-mode
+    mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
+
+    ltac2_CI_REF=proof-mode
+    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    equations_CI_REF=proof-mode
+    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi