diff options
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 148 |
1 files changed, 121 insertions, 27 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 85076418..598d6db2 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -8,9 +8,6 @@ ## # (see LICENSE file for the text of the license) ## ########################################################################## -# This is a standalone Makefile to run the test-suite. It can be used -# outside of the Coq source tree (if BIN is overridden). - # There is one %.v.log target per %.v test file. The target will be # filled with the output, timings and status of the test. There is # also one target per directory containing %.v files, that runs all @@ -23,6 +20,14 @@ # The "run" target runs all tests that have not been run yet. To force # all tests to be run, use the "clean" target. + +########################################################################### +# Includes +########################################################################### + +-include ../config/Makefile +include ../Makefile.common + ####################################################################### # Variables ####################################################################### @@ -79,6 +84,8 @@ log_anomaly = "==========> FAILURE <==========" log_failure = "==========> FAILURE <==========" log_intro = "==========> TESTING $(1) <==========" +FAIL = >&2 echo 'FAILED $@' + ####################################################################### # Testing subsystems ####################################################################### @@ -92,10 +99,10 @@ INTERACTIVE := interactive VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ - coqdoc + coqdoc ssr # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools unit-tests PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log \ @@ -116,25 +123,27 @@ run: $(SUBSYSTEMS) bugs: $(BUGS) clean: - rm -f trace .lia.cache - $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>" + rm -f trace .lia.cache output/MExtraction.out + $(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>' $(HIDE)find . \( \ - -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \ - \) -print0 | xargs -0 rm -f - + -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \ + \) -print0 | xargs -0 rm -f + $(SHOW) 'RM <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>' + $(HIDE)find unit-tests \( \ + -name '*.cmx' -o -name '*.cmi' -o -name '*.o' -o -name '*.test' \ + \) -print0 | xargs -0 rm -f distclean: clean - $(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f + $(SHOW) 'RM <**/*.aux>' + $(HIDE)find . -name '*.aux' -print0 | xargs -0 rm -f ####################################################################### # Per-subsystem targets ####################################################################### -define mkstamp -$(1): $(1).stamp ; @true -$(1).stamp: $(patsubst %.v,%.v.log,$(wildcard $(1)/*.v)) ; \ - $(HIDE)touch $$@ +define vdeps +$(1): $(patsubst %.v,%.v.log,$(wildcard $(1)/*.v)) endef -$(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S)))) +$(foreach S,$(VSUBSYSTEMS),$(eval $(call vdeps,$(S)))) ####################################################################### # Summary @@ -158,18 +167,21 @@ summary: $(call summary_dir, "Complexity tests", complexity); \ $(call summary_dir, "Module tests", modules); \ $(call summary_dir, "STM tests", stm); \ + $(call summary_dir, "SSR tests", ssr); \ $(call summary_dir, "IDE tests", ide); \ $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ $(call summary_dir, "Coqwc tests", coqwc); \ $(call summary_dir, "Coq makefile", coq-makefile); \ $(call summary_dir, "Coqdoc tests", coqdoc); \ + $(call summary_dir, "tools/ tests", tools); \ + $(call summary_dir, "Unit tests", unit-tests); \ 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`; \ - pourcentage=`expr 100 \* $$nb_success / $$nb_tests`; \ + percentage=`expr 100 \* $$nb_success / $$nb_tests`; \ echo; \ - echo "$$nb_success tests passed over $$nb_tests, i.e. $$pourcentage %"; \ + echo "$$nb_success tests passed over $$nb_tests, i.e. $$percentage %"; \ } summary.log: @@ -185,10 +197,7 @@ PRINT_LOGS:=APPVEYOR endif #APPVEYOR report: summary.log - $(HIDE)bash save-logs.sh - $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi - $(HIDE)if [ -n "${PRINT_LOGS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi - $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi + $(HIDE)bash report.sh ####################################################################### # Regression (and progression) tests @@ -218,6 +227,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v else \ echo $(log_failure); \ echo " $<...Error! (bug seems to be closed, please check)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -233,10 +243,49 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v else \ echo $(log_failure); \ echo " $<...Error! (bug seems to be opened, please check)"; \ + $(FAIL); \ fi; \ } > "$@" ####################################################################### +# Unit tests +####################################################################### + +OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) +SYSMOD:=-package num,str,unix,dynlink,threads + +COQSRCDIRS:=$(addprefix -I $(LIB)/,$(CORESRCDIRS)) +COQCMXS:=$(addprefix $(LIB)/,$(LINKCMX)) + +# ML files from unit-test framework, not containing tests +UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml) +UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml) +UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES)) +UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES)) + +UNIT_CMXS=utest.cmx + +unit-tests/src/utest.cmx: unit-tests/src/utest.ml unit-tests/src/utest.cmi + $(SHOW) 'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package oUnit $< +unit-tests/src/utest.cmi: unit-tests/src/utest.mli + $(SHOW) 'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) -package oUnit $< + +$(UNIT_LOGFILES): unit-tests/src/utest.cmx + +unit-tests: $(UNIT_LOGFILES) + +# Build executable, run it to generate log file +unit-tests/%.ml.log: unit-tests/%.ml + $(SHOW) 'TEST $<' + $(HIDE)$(OCAMLOPT) -linkall -linkpkg -cclib -lcoqrun \ + $(SYSMOD) -package camlp5.gramlib,oUnit \ + -I unit-tests/src $(COQSRCDIRS) $(COQCMXS) \ + $(UNIT_CMXS) $< -o $<.test; + $(HIDE)./$<.test + +####################################################################### # Other generic tests ####################################################################### @@ -248,13 +297,15 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be prepared" ; \ + $(FAIL); \ else \ echo $(log_success); \ echo " $<...correctly prepared" ; \ fi; \ } > "$@" -$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) +ssr: $(wildcard ssr/*.v:%.v=%.v.log) +$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \ @@ -266,6 +317,7 @@ $(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %. else \ echo $(log_failure); \ echo " $<...Error! (should be accepted)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -282,6 +334,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v else \ echo $(log_failure); \ echo " $<...Error! (should be accepted)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -296,6 +349,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error! (should be rejected)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -303,25 +357,33 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ + output=$*.out.real; \ $(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 --strip-trailing-cr $*.out $$tmpoutput 2>&1; R=$$?; times; \ + > $$output; \ + diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ + rm $$output; \ else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ - rm $$tmpoutput; \ } > "$@" +.PHONY: approve-output +approve-output: output + $(HIDE)for f in output/*.out.real; do \ + mv "$$f" "$${f%.real}"; \ + echo "Updated $${f%.real}!"; \ + done + # the expected output for the MExtraction test is # /plugins/micromega/micromega.ml except with additional newline output/MExtraction.out: ../plugins/micromega/micromega.ml @@ -360,6 +422,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ rm $$tmpoutput; \ rm $$tmpexpected; \ @@ -376,6 +439,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error! (should be accepted)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -408,6 +472,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error! (should run faster)"; \ + $(FAIL); \ fi; \ fi; \ } > "$@" @@ -425,6 +490,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG else \ echo $(log_failure); \ echo " $<...Good news! (wish seems to be granted, please check)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -448,6 +514,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ + export BIN="$(BIN)"; \ export coqc="$(coqc)"; \ export coqtop="$(coqtop)"; \ export coqdep="$(coqdep)"; \ @@ -459,6 +526,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -477,6 +545,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -496,6 +565,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -514,6 +584,7 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -533,6 +604,7 @@ coqwc/%.v.log : coqwc/%.v else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ rm $$tmpoutput; \ } > "$@" @@ -553,6 +625,7 @@ coq-makefile/%.log : coq-makefile/%/run.sh else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ ) > "$@" @@ -577,5 +650,26 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ } > "$@" + +# tools/ + +tools: $(patsubst %/run.sh,%.log,$(wildcard tools/*/run.sh)) + +tools/%.log : tools/%/run.sh + @echo "TEST tools/$*" + $(HIDE)(\ + export COQBIN=$(BIN);\ + cd tools/$* && \ + bash run.sh 2>&1; \ + if [ $$? = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error!"; \ + $(FAIL); \ + fi; \ + ) > "$@" |