diff --git a/Makefile b/Makefile index 6394c42a5c3cd9ecfa57864c33cf15f87b0549cc..7bfa06f89a5c19f9b279f65875196f870b6f88c7 100644 --- a/Makefile +++ b/Makefile @@ -3,14 +3,6 @@ ifeq ($(Y), 1) YFLAG=-y endif -# Determine Coq version -COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]') -COQ_MAKEFILE_FLAGS ?= - -ifeq ($(COQ_VERSION), 8.6) - COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files -endif - # Forward most targets to Coq makefile (with some trick to make this phony) %: Makefile.coq phony +@make -f Makefile.coq $@ @@ -25,7 +17,7 @@ clean: 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. Makefile.coq: _CoqProject Makefile awk.Makefile - coq_makefile $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq + 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 diff --git a/_CoqProject b/_CoqProject index 99afce68ce287ee66d07fdc33095f8a96fc2f4d4..dbeb27192793aeb041d3f2ebe60e9ae02431656b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,5 @@ -Q theories iris +-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files theories/algebra/cmra.v theories/algebra/cmra_big_op.v theories/algebra/cmra_tactics.v diff --git a/build/opam-pins.sh b/build/opam-pins.sh index 669cd99b833df5259808f3b8f3fae1f96f466271..5291cb234701dbaba66e19717a4ef242fc9e83e8 100755 --- a/build/opam-pins.sh +++ b/build/opam-pins.sh @@ -4,18 +4,23 @@ set -e ## 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" 2> /dev/null | "$0" + 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 - echo done diff --git a/opam b/opam index f3f2e979e0c4a182dcfcfc2838c33679122c317b..ea44830afe14223fca69264c3d71383126bd61e1 100644 --- a/opam +++ b/opam @@ -13,7 +13,7 @@ build: [ install: [make "install"] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'" ] depends: [ - "coq" { ((>= "8.5.1" & < "8.7~") | (= "dev"))} + "coq" { ((>= "8.6" & < "8.7~") | (= "dev"))} "coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev"))} "coq-stdpp" ]