Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGS

2 files changed, 62 insertions, 1 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index de669218c..16a56f440 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -40,6 +40,7 @@ coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
 coqtopcompile := $(coqtop) -compile
 coqdep := $(BIN)coqdep -coqlib $(LIB)
 
+VERBOSE?=
 SHOW := $(if $(VERBOSE),@true,@echo)
 HIDE := $(if $(VERBOSE),,@)
 REDIR := $(if $(VERBOSE),,> /dev/null 2>&1)
@@ -174,10 +175,20 @@ summary.log:
 
 # if not on travis we can get the log files (they're just there for a
 # local build, and downloadable on GitLab)
+PRINT_LOGS?=
+TRAVIS?= # special because we want to print travis_fold directives
+ifdef APPVEYOR
+PRINT_LOGS:=APPVEYOR
+else
+ifdef CIRCLECI
+PRINT_LOGS:=CIRCLECI
+endif #CIRCLECI
+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 "${APPVEYOR}" ")" -o "(" -n "${CIRCLECI}" ")" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; 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
 
 #######################################################################
diff --git a/test-suite/README.md b/test-suite/README.md
index 1ec5d667e..1d1195646 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -12,6 +12,56 @@ In these cases, a summary is not printed, but can be generated by `make summary`
 
 `make -B` can be used to rerun tests ( -B meaning always remake).
 
+From the `test-suite` directory, `make report` (included in `make
+all`) prints a summary of which tests failed using the produced log
+files (this still works when only some tests are built as described
+above). Setting the `PRINT_LOGS` variable will make it print the logs
+of the failing tests.
+
+For instance, running the following in the `test-suite` directory:
+
+```bash
+$ echo Fail. > success/fail.v # make some failing test
+
+$ make
+TEST      prerequisite/make_local.v
+...
+TEST      success/fail.v
+...
+BUILDING SUMMARY FILE
+FAILURES
+    success/fail.v...Error! (should be accepted)
+Makefile:189: recipe for target 'all failed
+make: *** [report] Error 1
+
+$ make report PRINT_LOGS=1
+BUILDING SUMMARY FILE
+logs/success/fail.v.log
+==========> TESTING success/fail.v <==========
+Welcome to Coq (version information)
+Skipping rcfile loading.
+File "/path/to/success/fail.v", line 1, characters 4-5:
+Error:
+Syntax error: [vernac:Vernac.vernac_control] expected after 'Fail' (in [vernac:Vernac.vernac_control]).
+
+0m0.000000s 0m0.000000s
+0m0.040000s 0m0.000000s
+==========> FAILURE <==========
+    success/fail.v...Error! (should be accepted)
+
+FAILURES
+    success/fail.v...Error! (should be accepted)
+Makefile:189: recipe for target 'report' failed
+make: *** [report] Error 1
+
+$ echo 'Comments "foo".' > success/fail.v
+
+$ make
+TEST      success/fail.v
+BUILDING SUMMARY FILE
+NO FAILURES
+```
+
 See [`test-suite/Makefile`](/test-suite/Makefile) for more information.
 
 ## Adding a test