aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-07-20 15:53:13 -0700
committerGravatar Jason Gross <jagro@google.com>2016-07-20 18:48:04 -0700
commit63cec62a5ae63f545f9db845e14552d6df19b86e (patch)
tree1aec236b42cc23f065182550a9ce7b048823463b /Makefile
parent3b89a26a5266f33dbfdf6968557de29a471098ab (diff)
Add support for TIMED=1 in Coq 8.4
This should fix #34
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile14
1 files changed, 11 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index c4c9f0c6b..03e0ccfcf 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,9 @@
MOD_NAME := Crypto
SRC_DIR := src
+TIMED?=
+TIMECMD?=
STDTIME?=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
VERBOSE?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
@@ -15,6 +18,14 @@ SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g'
FAST_TARGETS += archclean clean cleanall printenv clean-old update-_CoqProject Makefile.coq
SUPER_FAST_TARGETS += update-_CoqProject Makefile.coq
+COQ_VERSION_PREFIX = The Coq Proof Assistant, version
+COQ_VERSION := $(firstword $(subst $(COQ_VERSION_PREFIX),,$(shell "$(COQBIN)coqc" --version 2>/dev/null)))
+
+ifneq ($(filter 8.4%,$(COQ_VERSION)),) # 8.4
+# Give us TIMED=1 in Coq 8.4
+COQC?=$(TIMER) "$(COQBIN)coqc"
+endif
+
-include Makefile.coq
.DEFAULT_GOAL := coq
@@ -36,9 +47,6 @@ specific: $(SPECIFIC_VO) coqprime
non-specific: $(NON_SPECIFIC_VO) coqprime
coq: $(COQ_VOFILES) coqprime
-COQ_VERSION_PREFIX = The Coq Proof Assistant, version
-COQ_VERSION := $(firstword $(subst $(COQ_VERSION_PREFIX),,$(shell $(COQBIN)coqc --version 2>/dev/null)))
-
ifneq ($(filter 8.4%,$(COQ_VERSION)),) # 8.4
COQPRIME_FOLDER := coqprime-8.4
else