summaryrefslogtreecommitdiff
path: root/test-suite/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile224
1 files changed, 122 insertions, 102 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index ae1562c7..4a3a287c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -30,15 +30,11 @@
BIN := ../bin/
LIB := ..
-ifeq ($(BEST),byte)
- coqtop := $(BIN)coqtop.byte -boot -q -batch -I prerequisite
- bincoqc := $(BIN)coqc -coqlib $(LIB) -byte -I prerequisite
-else
- coqtop := $(BIN)coqtop -boot -q -batch -I prerequisite
- bincoqc := $(BIN)coqc -coqlib $(LIB) -I prerequisite
-endif
+coqtop := $(BIN)coqtop -boot -q -batch -R prerequisite TestSuite
+bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
+bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
-command := $(coqtop) -top Top -load-vernac-source
+command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
coqc := $(coqtop) -compile
coqdep := $(BIN)coqdep -coqlib $(LIB)
@@ -46,7 +42,16 @@ SHOW := $(if $(VERBOSE),@true,@echo)
HIDE := $(if $(VERBOSE),,@)
REDIR := $(if $(VERBOSE),,> /dev/null 2>&1)
-bogomips :=
+# read out an emacs config and look for coq-prog-args; if such exists, return it
+get_coq_prog_args_helper = sed -n s'/^.*coq-prog-args:[[:space:]]*(\([^)]*\)).*/\1/p' $(1)
+get_coq_prog_args = $(strip $(filter-out "-emacs-U" "-emacs",$(shell $(call get_coq_prog_args_helper,$(1)))))
+SINGLE_QUOTE="
+#" # double up on the quotes, in a comment, to appease the emacs syntax highlighter
+# wrap the arguments in parens, but only if they exist
+get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
+
+
+bogomips:=
ifneq (,$(wildcard /proc/cpuinfo))
sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc
sedbogo += -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" # sparc
@@ -59,6 +64,8 @@ ifeq (,$(bogomips))
endif
log_success = "==========> SUCCESS <=========="
+log_segfault = "==========> FAILURE <=========="
+log_anomaly = "==========> FAILURE <=========="
log_failure = "==========> FAILURE <=========="
log_intro = "==========> TESTING $(1) <=========="
@@ -69,14 +76,13 @@ log_intro = "==========> TESTING $(1) <=========="
# Apart so that it can be easily skipped with overriding
COMPLEXITY := $(if $(bogomips),complexity)
-BUGS := bugs/opened/shouldnotfail bugs/opened/shouldnotsucceed \
- bugs/closed/shouldsucceed bugs/closed/shouldfail
+BUGS := bugs/opened bugs/closed
VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
- interactive micromega $(COMPLEXITY) modules
+ interactive micromega $(COMPLEXITY) modules stm
# All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
#######################################################################
# Phony targets
@@ -93,11 +99,14 @@ bugs: $(BUGS)
clean:
rm -f trace lia.cache
- $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.log>"
+ $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>"
$(HIDE)find . \( \
- -name '*.stamp' -o -name '*.vo' -o -name '*.log' \
+ -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \
\) -print0 | xargs -0 rm -f
+distclean: clean
+ $(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f
+
#######################################################################
# Per-subsystem targets
#######################################################################
@@ -113,7 +122,7 @@ $(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S))))
# Summary
#######################################################################
-summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 -n 1 tail -n1 | sort -g
+summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 -n 1 tail -n1 | sort
.PHONY: summary summary.log
@@ -129,7 +138,10 @@ summary:
$(call summary_dir, "Miscellaneous tests", misc); \
$(call summary_dir, "Complexity tests", complexity); \
$(call summary_dir, "Module tests", modules); \
+ $(call summary_dir, "STM tests", stm); \
$(call summary_dir, "IDE tests", ide); \
+ $(call summary_dir, "VI tests", vio); \
+ $(call summary_dir, "Coqchk tests", coqchk); \
nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
nb_tests=`expr $$nb_success + $$nb_failure`; \
@@ -152,32 +164,21 @@ summary.log:
# All files are assumed to have <# of the bug>.v as a name
-# Opened bugs that should not succeed (FIXME: there were no such tests
-# at the time of writing this Makefile, but the possibility was in the
-# original shellscript... so left it here, but untested)
-$(addsuffix .log,$(wildcard bugs/opened/shouldnotsucceed/*.v)): %.v.log: %.v
- @echo "TEST $<"
- $(HIDE){ \
- $(call test_intro,$<); \
- $(command) "$<" 2>&1; R=$$?; times; \
- if [ $$R = 0 ]; then \
- echo $(log_success); \
- echo " $<...still active"; \
- else \
- echo $(log_failure); \
- echo " $<...Error! (bug seems to be closed, please check)";
- fi;
- } > "$@"
-
# Opened bugs that should not fail
-$(addsuffix .log,$(wildcard bugs/opened/shouldnotfail/*.v)): %.v.log: %.v
- @echo "TEST $<"
+$(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" 2>&1; R=$$?; times; \
- if [ $$R != 0 ]; then \
+ $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...still active"; \
+ elif [ $$R = 129 ]; then \
+ echo $(log_anomaly); \
+ echo " $<...still active"; \
+ elif [ $$R = 139 ]; then \
+ echo $(log_segfault); \
+ echo " $<...still active"; \
else \
echo $(log_failure); \
echo " $<...Error! (bug seems to be closed, please check)"; \
@@ -185,11 +186,11 @@ $(addsuffix .log,$(wildcard bugs/opened/shouldnotfail/*.v)): %.v.log: %.v
} > "$@"
# Closed bugs that should succeed
-$(addsuffix .log,$(wildcard bugs/closed/shouldsucceed/*.v)): %.v.log: %.v
- @echo "TEST $<"
+$(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" 2>&1; R=$$?; times; \
+ $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -199,30 +200,15 @@ $(addsuffix .log,$(wildcard bugs/closed/shouldsucceed/*.v)): %.v.log: %.v
fi; \
} > "$@"
-# Closed bugs that should fail
-$(addsuffix .log,$(wildcard bugs/closed/shouldfail/*.v)): %.v.log: %.v
- @echo "TEST $<"
- $(HIDE){ \
- echo $(call log_intro,$<); \
- $(command) "$<" 2>&1; R=$$?; times; \
- if [ $$R != 0 ]; then \
- echo $(log_success); \
- echo " $<...Ok"; \
- else \
- echo $(log_failure); \
- echo " $<...Error! (bug seems to be opened, please check)"; \
- fi; \
- } > "$@"
-
#######################################################################
# Other generic tests
#######################################################################
$(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
- @echo "TEST $<"
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(coqc) "$*" 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" ; \
@@ -233,11 +219,28 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
} > "$@"
$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v
- @echo "TEST $<"
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
+ $(HIDE){ \
+ opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
+ echo $(call log_intro,$<); \
+ $(command) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
+ if [ $$R = 0 ]; then \
+ echo $(log_success); \
+ echo " $<...Ok"; \
+ else \
+ echo $(log_failure); \
+ echo " $<...Error! (should be accepted)"; \
+ fi; \
+ } > "$@"
+
+stm: $(wildcard stm/*.v:%.v=%.v.log)
+$(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
- opts="$(if $(findstring modules/,$<),-I modules -impredicative-set)"; \
echo $(call log_intro,$<); \
- $(command) "$<" $$opts 2>&1; R=$$?; times; \
+ $(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 \
echo $(log_success); \
echo " $<...Ok"; \
@@ -248,11 +251,11 @@ $(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.
} > "$@"
$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v
- @echo "TEST $<"
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" 2>&1; R=$$?; times; \
- if [ $$R != 0 ]; then \
+ $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
else \
@@ -261,13 +264,14 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v
fi; \
} > "$@"
-$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v
- @echo "TEST $<"
+$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
- $(command) "$<" 2>&1 \
+ $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
| grep -v "Welcome to Coq" \
+ | grep -v "\[Loading ML file" \
| grep -v "Skipping rcfile loading" \
> $$tmpoutput; \
diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \
@@ -282,10 +286,10 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v
} > "$@"
$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
- @echo "TEST $<"
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(coqtop) < "$<" 2>&1; R=$$?; times; \
+ $(coqtop) $(call get_coq_prog_args,"$<") < "$<" 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -300,11 +304,11 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
# time is a 6120 bogomips cpu.
ifneq (,$(bogomips))
$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v
- @echo "TEST $<"
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
true "extract effective user time"; \
- res=`$(command) "$<" 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
+ res=`$(command) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
R=$$?; times; \
if [ $$R != 0 ]; then \
echo $(log_failure); \
@@ -331,10 +335,10 @@ endif
# Ideal-features tests
$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
- @echo "TEST $<"
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" 2>&1; R=$$?; times; \
+ $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R != 0 ]; then \
echo $(log_success); \
echo " $<...still wished"; \
@@ -346,35 +350,17 @@ $(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
-%.vo: %.v
- $(HIDE)$(coqtop) -compile $*
+modules/%.vo: modules/%.v
+ $(HIDE)$(coqtop) -R modules Mods -compile $(<:.v=)
#######################################################################
# Miscellaneous tests
#######################################################################
-misc: misc/xml.log misc/deps-order.log misc/universes.log
+misc: misc/deps-order.log misc/universes.log
-# Test xml compilation
-xml: misc/xml.log
-misc/xml.log:
- @echo "TEST misc/xml"
- $(HIDE){ \
- echo $(call log_intro,xml); \
- rm -rf misc/xml; \
- COQ_XML_LIBRARY_ROOT=misc/xml \
- $(bincoqc) -xml misc/berardi_test 2>&1; times; \
- if [ ! -d misc/xml ]; then \
- echo $(log_failure); \
- echo " misc/xml... failed"; \
- else \
- echo $(log_success); \
- echo " misc/xml...apparently ok"; \
- fi; rm -rf misc/xml; \
- } > "$@"
-
-# Check that both coqdep and coqtop/coqc takes the later -I/-R
-# Check that both coqdep and coqtop/coqc supports both -R and -I dir -as lib
+# Check that both coqdep and coqtop/coqc supports -R
+# Check that both coqdep and coqtop/coqc takes the later -R
# See bugs 2242, 2337, 2339
deps-order: misc/deps-order.log
misc/deps-order.log:
@@ -383,12 +369,12 @@ misc/deps-order.log:
echo $(call log_intro,deps-order); \
rm -f misc/deps/*/*.vo; \
tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
- $(coqdep) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \
+ $(coqdep) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \
| head -n 1 > $$tmpoutput; \
diff -u misc/deps/deps.out $$tmpoutput 2>&1; R=$$?; times; \
- $(bincoqc) -I misc/deps/lib -as lib misc/deps/lib/foo.v 2>&1; \
- $(bincoqc) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \
- $(coqtop) -I misc/deps/lib -as lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \
+ $(bincoqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \
+ $(bincoqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \
+ $(coqtop) -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \
S=$$?; times; \
if [ $$R = 0 -a $$S = 0 ]; then \
echo $(log_success); \
@@ -406,8 +392,8 @@ universes: misc/universes.log
misc/universes.log: misc/universes/all_stdlib.v
@echo "TEST misc/universes"
$(HIDE){ \
- $(bincoqc) -I misc/universes misc/universes/all_stdlib 2>&1; \
- $(bincoqc) -I misc/universes misc/universes/universes 2>&1; \
+ $(bincoqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \
+ $(bincoqc) -R misc/universes Universes misc/universes/universes 2>&1; \
mv universes.txt misc/universes; \
N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \
times; \
@@ -432,7 +418,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
@echo "TEST $<"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(BIN)fake_ide "$(BIN)coqtop -boot" < $< 2>&1; \
+ $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on" 2>&1; \
if [ $$? = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -441,3 +427,37 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
echo " $<...Error!"; \
fi; \
} > "$@"
+
+vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
+
+%.vio.log:%.v
+ @echo "TEST $<"
+ $(HIDE){ \
+ $(bincoqc) -quick -R vio vio $* 2>&1 && \
+ $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \
+ $(bincoqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \
+ if [ $$? = 0 ]; then \
+ echo $(log_success); \
+ echo " $<...Ok"; \
+ else \
+ echo $(log_failure); \
+ echo " $<...Error!"; \
+ fi; \
+ } > "$@"
+
+coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
+
+%.chk.log:%.v
+ @echo "TEST $<"
+ $(HIDE){ \
+ $(bincoqc) -R coqchk coqchk $* 2>&1 && \
+ $(bincoqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \
+ if [ $$? = 0 ]; then \
+ echo $(log_success); \
+ echo " $<...Ok"; \
+ else \
+ echo $(log_failure); \
+ echo " $<...Error!"; \
+ fi; \
+ } > "$@"
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-12 14:43:18 +0000