Commit 0b6bb546 authored by Ralf Jung's avatar Ralf Jung
Browse files

update build system

parent c3241b22
...@@ -3,14 +3,6 @@ ifeq ($(Y), 1) ...@@ -3,14 +3,6 @@ ifeq ($(Y), 1)
YFLAG=-y YFLAG=-y
endif 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) # Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony %: Makefile.coq phony
+@make -f Makefile.coq $@ +@make -f Makefile.coq $@
...@@ -25,7 +17,7 @@ clean: 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. # 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 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 mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# Install build-dependencies # Install build-dependencies
......
-Q theories iris -Q theories iris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/algebra/cmra.v theories/algebra/cmra.v
theories/algebra/cmra_big_op.v theories/algebra/cmra_big_op.v
theories/algebra/cmra_tactics.v theories/algebra/cmra_tactics.v
......
...@@ -4,18 +4,23 @@ set -e ...@@ -4,18 +4,23 @@ set -e
## Usage: ## Usage:
## ./opam-pins.sh < opam.pins ## ./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 # Process stdin
while read PACKAGE URL HASH; do while read PACKAGE URL HASH; do
if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
echo "[opam-pins] Recursing into $URL" echo "[opam-pins] Recursing into $URL"
# an MPI URL -- try doing recursive pin processing # 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 fi
if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
echo "[opam-pins] $PACKAGE already at commit $HASH" echo "[opam-pins] $PACKAGE already at commit $HASH"
else else
echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH" echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
fi
echo echo
fi
done done
...@@ -13,7 +13,7 @@ build: [ ...@@ -13,7 +13,7 @@ build: [
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'" ]
depends: [ depends: [
"coq" { ((>= "8.5.1" & < "8.7~") | (= "dev"))} "coq" { ((>= "8.6" & < "8.7~") | (= "dev"))}
"coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev"))} "coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev"))}
"coq-stdpp" "coq-stdpp"
] ]
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment