diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index da8b15ac80881ac1a4a23190d69969c5877b0cac..324ebde14f3f78ff491569807a4e2edbd7f49af8 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -5,21 +5,14 @@ stages:
variables:
CPU_CORES: "10"
+ GIT_SUBMODULE_STRATEGY: "recursive"
.template: &template
stage: build
tags:
- fp
script:
- # 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'
+ - ci/buildjob
cache:
key: "$CI_JOB_NAME"
paths:
@@ -33,21 +26,19 @@ variables:
## Build jobs
-build-coq.8.8.dev:
+build-coq.8.8.0:
<<: *template
variables:
- OPAM_PINS: "coq version 8.8.dev"
+ OPAM_PINS: "coq version 8.8.0"
build-coq.8.7.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.2"
+ TIMING_PROJECT: "igps"
+ TIMING_CONF: "coq-8.7.2"
tags:
- fp-timing
- artifacts:
- paths:
- - build-time.txt
- - build-env.txt
build-iris.dev:
<<: *template
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000000000000000000000000000000000000..53648fdc2581a4d79760bf124d570b7692157ba8
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "ci"]
+ path = ci
+ url = https://gitlab.mpi-sws.org/FP/iris-ci.git
diff --git a/Makefile b/Makefile
index 2aa31aa00ed15829352d41b9919eceeee8a92937..aa91ea531c5f0c1a60dddd855097151ae5c06042 100644
--- a/Makefile
+++ b/Makefile
@@ -20,7 +20,7 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
# Install build-dependencies
build-dep/opam: opam Makefile
- # Creating the build-dep package.
+ @echo "# Creating 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,12 +31,13 @@ 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.
- @# Upgrading is needed in case the pin already exists, but the builddep package changed.
+ @# Reinstalling is needed in case the pin already exists, but the builddep package changed.
+ @# Once we depend on opam 2, we can remove that last step.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
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"
+ echo "# Reinstalling build-dep package." && \
+ opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
diff --git a/README.md b/README.md
index 7bbad27d01711f193f0292cdfad6121173174254..fd3d1dd27d53c39e04519e340c550877c6582f0a 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ which are variants of **GPS** and **RSL** in Iris.
## Dependencies
The master branch is known to compile with:
-* Coq 8.7.1
+* Coq 8.7.2 / 8.8.0
* Iris (MoSeL branch)
## Build
diff --git a/awk.Makefile b/awk.Makefile
index 91f7d7374d1fd76f61ef2f9404ba4e1b1ac3dfb7..dc1c7eee18ec6f3d5f1530e777e707dc9c1ff393 100644
--- a/awk.Makefile
+++ b/awk.Makefile
@@ -19,17 +19,5 @@
next
}
-# Add new target quick2vo to (a) run "make quick" with the same number of jobs, ensuring
-# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
-# files where the .vo is *older* than the .vio.
-/^vio2vo:/ {
- print "quick2vo:";
- print "\t@make -j $(J) quick"
- print "\t@VIOFILES=$$(for vofile in $(VOFILES); do viofile=\"$$(echo \"$$vofile\" | sed \"s/\\.vo/.vio/\")\"; if [ \"$$vofile\" -ot \"$$viofile\" -o ! -e \"$$vofile\" ]; then echo -n \"$$viofile \"; fi; done); \\"
- print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
- print "\t if [ -n \"$$VIOFILES\" ]; then $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
- print ".PHONY: quick2vo"
-}
-
# This forwards all unchanged lines
1
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
deleted file mode 100755
index bc51df87ef1e4c3867512df9f8b309111109a151..0000000000000000000000000000000000000000
--- a/build/opam-ci.sh
+++ /dev/null
@@ -1,68 +0,0 @@
-#!/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
diff --git a/ci b/ci
new file mode 160000
index 0000000000000000000000000000000000000000..40b71102efe051c777a785035aebcbaa4c2ec19f
--- /dev/null
+++ b/ci
@@ -0,0 +1 @@
+Subproject commit 40b71102efe051c777a785035aebcbaa4c2ec19f