From b5fa9b29d1fa06d3d7c46eeda9a8ebb91bf24ccd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 Jan 2017 19:02:27 +0100
Subject: [PATCH] avoid re-downloading already properly pinned packages
---
.gitlab-ci.yml | 2 +-
build/opam-ci.sh | 14 ++++++++++----
build/opam-pins.sh | 8 ++++++--
3 files changed, 17 insertions(+), 7 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 27b7707fe..28e8e1605 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -5,7 +5,7 @@ iris-coq8.6:
- coq
script:
# prepare
- - . build/opam-ci.sh 'coq 8.6' 'coq-mathcomp-ssreflect 1.6.1'
+ - . build/opam-ci.sh coq 8.6 coq-mathcomp-ssreflect 1.6.1
# build
- 'time make -j8'
cache:
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index 9a10038de..c4189bab6 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -17,10 +17,16 @@ opam update
# Install fixed versions of some dependencies
echo
-for PIN in "${@}"
-do
- echo "Applying pin: $PIN"
- opam pin add $PIN -k version -y
+while (( "$#" )); do # while there are arguments left
+ PACKAGE="$1" ; shift
+ VERSION="$1" ; shift
+ # Check if the pin is already set
+ if opam pin list | fgrep "$PACKAGE.$VERSION " > /dev/null; then
+ echo "[opam-ci] $PACKAGE already pinned to $VERSION"
+ else
+ echo "[opam-ci] Pinning $PACKAGE to $VERSION"
+ opam pin add "$PACKAGE" "$VERSION" -k version -y
+ fi
done
# Install build-dependencies
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
index aebd23ca2..669cd99b8 100755
--- a/build/opam-pins.sh
+++ b/build/opam-pins.sh
@@ -11,7 +11,11 @@ while read PACKAGE URL HASH; do
# an MPI URL -- try doing recursive pin processing
curl -f "$URL/raw/$HASH" 2> /dev/null | "$0"
fi
- echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
- opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
+ 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
+ fi
echo
done
--
GitLab