diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3fad1c8c5156fc09b35aed3f48dcb0d71f3c2990..e4acbd9ff31a703a65c7a70657f8261acee7f24a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,41 +1,57 @@
 image: ralfjung/opam-ci:latest
 
+stages:
+  - build
+
 variables:
-  CPU_CORES: "9"
+  CPU_CORES: "10"
 
 .template: &template
+  stage: build
   tags:
-  - fp-timing
+  - fp
   script:
   # prepare
-  - . build/opam-ci.sh coq "$COQ_VERSION" coq-mathcomp-ssreflect "$SSR_VERSION"
+  - . build/opam-ci.sh $OPAM_PINS
   - env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
   # build
   - 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
   - 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
   - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
-  - 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
+  # maybe validate
+  - 'if [[ -n "$VALIDATE" ]]; then make validate; fi'
   cache:
-    key: "coq.$COQ_VERSION-ssr.$SSR_VERSION"
+    key: "$CI_JOB_NAME"
     paths:
     - opamroot/
   only:
-  - master
+  - gen_proofmode_WIP
   - /^ci/
+  except:
+  - triggers
 
-build-coq8.7:
-  <<: *template
-  variables:
-    COQ_VERSION: "8.7.dev"
-    SSR_VERSION: "dev"
+## Build jobs
 
-build-coq8.6.1:
+build-coq.8.7.1:
   <<: *template
   variables:
-    COQ_VERSION: "8.6.1"
-    SSR_VERSION: "1.6.1"
-    VALIDATE: "1"
+    OPAM_PINS: "coq version 8.7.1   coq-mathcomp-ssreflect version 1.6.4"
+  tags:
+  - fp-timing
   artifacts:
     paths:
     - build-time.txt
     - build-env.txt
+
+build-coq.8.6.1:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.6.1   coq-mathcomp-ssreflect version 1.6.4"
+
+build-iris.dev:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.7.1   coq-mathcomp-ssreflect version 1.6.4   coq-iris.dev git https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
+  except:
+  only:
+  - triggers
diff --git a/Makefile b/Makefile
index 83a26f561bc7ce8d8ec208c44750d51da303c032..2aa31aa00ed15829352d41b9919eceeee8a92937 100644
--- a/Makefile
+++ b/Makefile
@@ -15,12 +15,12 @@ clean: Makefile.coq
 # Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
 # filename, so we do some file gymnastics.
 Makefile.coq: _CoqProject Makefile awk.Makefile
-	coq_makefile -f _CoqProject -o Makefile.coq
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
 	mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
 
 # Install build-dependencies
 build-dep/opam: opam Makefile
-	# Create the build-dep package.
+	# Creating the build-dep package.
 	@mkdir -p build-dep
 	@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
 	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
@@ -31,11 +31,12 @@ build-dep: build-dep/opam phony
 	@# that are incompatible with our build requirements.
 	@# To achieve this, we create a fake opam package that has our build-dependencies as
 	@# dependencies, but does not actually install anything.
-	# Add the pin and (re)install build-dep package.
-	@# Reinstallation is needed in case the pin already exists, but the builddep package changed.
+	@# Upgrading is needed in case the pin already exists, but the builddep package changed.
 	@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
-	  opam pin add "$$BUILD_DEP_PACKAGE".dev "$$(pwd)/build-dep" -k path $(OPAMFLAGS) && \
-	  opam reinstall "$$BUILD_DEP_PACKAGE"
+	  echo "# Pinning build-dep package." && \
+	  opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
+	  echo "# Updating build-dep package." && \
+	  opam upgrade "$$BUILD_DEP_PACKAGE"
 
 # Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index 27ae623d2f580b2d2b898d674cd6229bf74425e1..bc51df87ef1e4c3867512df9f8b309111109a151 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -1,10 +1,7 @@
 #!/bin/bash
 set -e
+set -x
 ## This script installs the build dependencies for CI builds.
-function run_and_print() {
-    echo "$ $@"
-    "$@"
-}
 
 # Prepare OPAM configuration
 export OPAMROOT="$(pwd)/opamroot"
@@ -12,26 +9,27 @@ export OPAMJOBS="$((2*$CPU_CORES))"
 export OPAM_EDITOR="$(which false)"
 
 # Make sure we got a good OPAM.
-test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && run_and_print opam init --no-setup -y)
+test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
 eval `opam conf env`
-# Delete old pins from opam.pins times.
-run_and_print opam pin remove coq-stdpp -n
-run_and_print opam pin remove coq-iris -n
+
 # Make sure the pin for the builddep package is not stale.
-run_and_print make build-dep/opam
+make build-dep/opam
+
+# Update repositories
+opam update
 
-# Get us all the latest repositories
-if test $(find "$OPAMROOT/repo/package-index" -mtime +0); then
-    # last update was more than a day ago
-    run_and_print opam update
+# Make sure we got the right set of repositories registered
+if echo "$@" | fgrep "dev" > /dev/null; then
+    # We are compiling against a dev version of something.  Get ourselves the dev repositories.
+    test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 0
+    test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
 else
-    # only update iris-dev
-    if test -d "$OPAMROOT/repo/iris-dev"; then run_and_print opam update iris-dev; fi
+    # No dev version, make sure we do not have the dev repositories.
+    test -d "$OPAMROOT/repo/coq-extra-dev" && opam repo remove coq-extra-dev
+    test -d "$OPAMROOT/repo/coq-core-dev" && opam repo remove coq-core-dev
 fi
-test -d "$OPAMROOT/repo/coq-extra-dev" && run_and_print opam repo remove coq-extra-dev
-test -d "$OPAMROOT/repo/coq-core-dev" || run_and_print opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
-test -d "$OPAMROOT/repo/coq-released" || run_and_print opam repo add coq-released https://coq.inria.fr/opam/released -p 10
-test -d "$OPAMROOT/repo/iris-dev" || run_and_print opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
+test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
+test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
 echo
 
 # We really want to run all of the following in one opam transaction, but due to opam limitations,
@@ -41,21 +39,23 @@ echo
 echo
 while (( "$#" )); do # while there are arguments left
     PACKAGE="$1" ; shift
+    KIND="$1" ; shift
     VERSION="$1" ; shift
 
     # Check if the pin is already set
-    if opam pin list | fgrep "$PACKAGE.$VERSION " > /dev/null; then
-        echo "[opam-ci] $PACKAGE already pinned to $VERSION"
+    read -a PIN <<< $(opam pin list | (egrep "^$PACKAGE[. ]"))
+    if [[ "${PIN[1]}" == "$KIND" && "${PIN[2]}" == "$VERSION" ]]; then
+        echo "[opam-ci] $PACKAGE already $KIND-pinned to $VERSION"
     else
-        echo "[opam-ci] Pinning $PACKAGE to $VERSION"
-        run_and_print opam pin add "$PACKAGE" "$VERSION" -k version -y
+        echo "[opam-ci] $KIND-pinning $PACKAGE to $VERSION"
+        opam pin add -y -k "$KIND" "$PACKAGE" "$VERSION"
     fi
 done
 
 # Upgrade cached things.
 echo
 echo "[opam-ci] Upgrading opam"
-run_and_print opam upgrade -y
+opam upgrade -y --fixup && opam upgrade -y
 
 # Install build-dependencies.
 echo
@@ -63,5 +63,6 @@ echo "[opam-ci] Installing build-dependencies"
 make build-dep OPAMFLAGS=-y
 
 # done
+set +x
 echo
 coqc -v