aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile8
-rw-r--r--README.md4
2 files changed, 11 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 3be8c6754..0deb7bd28 100644
--- a/Makefile
+++ b/Makefile
@@ -63,6 +63,9 @@ OTHERFLAGS ?= -w "-deprecated-appcontext -notation-overridden"
endif
endif
+COQPATH?=$(shell pwd)/$(COQPRIME_FOLDER)
+export COQPATH
+
coqprime:
$(MAKE) -C $(COQPRIME_FOLDER)
@@ -74,7 +77,7 @@ install-coqprime:
Makefile.coq: Makefile _CoqProject
$(SHOW)'COQ_MAKEFILE -f _CoqProject > $@'
- $(HIDE)$(COQBIN)coq_makefile -f _CoqProject | sed s'|^\(-include.*\)$$|ifneq ($$(filter-out $(FAST_TARGETS),$$(MAKECMDGOALS)),)~\1~else~ifeq ($$(MAKECMDGOALS),)~\1~endif~endif|g' | tr '~' '\n' | sed s'/^clean:$$/clean::/g' | sed s'/^Makefile: /Makefile-old: /g' > $@
+ $(HIDE)$(COQBIN)coq_makefile -f _CoqProject | sed s'|^\(-include.*\)$$|ifneq ($$(filter-out $(FAST_TARGETS),$$(MAKECMDGOALS)),)~\1~else~ifeq ($$(MAKECMDGOALS),)~\1~endif~endif|g' | tr '~' '\n' | sed s'/^clean:$$/clean::/g' | sed s'/^Makefile: /Makefile-old: /g' | sed s'/^printenv:$$/printenv::/g' > $@
clean::
rm -f Makefile.coq
@@ -84,5 +87,8 @@ cleanall:: clean clean-coqprime
install: coq install-coqprime
+printenv::
+ @echo "COQPATH = $$COQPATH"
+
.dir-locals.el::
sed 's:@COQPRIME@:$(COQPRIME_FOLDER):g' .dir-locals.el.in > $@
diff --git a/README.md b/README.md
index c20a08528..2bc177c68 100644
--- a/README.md
+++ b/README.md
@@ -6,6 +6,10 @@ Fiat-Crypto: Synthesizing Correct-by-Construction Assembly for Cryptographic Pri
NOTE: The github.com repo is only intermittently synced with
github.mit.edu.
+To build (if your COQPATH variable is empty):
+
+ make
+
To build (Coq 8.5):
export COQPATH="$(pwd)/coqprime${COQPATH:+:}$COQPATH"