aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile70
1 files changed, 55 insertions, 15 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 8500ef1b3..10eb2df39 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -49,6 +49,10 @@ 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)))))
+# get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
+has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
+has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
+get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command))
bogomips:=
@@ -79,7 +83,7 @@ COMPLEXITY := $(if $(bogomips),complexity)
BUGS := bugs/opened bugs/closed
VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
- interactive micromega $(COMPLEXITY) modules stm
+ output-modulo-time interactive micromega $(COMPLEXITY) modules stm
# All subsystems
SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
@@ -92,7 +96,7 @@ SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
.PHONY: all run clean $(SUBSYSTEMS)
all: run
- $(MAKE) --quiet summary.log
+ $(MAKE) report
run: $(SUBSYSTEMS)
bugs: $(BUGS)
@@ -133,6 +137,7 @@ summary:
$(call summary_dir, "Failure tests", failure); \
$(call summary_dir, "Bugs tests", bugs); \
$(call summary_dir, "Output tests", output); \
+ $(call summary_dir, "Output (modulo time changes) tests", output-modulo-time); \
$(call summary_dir, "Interactive tests", interactive); \
$(call summary_dir, "Micromega tests", micromega); \
$(call summary_dir, "Miscellaneous tests", misc); \
@@ -151,11 +156,11 @@ summary:
}
summary.log:
- $(SHOW) SUMMARY
+ $(SHOW) BUILDING SUMMARY FILE
$(HIDE)$(MAKE) --quiet summary > "$@"
report: summary.log
- $(HIDE)if grep -F 'Error!' summary.log ; then false; fi
+ $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi
#######################################################################
# Regression (and progression) tests
@@ -172,7 +177,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...still active"; \
@@ -193,7 +198,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -226,7 +231,7 @@ $(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.
$(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; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -242,7 +247,6 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
$(HIDE){ \
echo $(call log_intro,$<); \
$(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); \
@@ -257,7 +261,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -272,11 +276,12 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
$(HIDE){ \
echo $(call log_intro,$<); \
tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
- $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
| grep -v "Welcome to Coq" \
| grep -v "\[Loading ML file" \
| grep -v "Skipping rcfile loading" \
| grep -v "^<W>" \
+ | sed 's/File "[^"]*"/File "stdin"/' \
> $$tmpoutput; \
diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
@@ -289,6 +294,42 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
rm $$tmpoutput; \
} > "$@"
+$(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
+ $(HIDE){ \
+ echo $(call log_intro,$<); \
+ tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
+ tmpexpected=`mktemp /tmp/coqcheck.XXXXXX`; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+ | grep -v "Welcome to Coq" \
+ | grep -v "\[Loading ML file" \
+ | grep -v "Skipping rcfile loading" \
+ | grep -v "^<W>" \
+ | sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \
+ -e 's/\s*0\.\s*//g' \
+ -e 's/\s*[-+]nan\s*//g' \
+ -e 's/\s*[-+]inf\s*//g' \
+ -e 's/^[^a-zA-Z]*//' \
+ | sort \
+ > $$tmpoutput; \
+ sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \
+ -e 's/\s*0\.\s*//g' \
+ -e 's/\s*[-+]nan\s*//g' \
+ -e 's/\s*[-+]inf\s*//g' \
+ -e 's/^[^a-zA-Z]*//' \
+ $*.out | sort > $$tmpexpected; \
+ diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \
+ if [ $$R = 0 ]; then \
+ echo $(log_success); \
+ echo " $<...Ok"; \
+ else \
+ echo $(log_failure); \
+ echo " $<...Error! (unexpected output)"; \
+ fi; \
+ rm $$tmpoutput; \
+ rm $$tmpexpected; \
+ } > "$@"
+
$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
@@ -312,7 +353,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
$(HIDE){ \
echo $(call log_intro,$<); \
true "extract effective user time"; \
- 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`; \
+ res=`$(call get_command_based_on_flags,"$<") "$<" $(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); \
@@ -342,7 +383,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R != 0 ]; then \
echo $(log_success); \
echo " $<...still wished"; \
@@ -411,7 +452,7 @@ misc/deps-checksum.log:
# Sort universes for the whole standard library
-EXPECTED_UNIVERSES := 5
+EXPECTED_UNIVERSES := 4 # Prop is not counted
universes: misc/universes.log
misc/universes.log: misc/universes/all_stdlib.v
@echo "TEST misc/universes"
@@ -442,7 +483,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
@echo "TEST $<"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on" 2>&1; \
+ $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \
if [ $$? = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -484,4 +525,3 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
echo " $<...Error!"; \
fi; \
} > "$@"
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 02:22:56 +0000