From 842e85c0432d427f0b72bc98349a51764dee236c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 19 Sep 2017 14:44:11 +0200
Subject: [PATCH] CI: tweaks
---
.gitlab-ci.yml | 2 +-
Makefile | 4 ++--
build/opam-ci.sh | 4 +++-
3 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6c26341e8..2cd43b62c 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 3644fec89..97b9487b5 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 73f621291..94c738e52 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
--
GitLab