diff options
| author | Pierre Roux | 2020-04-11 19:35:20 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-05-22 12:15:22 +0200 |
| commit | 4bab69688d91648ec1725f6294b7430622e6accf (patch) | |
| tree | 9847b86e3c7af205d58babe6fbbb5e3d398dc79c /test-suite/Makefile | |
| parent | f44ec99f9ae9b8aa8d77c39795dd4de2a5724218 (diff) | |
[coqchk] Add test
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 40 |
1 files changed, 39 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 5dd4f42af3..d4ad438d61 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -115,7 +115,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ coqdoc ssr primitive/uint63 primitive/float ltac2 # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk output-coqchk coqwc coq-makefile tools $(UNIT_TESTS) .csdp.cache: .csdp.cache.test-suite cp $< $@ @@ -192,6 +192,7 @@ summary: $(call summary_dir, "IDE tests", ide); \ $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ + $(call summary_dir, "Output tests with coqchk", output-coqchk); \ $(call summary_dir, "Coqwc tests", coqwc); \ $(call summary_dir, "Coq makefile", coq-makefile); \ $(call summary_dir, "Coqdoc tests", coqdoc); \ @@ -462,6 +463,43 @@ $(addsuffix .log,$(wildcard output-coqtop/*.v)): %.v.log: %.v %.out $(PREREQUISI fi; \ } > "$@" +output-coqchk: $(addsuffix .log,$(wildcard output-coqchk/*.v)) +$(addsuffix .log,$(wildcard output-coqchk/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) + @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" + $(HIDE){ \ + opts="$(if $(findstring modules/,$<),-R modules Mods)"; \ + echo $(call log_intro,$<); \ + $(coqc) "$<" $(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)"; \ + $(FAIL); \ + fi; \ + } > "$@" + @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi + $(HIDE)if ! grep -q -F "Error!" $@; then { \ + echo $(call log_intro,$<); \ + output=$*.out.real; \ + export LC_CTYPE=C; \ + export LANG=C; \ + $(coqchk) -o -silent $(call get_set_impredicativity,$<) $(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-Q $(shell dirname $<) "" -norec $(shell basename $< .v)) 2>&1 \ + | sed 's/File "[^"]*"/File "stdin"/' \ + > $$output; \ + diff -a -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; \ + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi + .PHONY: approve-output approve-output: output output-coqtop $(HIDE)for f in output/*.out.real; do \ |