summaryrefslogtreecommitdiff
path: root/test-suite/Makefile
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /test-suite/Makefile
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile12
1 files changed, 6 insertions, 6 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index cffbe481..31b21290 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -28,9 +28,9 @@
# Default value when called from a freshly compiled Coq, but can be
# easily overridden
BIN := ../bin/
-LIB := ..
+LIB := $(shell cd ..; pwd)
-coqtop := $(BIN)coqtop -boot -q -batch -R prerequisite TestSuite
+coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite
bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
@@ -208,7 +208,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(coqc) "$*" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R != 0 ]; then \
echo $(log_failure); \
echo " $<...could not be prepared" ; \
@@ -238,7 +238,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(coqc) "$*" $(call get_coq_prog_args,"$<") -async-proofs on \
+ $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \
-async-proofs-private-flags fallback-to-lazy-if-marshal-error=no,fallback-to-lazy-if-slave-dies=no \
$$opts 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
@@ -352,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
# Additionnal dependencies for module tests
$(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo
modules/%.vo: modules/%.v
- $(HIDE)$(coqtop) -R modules Mods -compile $(<:.v=)
+ $(HIDE)$(coqtop) -R modules Mods -compile $<
#######################################################################
# Miscellaneous tests
@@ -388,7 +388,7 @@ misc/deps-order.log:
} > "$@"
# Sort universes for the whole standard library
-EXPECTED_UNIVERSES := 3
+EXPECTED_UNIVERSES := 5
universes: misc/universes.log
misc/universes.log: misc/universes/all_stdlib.v
@echo "TEST misc/universes"