aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorRalf Jung2017-09-28 16:40:13 +0200
committerRalf Jung2017-09-29 10:56:42 +0200
commit39eb1cfb3ac9bc12b6cd80e6bca7c4baf6b365c0 (patch)
tree5e0d938a5741edbf02688bb74ce25c2cfaa0845d /dev
parent4b6383889d4d38de4c9a28bee960b30114a51b16 (diff)
Iris CI: use opam to determine std++ git commit
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-iris-coq.sh16
1 files changed, 9 insertions, 7 deletions
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index 2d127ddc1b..4347da1da4 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -9,17 +9,19 @@ Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq
install_ssreflect
-# Setup Iris first, as it is needed to compute the dependencies
+# Add or update the opam repo we need for dependency resolution
+opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 0 || opam update iris-dev
+# Setup Iris first, extract required version of std++
git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR}
-read -a IRIS_DEP < ${Iris_CI_DIR}/opam.pins
+stdpp_VERSION=$(cat ${Iris_CI_DIR}/opam | fgrep coq-stdpp | egrep 'dev\.([0-9.-]+)' -o)
-# Setup stdpp
-stdpp_CI_GITURL=${IRIS_DEP[1]}.git
-stdpp_CI_COMMIT=${IRIS_DEP[2]}
-
-git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT}
+# Ask opam where to get this std++, separating at the #
+stdpp_URL=$(opam show coq-stdpp.$stdpp_VERSION -f upstream-url)
+read -a stdpp_URL_PARTS <<< $(echo $stdpp_URL | tr '#' ' ')
+# Setup std++
+git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[1]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[2]}
( cd ${stdpp_CI_DIR} && make && make install )
# Build iris now