From 135b56936e36eff23eb580c097045d2a932a19f8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 7 Jun 2019 11:15:18 +0200
Subject: test suite: don't try to coqchk failed tests

---
 test-suite/Makefile | 20 ++++++++++----------
 1 file 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,"$<")"
-- 
cgit v1.2.3