From 4b6af89cc9ca8cdc4cfb25a8fcb35d3c89d92bc6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 20 Sep 2017 13:22:58 +0200
Subject: [PATCH] no more opam.pins
---
.gitignore | 1 +
Makefile | 28 ++++++++++++++++------------
build/opam-pins.sh | 26 --------------------------
opam | 4 +---
opam.pins | 0
5 files changed, 18 insertions(+), 41 deletions(-)
delete mode 100755 build/opam-pins.sh
delete mode 100644 opam.pins
diff --git a/.gitignore b/.gitignore
index 7e4e4f0c..90fe9644 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,3 +12,4 @@
Makefile.coq*
*.crashcoqide
html/
+build-dep/
diff --git a/Makefile b/Makefile
index 7bfa06f8..a8c1e057 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,3 @@
-# Process flags
-ifeq ($(Y), 1)
- YFLAG=-y
-endif
-
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
@@ -15,18 +10,27 @@ clean: Makefile.coq
find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
rm -f Makefile.coq
-# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real filename, so we do some file gymnastics.
+# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
+# filename, so we do some file gymnastics.
Makefile.coq: _CoqProject Makefile awk.Makefile
coq_makefile -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# 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 install opam-builddep-temp --deps-only $(YFLAG)
- opam pin remove opam-builddep-temp
+build-dep: phony
+ @# We want opam to not just instal the build-deps now, but to also keep satisfying these
+ @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
+ @# that are incompatible with our build requirements.
+ @# To achieve this, we create a fake opam package that has our build-dependencies as
+ @# dependencies, but does not actually install anything.
+ mkdir -p build-dep
+ # Create the build-dep package, add the pin and (re)install it.
+ @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
+ @# 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"
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
deleted file mode 100755
index 5291cb23..00000000
--- 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/opam b/opam
index d6a40c1d..b86fc53d 100644
--- a/opam
+++ b/opam
@@ -7,9 +7,7 @@ authors: "Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung"
bug-reports: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/issues"
license: "BSD"
dev-repo: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git"
-build: [
- [make "-j%{jobs}%"]
-]
+build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/stdpp'" ]
depends: [
diff --git a/opam.pins b/opam.pins
deleted file mode 100644
index e69de29b..00000000
--
GitLab