use opam-based CI

.gitignore

@@ -17,3 +17,4 @@
 auto
 *.fmt
 coq/*/Makefile.coq
+*~

.gitlab-ci.yml

-image: coq:8.5
+image: ralfjung/opam-ci:latest
 
-stages:
-  - depsquick
-  - depsfull
-  - quickbuild
-  - quickcheck
-  - fullbuild
-
-iris-quick:
-  stage: depsquick
-  tags:
-  - coq
-  script: >
-    (git --version || (apt-get update && apt-get install -y git));
-    git submodule update --init --recursive;
-    cd coq/iris;
-    cat _CoqProject | grep -v '^test' > _CoqProject_filtered;
-    mv _CoqProject_filtered _CoqProject;
-    make -j8 quick;
-    git checkout _CoqProject
-  only:
-  - master
-
-iris-full:
-  stage: depsfull
-  tags:
-  - coq
-  script: >
-    (git --version || (apt-get update && apt-get install -y git));
-    git submodule update --init --recursive;
-    cd coq/iris;
-    cat _CoqProject | grep -v '^test' > _CoqProject_filtered;
-    mv _CoqProject_filtered _CoqProject;
-    make -j8;
-    git checkout _CoqProject
-  only:
-  - master
-
-# vio:
-#   stage: quickbuild
-#   tags:
-#   - coq
-#   script: >
-#     cd coq/ra/;
-#     coqc -v;
-#     time make -j8 TIMED=y quick 2>&1 | tee build-log-vio.txt;
-#     cat build-log-vio.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio.txt
-#   only:
-#   - master
-#   cache:
-#     paths:
-#     - coq/ra/*.vio
-#   artifacts:
-#     paths:
-#     - coq/ra/build-time-vio.txt
-
-# vio2vo:
-#   stage: quickcheck
-#   tags:
-#   - coq
-#   script: >
-#     cd coq/ra/;
-#     coqc -v;
-#     time make -j8 TIMED=y vio2vo J=8 2>&1 | tee build-log-vio2vo.txt;
-#     cat build-log-vio2vo.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio2vo.txt
-#   only:
-#   - master
-#   allow_failure: true
-#   artifacts:
-#     paths:
-#     - coq/ra/build-time-vio2vo.txt
-
-full:
-  stage: fullbuild
-  tags:
-  - coq
-  script: >
-    cd coq/ra/;
-    coqc -v;
-    make clean;
-    time make -j8 TIMED=y 2>&1 | tee build-log-full.txt;
-    fgrep Axiom build-log-full.txt && exit 1;
-    cat build-log-full.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-full.txt;
+gps-coq8.5.3:
+  script:
+  # prepare
+  - cd coq
+  - . build/opam-ci.sh 'coq 8.5.3' 'coq-mathcomp-ssreflect 1.6'
+  # build (the script above switched us to the right directory)
+  - 'time make -j8 TIMED=y 2>&1 | tee build-log-full.txt'
+  - 'if fgrep Axiom build-log-full.txt >/dev/null; then exit 1; fi'
+  - 'cat build-log-full.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-full.txt'
+  cache:
+    key: "coq8.5.3"
+    paths:
+    - coq/opamroot/
   only:
   - master
+  - opam-ci
   artifacts:
     paths:
     - coq/ra/build-time-full.txt

.gitmodules

-[submodule "coq/iris"]
-	path = coq/iris
-	url = https://gitlab.mpi-sws.org/FP/iris-coq.git

coq/build/opam-ci.sh

+#!/bin/bash
+set -e
+# This script installs the build dependencies for CI builds.
+
+# Prepare OPAM configuration
+export OPAMROOT="$(pwd)/opamroot"
+export OPAMJOBS=16
+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`
+test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 5
+test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
+test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
+opam update
+opam install ocamlfind -y # Remove this once the Coq crew fixed their package...
+
+# Install fixed versions of some dependencies
+echo
+for PIN in "${@}"
+do
+    echo "Applying pin: $PIN"
+    opam pin add $PIN -k version -y
+done
+
+# Install build-dependencies
+echo
+cd ra
+make build-dep Y=1
+
+# done
+echo
+coqc -v

coq/build/opam-pins.sh

+#!/bin/bash
+set -e
+## Process an opam.pins file from stdin: Add all the given pins, but don't install anything.
+## Usage:
+##   ./opam-pins.sh < opam.pins
+
+# Process stdin
+while read PACKAGE URL HASH; do
+    if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
+        echo "[opam-pins] Recursing into $URL"
+        # an MPI URL -- try doing recursive pin processing
+        curl -f "$URL/raw/$HASH" 2> /dev/null | "$0"
+    fi
+    echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
+    opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
+    echo
+done

iris @ 6e00aa34

-Subproject commit 6e00aa3402b729fb58e5dd0c95d18156ca70c3a2

coq/ra/Makefile

-# Makefile originally taken from coq-club
+# Process flags
+ifeq ($(Y), 1)
+	YFLAG=-y
+endif
 
+# Determine Coq version
+COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]')
+COQ_MAKEFILE_FLAGS ?=
+
+ifeq ($(COQ_VERSION), 8.6)
+	COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection
+endif
+
+# Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
-	+make -f Makefile.coq $@
+	+@make -f Makefile.coq $@
 
 all: Makefile.coq
-	+make -f Makefile.coq all
+	+@make -f Makefile.coq all
 
 clean: Makefile.coq
-	+make -f Makefile.coq clean
+	+@make -f Makefile.coq clean
+	find \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
 	rm -f Makefile.coq
 
+# Create Coq Makefile
 Makefile.coq: _CoqProject Makefile
-	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
-
-_CoqProject: ;
-
+	@# we want to pass the correct name to coq_makefile or it will be confused.
+	coq_makefile $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq
+	mv Makefile.coq Makefile.coq.tmp
+	@# The sed script is for Coq 8.5 only, it fixes 'make verify'.
+	@# The awk script fixes 'make uninstall'.
+	sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' < Makefile.coq.tmp \
+	  | awk '/^uninstall:/{print "uninstall:";print "\tif [ -d \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ ]; then find \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ -name \"*.vo\" -print -delete; fi";getline;next}1' > Makefile.coq
+	rm Makefile.coq.tmp
+
+# Install build-dependencies
+build-dep:
+	../build/opam-pins.sh < ../../opam.pins
+	opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
+	opam pin add coq-gps "$$(pwd)/../..#HEAD" -k git -n -y
+	opam install coq-gps --deps-only $(YFLAG)
+	opam pin remove coq-gps
+
+# some fiels that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
+_CoqProject: ;
 
+# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
 phony: ;
-
 .PHONY: all clean phony

coq/ra/_CoqProject

 -R . ra
--Q ../iris iris
 ./infrastructure.v
 ./types.v
 ./views.v

opam

+opam-version: "1.2"
+name: "coq-gps"
+version: "dev"
+maintainer: "Jan-Oliver Kaiser, Hoang-Hai Dang"
+authors: "Jan-Oliver Kaiser, Hoang-Hai Dang"
+# homepage: "?"
+bug-reports: "https://gitlab.mpi-sws.org/FP/sra-gps/issues"
+dev-repo: "https://gitlab.mpi-sws.org/FP/sra-gps.git"
+build: [
+  [make "-j%{jobs}%"]
+]
+install: [make "install"]
+# TODO: probably we want to install things to a different folder, "ra" is rather undescriptive
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/ra" ]
+depends: [
+  "coq-iris"
+]

opam.pins

+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 6e00aa3402b729fb58e5dd0c95d18156ca70c3a2