From 99470279e32026018b28ed3b50bcfcb39d3bf722 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Dec 2016 16:29:00 +0100
Subject: [PATCH] use OPAM-based CI
---
.gitlab-ci.yml | 32 ++++++++++++++++++++++++++++----
Makefile | 23 ++++++++++++++++++++---
build/opam-ci.sh | 33 +++++++++++++++++++++++++++++++++
build/opam-pins.sh | 17 +++++++++++++++++
opam.pins | 0
5 files changed, 98 insertions(+), 7 deletions(-)
create mode 100755 build/opam-ci.sh
create mode 100755 build/opam-pins.sh
create mode 100644 opam.pins
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 5c3e7df8a..8c1c988f1 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,17 +1,41 @@
-image: coq:8.5
+image: ralfjung/opam-ci:latest
-buildjob:
+iris-coq8.5.3:
tags:
- coq
script:
- - coqc -v
+ # prepare
+ - . build/opam-ci.sh 'coq 8.5.3' 'coq-mathcomp-ssreflect 1.6'
+ # build
- 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
- 'fgrep Axiom build-log.txt && exit 1'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
- - make validate
+ #- make validate
+ cache:
+ key: "coq8.5.3"
+ paths:
+ - opamroot/
only:
- master
+ - ci
- timing
artifacts:
paths:
- build-time.txt
+
+iris-coq8.6beta:
+ tags:
+ - coq
+ script:
+ # prepare
+ - . build/opam-ci.sh 'coq 8.6.dev 'coq-mathcomp-ssreflect dev'
+ # build
+ - 'time make -j8'
+ cache:
+ key: "coq8.6"
+ paths:
+ - opamroot/
+ only:
+ - master
+ - ci
+ - timing
diff --git a/Makefile b/Makefile
index b1c684e83..79ae75eb8 100644
--- a/Makefile
+++ b/Makefile
@@ -1,3 +1,8 @@
+# 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 ?=
@@ -6,6 +11,7 @@ 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 $@
@@ -17,18 +23,29 @@ clean: Makefile.coq
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
- @# we want to pass the correct name to coq_makefile or it will be confused
+ @# 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
-_CoqProject: ;
+# 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-iris "$$(pwd)#HEAD" -k git -n -y
+ opam install coq-iris --deps-only $(YFLAG)
+ opam pin remove coq-iris
+# 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
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
new file mode 100755
index 000000000..e95257363
--- /dev/null
+++ b/build/opam-ci.sh
@@ -0,0 +1,33 @@
+#!/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
+make build-dep Y=1
+
+# done
+echo
+coqc -v
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
new file mode 100755
index 000000000..aebd23ca2
--- /dev/null
+++ b/build/opam-pins.sh
@@ -0,0 +1,17 @@
+#!/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
diff --git a/opam.pins b/opam.pins
new file mode 100644
index 000000000..e69de29bb
--
GitLab