Merge PR #7322: Test suite Makefile: print message for failing tests as they come, misc improvements

1 files changed, 28 insertions, 9 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 8239600b1..9d84cd5c7 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -79,6 +79,8 @@ log_anomaly = "==========> FAILURE <=========="
 log_failure = "==========> FAILURE <=========="
 log_intro = "==========> TESTING $(1) <=========="
 
+FAIL = >&2 echo 'FAILED    $@'
+
 #######################################################################
 # Testing subsystems
 #######################################################################
@@ -115,25 +117,24 @@ 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        <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>"
 	$(HIDE)find . \( \
-	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \
+	  -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \
 	\) -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
@@ -221,6 +222,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; \
 	} > "$@"
 
@@ -236,6 +238,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (bug seems to be opened, please check)"; \
+	    $(FAIL); \
 	  fi; \
 	} > "$@"
 
@@ -251,6 +254,7 @@ $(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" ; \
@@ -269,6 +273,7 @@ $(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (should be accepted)"; \
+	    $(FAIL); \
 	  fi; \
 	} > "$@"
 
@@ -285,6 +290,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (should be accepted)"; \
+	    $(FAIL); \
 	  fi; \
 	} > "$@"
 
@@ -299,6 +305,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (should be rejected)"; \
+	    $(FAIL); \
 	  fi; \
 	} > "$@"
 
@@ -321,6 +328,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (unexpected output)"; \
+	    $(FAIL); \
 	  fi; \
 	  rm $$tmpoutput; \
 	} > "$@"
@@ -363,6 +371,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; \
@@ -379,6 +388,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (should be accepted)"; \
+	    $(FAIL); \
 	  fi; \
 	} > "$@"
 
@@ -411,6 +421,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	    else \
 	      echo $(log_failure); \
 	      echo "    $<...Error! (should run faster)"; \
+	      $(FAIL); \
 	    fi; \
 	  fi; \
 	} > "$@"
@@ -428,6 +439,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; \
 	} > "$@"
 
@@ -462,6 +474,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error!"; \
+	    $(FAIL); \
 	  fi; \
 	} > "$@"
 
@@ -480,6 +493,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error!"; \
+	    $(FAIL); \
 	  fi; \
 	} > "$@"
 
@@ -499,6 +513,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error!"; \
+	    $(FAIL); \
 	  fi; \
 	} > "$@"
 
@@ -517,6 +532,7 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error!"; \
+	    $(FAIL); \
 	  fi; \
 	} > "$@"
 
@@ -536,6 +552,7 @@ coqwc/%.v.log : coqwc/%.v
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (unexpected output)"; \
+	    $(FAIL); \
 	  fi; \
 	  rm $$tmpoutput; \
 	} > "$@"
@@ -556,6 +573,7 @@ coq-makefile/%.log : coq-makefile/%/run.sh
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error!"; \
+	    $(FAIL); \
 	  fi; \
 	) > "$@"
 
@@ -580,5 +598,6 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (unexpected output)"; \
+	    $(FAIL); \
 	  fi; \
 	} > "$@"