diff options
| author | Enrico Tassi | 2019-06-17 13:37:51 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-17 13:37:51 +0200 |
| commit | 535d897ed25f37d454b119a3873a2ff232d3f46e (patch) | |
| tree | f45dbc062d15ef3637629ff7e8c17fdb73dc0289 | |
| parent | 658db3a8b75a338df6b07d0f0e5034bb81bcfd16 (diff) | |
| parent | 135b56936e36eff23eb580c097045d2a932a19f8 (diff) | |
Merge PR #10332: test suite: don't try to coqchk failed tests
Reviewed-by: maximedenes
| -rw-r--r-- | test-suite/Makefile | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 552d007f85..ed4777608a 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -335,16 +335,16 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithm $(FAIL); \ fi; \ } > "$@" - @echo "CHECK $<" - $(HIDE){ \ - opts="$(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-I $(shell dirname $<) -norec $(shell basename $< .v))"; \ + @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi + $(HIDE)if ! grep -q -F "Error!" $@; then { \ + opts="$(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-I $(shell dirname $<) -norec $(shell basename $< .v))"; \ $(coqchk) -silent $(call get_set_impredicativity,$<) $$opts 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ $(FAIL); \ fi; \ - } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi stm: $(wildcard stm/*.v:%.v=%.v.log) $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v @@ -362,15 +362,15 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v $(FAIL); \ fi; \ } > "$@" - @echo "CHECK $<" - $(HIDE){ \ + @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi + $(HIDE)if ! grep -q -F "Error!" $@; then { \ $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ $(FAIL); \ fi; \ - } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" @@ -386,15 +386,15 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(FAIL); \ fi; \ } > "$@" - @echo "CHECK $<" - $(HIDE){ \ + @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi + $(HIDE)if ! grep -q -F "Error!" $@; then { \ $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ $(FAIL); \ fi; \ - } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" |