diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 0dc9b472b178bf7d4c49b9c4853162cfc86db5be..c081776228a82845e3a3e4813b6661864576daf8 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 7bfa06f89a5c19f9b279f65875196f870b6f88c7..be2731d656d3103fc04f8b93f217e81455332683 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 20d87f9d4da508096531227791ccce63da17bd6f..db3ca7868450cf294fa560de8c4b52dca907c570 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 5291cb234701dbaba66e19717a4ef242fc9e83e8..0000000000000000000000000000000000000000 --- 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 0000000000000000000000000000000000000000..5a8a5a0e57e0fa3c105bb39204538f814a872bfc --- /dev/null +++ b/descr @@ -0,0 +1 @@ +This is the Coq development of the Iris Project. diff --git a/opam b/opam index ec5e2b4c3889059edfceb9dd348e2f4bb576cc12..8260924cdc2eeab9107227291bf80081fb96f7f4 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 7af26ad434a7dd207eb035c8a7da483e68358851..0000000000000000000000000000000000000000 --- a/opam.pins +++ /dev/null @@ -1 +0,0 @@ -coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 7d7c9871312719a4e1296d52eb95ea0ac959249f