From 2f28694b3d381f79e0311d8836d0552076ce1551 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 17 Mar 2017 14:56:33 +0100
Subject: [PATCH] update to new CI machine
---
.gitlab-ci.yml | 20 +++++++++++---------
Makefile | 16 ++++------------
_CoqProject | 1 +
build/opam-ci.sh | 24 +++++++++++++++++-------
build/opam-pins.sh | 17 +++++++++++++----
5 files changed, 46 insertions(+), 32 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 50665ca..860cf17 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,34 +1,36 @@
image: ralfjung/opam-ci:latest
+variables:
+ CPU_CORES: "9"
+
iris_atomic-coq8.5.3:
tags:
- - coq
+ - fp-timing
script:
# prepare
- - . build/opam-ci.sh 'coq 8.5.3' 'coq-mathcomp-ssreflect 1.6.1'
+ - . build/opam-ci.sh coq 8.5.3 coq-mathcomp-ssreflect 1.6.1
# build
- - 'time make -j8'
+ - 'time make -j$CPU_CORES'
cache:
key: "coq8.5.3"
paths:
- opamroot/
only:
- master
- - ci
+ - /^ci/
iris_atomic-coq8.6:
tags:
- - coq
+ - fp-timing
script:
# prepare
- - . build/opam-ci.sh 'coq 8.6' 'coq-mathcomp-ssreflect 1.6.1'
+ - . build/opam-ci.sh coq 8.6 coq-mathcomp-ssreflect 1.6.1
# build
- - 'time make -j8'
+ - 'time make -j$CPU_CORES'
cache:
key: "coq8.6"
paths:
- opamroot/
only:
- master
- - ci
- - timing
+ - /^ci/
diff --git a/Makefile b/Makefile
index 843c643..7bfa06f 100644
--- a/Makefile
+++ b/Makefile
@@ -3,14 +3,6 @@ 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,-several-object-files
-endif
-
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
@@ -25,16 +17,16 @@ 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 $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq
+ 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:
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-atomic "$$(pwd)#HEAD" -k git -n -y
- opam install coq-iris-atomic --deps-only $(YFLAG)
- opam pin remove coq-iris-atomic
+ opam pin add opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
+ opam install opam-builddep-temp --deps-only $(YFLAG)
+ opam pin remove opam-builddep-temp
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
diff --git a/_CoqProject b/_CoqProject
index 69fa428..3fd2388 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,5 @@
-Q theories iris_atomic
+-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/atomic.v
theories/sync.v
theories/atomic_incr.v
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index e952573..20d87f9 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -4,24 +4,34 @@ set -e
# Prepare OPAM configuration
export OPAMROOT="$(pwd)/opamroot"
-export OPAMJOBS=16
+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`
+if test $(find "$OPAMROOT/repo/package-index" -mtime +0); then
+ # last update was more than a day ago
+ opam update
+else
+ echo "[opam-ci] Not updating opam."
+fi
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
+while (( "$#" )); do # while there are arguments left
+ PACKAGE="$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"
+ else
+ echo "[opam-ci] Pinning $PACKAGE to $VERSION"
+ opam pin add "$PACKAGE" "$VERSION" -k version -y
+ fi
done
# Install build-dependencies
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
index aebd23c..5291cb2 100755
--- a/build/opam-pins.sh
+++ b/build/opam-pins.sh
@@ -4,14 +4,23 @@ set -e
## Usage:
## ./opam-pins.sh < opam.pins
+if ! which curl >/dev/null; then
+ echo "opam-pins needs curl. Please install curl and try again."
+ exit 1
+fi
+
# 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"
+ curl -f "$URL/raw/$HASH/opam.pins" 2>/dev/null | "$0"
+ fi
+ if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
+ echo "[opam-pins] $PACKAGE already at commit $HASH"
+ else
+ echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
+ opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
+ echo
fi
- echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
- opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
- echo
done
--
GitLab