diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6c26341e866d396d3dd9752b24281c820b4d0054..2cd43b62c481b956d0ec0507604685eb40d1645f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -21,7 +21,7 @@ variables: - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt' - 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi' cache: - key: "coq$COQ_VERSION-ssr$SSR_VERSION" + key: "coq.$COQ_VERSION-ssr.$SSR_VERSION" paths: - opamroot/ only: diff --git a/Makefile b/Makefile index 3644fec8947d1b2824d571b6a048d8f66813019e..97b9487b5abf7b457a922f469bc8a36ca0038c3c 100644 --- a/Makefile +++ b/Makefile @@ -26,8 +26,8 @@ build-dep: phony mkdir -p build-dep @sed <opam 's/^\(build\|install\|remove\):.*/\1: []/; s/^name: *"\(.*\)" */name: "\1-builddep"/' > build-dep/opam @fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check - @# Compute the package name, add the pin and (re)install it. Reinstallation is needed - @# in case the pin already exists, but the builddep package changed. + # Compute the package name, add the pin and (re)install it. + @# Reinstallation is needed in case the pin already exists, but the builddep package changed. @BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \ opam pin add "$$BUILD_DEP_PACKAGE" "$$(pwd)/build-dep" -k path $(OPAMFLAGS) && \ opam reinstall "$$BUILD_DEP_PACKAGE" diff --git a/build/opam-ci.sh b/build/opam-ci.sh index 73f621291e3e737708e3030bca40db4c88da1661..94c738e52845312a7f8c45660917b4ad87c97fd7 100755 --- a/build/opam-ci.sh +++ b/build/opam-ci.sh @@ -1,6 +1,6 @@ #!/bin/bash set -e -# This script installs the build dependencies for CI builds. +## This script installs the build dependencies for CI builds. # Prepare OPAM configuration export OPAMROOT="$(pwd)/opamroot" @@ -44,10 +44,12 @@ while (( "$#" )); do # while there are arguments left done # Upgrade cached things. +echo "[opam-ci] Upgrading opam" opam upgrade -y # Install build-dependencies. echo +echo "[opam-ci] Installing build-dependencies" make build-dep OPAMFLAGS=-y # done