diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/ci-common.sh | 21 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 5 | ||||
| -rw-r--r-- | dev/ci/user-overlays/09439-sep-variance.sh | 14 |
3 files changed, 27 insertions, 13 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index a5aa54144c..b4d2a9ca4e 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -62,27 +62,30 @@ git_download() { local PROJECT=$1 local DEST="$CI_BUILD_DIR/$PROJECT" + local GITURL_VAR="${PROJECT}_CI_GITURL" + local GITURL="${!GITURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" if [ -d "$DEST" ]; then echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists." elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then - local GITURL_VAR="${PROJECT}_CI_GITURL" - local GITURL="${!GITURL_VAR}" - local REF_VAR="${PROJECT}_CI_REF" - local REF="${!REF_VAR}" git clone "$GITURL" "$DEST" cd "$DEST" git checkout "$REF" else # When possible, we download tarballs to reduce bandwidth and latency local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL" local ARCHIVEURL="${!ARCHIVEURL_VAR}" - local REF_VAR="${PROJECT}_CI_REF" - local REF="${!REF_VAR}" mkdir -p "$DEST" cd "$DEST" - wget "$ARCHIVEURL/$REF.tar.gz" - tar xvfz "$REF.tar.gz" --strip-components=1 - rm -f "$REF.tar.gz" + local COMMIT=$(git ls-remote "$GITURL" "refs/heads/$REF" | cut -f 1) + if [[ "$COMMIT" == "" ]]; then + # $REF must have been a tag or hash, not a branch + COMMIT="$REF" + fi + wget "$ARCHIVEURL/$COMMIT.tar.gz" + tar xvfz "$COMMIT.tar.gz" --strip-components=1 + rm -f "$COMMIT.tar.gz" fi } diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 4cd7faf757..43278c37b1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-01-28-V1" +# CACHEKEY: "bionic_coq-V2019-02-17-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -56,9 +56,6 @@ ENV COMPILER_EDGE="4.07.1" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ BASE_OPAM_EDGE="dune-release.1.1.0" -RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ - opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE - # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \ diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh new file mode 100644 index 0000000000..cca85a2f68 --- /dev/null +++ b/dev/ci/user-overlays/09439-sep-variance.sh @@ -0,0 +1,14 @@ + +if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then + elpi_CI_REF=sep-variance + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=sep-variance + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + mtac2_CI_REF=sep-variance + mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 + + paramcoq_CI_REF=sep-variance + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq +fi |