6 files changed, 34 insertions, 7 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 19ba9de245..475f812b5a 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -283,8 +283,9 @@
 ########################################################################
 # menhirlib
 ########################################################################
+# Note: menhirlib is now in subfolder coq-menhirlib of menhir
 : "${menhirlib_CI_REF:=master}"
-: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/coq-menhirlib}"
+: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/menhir}"
 : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}"
 
 ########################################################################
@@ -348,7 +349,7 @@
 ########################################################################
 # perennial
 ########################################################################
-: "${perennial_CI_REF:=master}"
+: "${perennial_CI_REF:=coq/tested}"
 : "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}"
 : "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}"
 
diff --git a/dev/ci/ci-unicoq.sh b/dev/ci/ci-unicoq.sh
index 36acb115e9..df1d9cceb8 100755
--- a/dev/ci/ci-unicoq.sh
+++ b/dev/ci/ci-unicoq.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download unicoq
 
-( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install )
+( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f _CoqProject -o Makefile && make && make install )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 0d2f1dfbc7..8c5696f4f9 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-05-19-V33"
+# CACHEKEY: "bionic_coq-V2020-05-24-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -13,8 +13,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         libgtksourceview-3.0-dev \
         # Dependencies of stdlib and sphinx doc
         texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
-        xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
-        fonts-freefont-otf \
+        python3-pip python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \
         # Dependencies of source-doc and coq-makefile
         texlive-science tipa
 
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index b3ced999f6..05624ff4a1 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -74,9 +74,20 @@ let Verdi = (coqPackages.Verdi.override { inherit Cheerios ssreflect; })
     src = fetchTarball "https://github.com/uwplse/verdi/tarball/master";
   }); in
 
+let flocq = coqPackages.flocq.overrideAttrs (o: {
+    src = fetchTarball "https://gitlab.inria.fr/flocq/flocq/-/archive/master/flocq-master.tar.gz";
+    configurePhase = ''
+      autoreconf
+      ${bash}/bin/bash configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Flocq
+    '';
+    buildPhase = ''
+      ./remake
+    '';
+  }); in
+
 let callPackage = newScope { inherit coq
   bignums coq-ext-lib coqprime corn iris math-classes
-  mathcomp simple-io ssreflect stdpp unicoq Verdi;
+  mathcomp simple-io ssreflect stdpp unicoq Verdi flocq;
 }; in
 
 # Environments for building CI libraries with this Coq
@@ -93,6 +104,7 @@ let projects = {
   fiat_crypto = callPackage ./fiat_crypto.nix {};
   flocq = callPackage ./flocq.nix {};
   formal-topology = callPackage ./formal-topology.nix {};
+  gappa = callPackage ./gappa.nix {};
   GeoCoq = callPackage ./GeoCoq.nix {};
   HoTT = callPackage ./HoTT.nix {};
   iris = callPackage ./iris.nix {};
diff --git a/dev/ci/nix/gappa.nix b/dev/ci/nix/gappa.nix
new file mode 100644
index 0000000000..8560cc072b
--- /dev/null
+++ b/dev/ci/nix/gappa.nix
@@ -0,0 +1,9 @@
+{ autoconf, automake, ocaml, flocq }:
+
+{
+  buildInputs = [ autoconf automake ocaml ];
+  coqBuildInputs = [ flocq ];
+  configure = "autoreconf && ./configure";
+  make = "./remake";
+  clean = "./remake clean";
+}
diff --git a/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh b/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh
new file mode 100644
index 0000000000..ced0d95945
--- /dev/null
+++ b/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12505" ] || [ "$CI_BRANCH" = "factor-hint-flags" ]; then
+
+    fiat_parsers_CI_REF="factor-hint-flags"
+    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat
+
+fi