8 files changed, 71 insertions, 12 deletions
diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 2ac78d3c2b..2d242d80a4 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download bedrock2
 
-( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make )
+( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make | iconv -t UTF-8 -c `#9767` )
diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh
index c641af2abb..d2e0ee89bf 100755
--- a/dev/ci/ci-paramcoq.sh
+++ b/dev/ci/ci-paramcoq.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download paramcoq
 
-( cd "${CI_BUILD_DIR}/paramcoq" && make && make install )
+( cd "${CI_BUILD_DIR}/paramcoq" && make && make install && cd test-suite && make examples)
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index ac763547b6..e553cbed1b 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-03-11-V1"
+# CACHEKEY: "bionic_coq-V2019-03-12-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -10,7 +10,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         # Dependencies of the image, the test-suite and external projects
         m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \
         # Dependencies of lablgtk (for CoqIDE)
-        libgtk2.0-dev libgtksourceview2.0-dev \
+        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 \
@@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \
                  antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
 
 # We need to install OPAM 2.0 manually for now.
-RUN wget https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.3/opam-2.0.3-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
 
 # Basic OPAM setup
 ENV NJOBS="2" \
@@ -41,7 +41,10 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \
     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"
+ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
+
+# Must add this to COQIDE_OPAM{,_EDGE} when we update the opam
+# packages "lablgtk3-gtksourceview3"
 
 # base switch
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
@@ -53,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.07.1" \
-    COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
+    COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" \
     BASE_OPAM_EDGE="dune-release.1.1.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
diff --git a/dev/ci/nix/coq.nix b/dev/ci/nix/coq.nix
index ecd280e58d..b610790f61 100644
--- a/dev/ci/nix/coq.nix
+++ b/dev/ci/nix/coq.nix
@@ -5,5 +5,4 @@ let coq = callPackage wd { buildDoc = false; doInstallCheck = false; coq-version
 coq.overrideAttrs (o: {
   name = "coq-local-${branch}";
   src = fetchGit "${wd}";
-  enableParallelBuilding = true;
 })
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 94e0a666e2..17070e66ee 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -1,4 +1,4 @@
-{ pkgs ? import <nixpkgs> {}
+{ pkgs ? import ../../nixpkgs.nix {}
 , branch
 , wd
 , project ? "xyz"
@@ -20,8 +20,17 @@ let mathcomp = coqPackages.mathcomp.overrideAttrs (o: {
 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 coq-ext-lib = coqPackages.coq-ext-lib.overrideAttrs (o: {
+    src = fetchTarball "https://github.com/coq-ext-lib/coq-ext-lib/tarball/master";
+  }); in
+
+let simple-io =
+  (coqPackages.simple-io.override { inherit coq-ext-lib; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://github.com/Lysxia/coq-simple-io/tarball/master";
+  }); 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
diff --git a/dev/ci/nix/quickchick.nix b/dev/ci/nix/quickchick.nix
index 46bf02ae3c..b90f1e4f88 100644
--- a/dev/ci/nix/quickchick.nix
+++ b/dev/ci/nix/quickchick.nix
@@ -1,5 +1,5 @@
 { ocamlPackages, ssreflect, coq-ext-lib, simple-io }:
 {
   buildInputs = with ocamlPackages; [ ocaml findlib ocamlbuild num ];
-  coqBuildInputs = [ ssreflect coq-ext-lib simple-io ];
+  coqBuildInputs = [ ssreflect simple-io ];
 }
diff --git a/dev/ci/user-overlays/08817-sprop.sh b/dev/ci/user-overlays/08817-sprop.sh
new file mode 100644
index 0000000000..81e18226ed
--- /dev/null
+++ b/dev/ci/user-overlays/08817-sprop.sh
@@ -0,0 +1,34 @@
+if [ "$CI_PULL_REQUEST" = "8817" ] || [ "$CI_BRANCH" = "sprop" ]; then
+    aac_tactics_CI_REF=sprop
+    aac_tactics_CI_GITURL=https://github.com/SkySkimmer/aac-tactics
+
+    coq_dpdgraph_CI_REF=sprop
+    coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph
+
+    coqhammer_CI_REF=sprop
+    coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer
+
+    elpi_CI_REF=sprop
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    equations_CI_REF=sprop
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    ltac2_CI_REF=sprop
+    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
+
+    unicoq_CI_REF=sprop
+    unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq
+
+    mtac2_CI_REF=sprop
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2
+
+    paramcoq_CI_REF=sprop
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+    quickchick_CI_REF=sprop
+    quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
+
+    relation_algebra_CI_REF=sprop
+    relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra
+fi
diff --git a/dev/ci/user-overlays/09678-printed-by-env.sh b/dev/ci/user-overlays/09678-printed-by-env.sh
new file mode 100644
index 0000000000..ccb3498764
--- /dev/null
+++ b/dev/ci/user-overlays/09678-printed-by-env.sh
@@ -0,0 +1,14 @@
+
+if [ "$CI_PULL_REQUEST" = "9678" ] || [ "$CI_BRANCH" = "printed-by-env" ]; then
+    elpi_CI_REF=printed-by-env
+    elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
+
+    equations_CI_REF=printed-by-env
+    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+    ltac2_CI_REF=printed-by-env
+    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    quickchick_CI_REF=printed-by-env
+    quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick
+fi