From 8f8796c0d6459fa6494ea483fe52501fb1644cc2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 18 Sep 2017 17:56:17 +0200
Subject: [PATCH] CI: depend on std++ via opam; prepare for automatic opam
releases
---
.gitlab-ci.yml | 13 +++++++++++++
Makefile | 4 +---
build/opam-ci.sh | 8 ++++++++
build/opam-pins.sh | 26 --------------------------
descr | 1 +
opam | 4 ++--
opam.pins | 1 -
7 files changed, 25 insertions(+), 32 deletions(-)
delete mode 100755 build/opam-pins.sh
create mode 100644 descr
delete mode 100644 opam.pins
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0dc9b472b..c08177622 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,9 +1,14 @@
image: ralfjung/opam-ci:latest
+stages:
+ - build
+ - opam
+
variables:
CPU_CORES: "9"
.template: &template
+ stage: build
tags:
- fp-timing
script:
@@ -23,6 +28,14 @@ variables:
- master
- /^ci/
+opam:
+ stage: opam
+ script:
+ # Send a trigger to the repository doing the work
+ - 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]=coq-iris" https://gitlab.mpi-sws.org/api/v3/projects/581/trigger/builds
+ only:
+ - master
+
iris-coq8.7:
<<: *template
variables:
diff --git a/Makefile b/Makefile
index 7bfa06f89..be2731d65 100644
--- a/Makefile
+++ b/Makefile
@@ -22,9 +22,7 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
# 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 opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
+ opam pin add opam-builddep-temp "$$(pwd)" -k path -n -y
opam install opam-builddep-temp --deps-only $(YFLAG)
opam pin remove opam-builddep-temp
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index 20d87f9d4..db3ca7868 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -19,6 +19,11 @@ 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
+test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
+
+# Make sure we have no undesired pins left from opam.pins times
+opam pin remove coq-stdpp -n
+opam pin remove coq-iris -n
# Install fixed versions of some dependencies
echo
@@ -34,6 +39,9 @@ while (( "$#" )); do # while there are arguments left
fi
done
+# Upgrade cached things
+opam upgrade -y
+
# Install build-dependencies
echo
make build-dep Y=1
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
deleted file mode 100755
index 5291cb234..000000000
--- a/build/opam-pins.sh
+++ /dev/null
@@ -1,26 +0,0 @@
-#!/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
-
-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/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
-done
diff --git a/descr b/descr
new file mode 100644
index 000000000..5a8a5a0e5
--- /dev/null
+++ b/descr
@@ -0,0 +1 @@
+This is the Coq development of the Iris Project.
diff --git a/opam b/opam
index ec5e2b4c3..8260924cd 100644
--- a/opam
+++ b/opam
@@ -13,7 +13,7 @@ build: [
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'" ]
depends: [
- "coq" { (>= "8.6.1" & < "8.8~") } # replace with (= "dev") if you want to test against a development version of Coq
+ "coq" { (>= "8.6.1" & < "8.8~") }
"coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev")) }
- "coq-stdpp"
+ "coq-stdpp" { ((= "dev.2017-09-18.1") | (= "dev")) }
]
diff --git a/opam.pins b/opam.pins
deleted file mode 100644
index 7af26ad43..000000000
--- a/opam.pins
+++ /dev/null
@@ -1 +0,0 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 7d7c9871312719a4e1296d52eb95ea0ac959249f
--
GitLab