diff --git a/.gitignore b/.gitignore index 7e4e4f0c2ef39f99a65bc9eb8d7fba1da5953b9b..90fe9644eb6393f34d12c56ad4c8e86cd1e30ca2 100644 --- a/.gitignore +++ b/.gitignore @@ -12,3 +12,4 @@ Makefile.coq* *.crashcoqide html/ +build-dep/ diff --git a/Makefile b/Makefile index 7bfa06f89a5c19f9b279f65875196f870b6f88c7..a8c1e0574582a8bf06276f2339ad98864961a7c6 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 5291cb234701dbaba66e19717a4ef242fc9e83e8..0000000000000000000000000000000000000000 --- 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 d6a40c1d4a337c070ec544ebeead5d8c429d2a40..b86fc53dd15990ddab8aea2607da4fe483c6a38c 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 e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000