diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-10 10:49:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-10 10:49:09 +0200 |
| commit | 7467198ed666669f28038430dc83ad0241238634 (patch) | |
| tree | 488ee1e472765aaad5f3f1a377883f92fa0cea1d /dev/ci | |
| parent | 1aeb43a3c7779001b0404d9dcc1603bf4c49dee0 (diff) | |
| parent | 388db1f6be8a52d0585cdf48489dfab8499d7ef5 (diff) | |
Merge PR #1067: Iris CI: use opam to install dependencies
Diffstat (limited to 'dev/ci')
| -rwxr-xr-x | dev/ci/ci-iris-coq.sh | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index 2d127ddc1..c49b6ed9c 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[0]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[1]} ( cd ${stdpp_CI_DIR} && make && make install ) # Build iris now |