update for CI

.gitlab-ci.yml

-image: coq:8.5
+image: ralfjung/opam-ci:latest
 
-buildjob:
+stages:
+  - build
+
+variables:
+  CPU_CORES: "10"
+
+.template: &template
+  stage: build
   tags:
-  - coq
+  - fp
   script:
-  - coqc -v
-  - 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
-  - 'grep Axiom build-log.txt && exit 1'
-  - 'cat build-log.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
+  # prepare
+  - . 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'
+  # maybe validate
+  - 'if [[ -n "$VALIDATE" ]]; then make validate; fi'
+  # maybe create opam package
+  - 'if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == master ]]; then curl --fail -X POST -F "token=$OPAM_UPDATE_SECRET" -F "ref=master" -F "variables[REPO]=$CI_PROJECT_URL.git" -F "variables[REF]=$CI_COMMIT_REF_NAME" -F "variables[SHA]=$CI_COMMIT_SHA" -F "variables[NAME]=$OPAM_PKG" https://gitlab.mpi-sws.org/api/v4/projects/581/trigger/pipeline; fi'
+  cache:
+    key: "$CI_JOB_NAME"
+    paths:
+    - opamroot/
   only:
   - master
-  - jh_simplified_resources
-  artifacts:
-    paths:
-    - build-time.txt
+  - /^ci/
+  except:
+  - triggers
+
+## Build jobs
+
+build-coq.8.7.0:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.7.0   coq-mathcomp-ssreflect version 1.6.4"

Makefile

@@ -15,7 +15,7 @@ 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/opam-ci.sh

+#!/bin/bash
+set -e
+set -x
+## This script installs the build dependencies for CI builds.
+
+# Prepare OPAM configuration
+export OPAMROOT="$(pwd)/opamroot"
+export OPAMJOBS="$((2*$CPU_CORES))"
+export OPAM_EDITOR="$(which false)"
+
+# Make sure we got a good OPAM.
+test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
+eval `opam conf env`
+
+# Make sure the pin for the builddep package is not stale.
+make build-dep/opam
+
+# Update repositories
+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
+    # 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-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,
+# that is not currently possible.
+
+# Install fixed versions of some dependencies.
+echo
+while (( "$#" )); do # while there are arguments left
+    PACKAGE="$1" ; shift
+    KIND="$1" ; shift
+    VERSION="$1" ; shift
+
+    # Check if the pin is already set
+    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] $KIND-pinning $PACKAGE to $VERSION"
+        opam pin add -y -k "$KIND" "$PACKAGE" "$VERSION"
+    fi
+done
+
+# Upgrade cached things.
+echo
+echo "[opam-ci] Upgrading opam"
+opam upgrade -y --fixup && opam upgrade -y
+
+# Install build-dependencies.
+echo
+echo "[opam-ci] Installing build-dependencies"
+make build-dep OPAMFLAGS=-y
+
+# done
+set +x
+echo
+coqc -v