From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/Makefile | 224 ++++++++++++++++++++++++++++------------------------ 1 file changed, 122 insertions(+), 102 deletions(-) (limited to 'test-suite/Makefile') 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; \ + } > "$@" + -- cgit v1.2.3