6 files changed, 107 insertions, 6 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
new file mode 100644
index 000000000..1d1195646
--- /dev/null
+++ b/test-suite/README.md
@@ -0,0 +1,75 @@
+# Coq Test Suite
+
+The test suite can be run from the Coq root directory by `make test-suite`.
+This does a clean step first, so if you've already run it, then change something,
+you'll have to do a lot of work again.
+
+If you run `make` from the `test-suite` directory, there is no clean step.
+You can also run `make aaa/bbb/ccc.v.log` to build the log for one test,
+or `make ddd` where `ddd` is on of the sub-directories of `test-suite`
+to just build the logs for that directory.
+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
+
+Regression tests for closed bugs should be added to `test-suite/bugs/closed`, as `1234.v` where `1234` is the bug number.
+Files in this directory are tested for successful compilation.
+When you fix a bug, you should usually add a regression test here as well.
+
+The error "(bug seems to be opened, please check)" when running `make test-suite` means that a test in `bugs/closed` failed to compile.
+
+There are also output tests in `test-suite/output` which consist of a `.v` file and a `.out` file with the expected output.
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 898af5590..2439d3f37 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -31,16 +31,16 @@ coq_makefile -f _CoqProject -o Makefile
 make cleanall
 make make-pretty-timed-after TGTS="all" -j1 || exit $?
 rm -f time-of-build-before.log
-make print-pretty-timed-diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log
+make print-pretty-timed-diff TIMING_SORT_BY=diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log
 cp ../before/time-of-build-before.log ./
-make print-pretty-timed-diff || exit $?
+make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $?
 
 INFINITY="∞"
 INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase
 
 for ext in "" .desired; do
     for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
-	cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/  */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed
+        cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/  */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed
     done
 done
 for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
@@ -74,7 +74,7 @@ echo
 
 for ext in "" .desired; do
     for file in A.v.timing.diff; do
-	cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/  */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed
+        cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/  */ /g' | sed s'/ *$//g' | sed s'/+/-/g' | sort > ${file}${ext}.processed
     done
 done
 for file in A.v.timing.diff; do
diff --git a/test-suite/output/optimize_heap.out b/test-suite/output/optimize_heap.out
new file mode 100644
index 000000000..94a0b1911
--- /dev/null
+++ b/test-suite/output/optimize_heap.out
@@ -0,0 +1,8 @@
+1 subgoal
+  
+  ============================
+  True
+1 subgoal
+  
+  ============================
+  True
diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v
new file mode 100644
index 000000000..e566bd7ba
--- /dev/null
+++ b/test-suite/output/optimize_heap.v
@@ -0,0 +1,7 @@
+(* optimize_heap should not affect the proof state *)
+
+Goal True.
+  idtac.
+  Show.
+  optimize_heap.
+  Show.
diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v
index b736b734f..aa8da5336 100644
--- a/test-suite/success/abstract_poly.v
+++ b/test-suite/success/abstract_poly.v
@@ -17,4 +17,4 @@ intros m n P e p.
 abstract (rewrite e in p; exact p).
 Defined.
 
-Check bar_subproof@{Set Set Set}.
+Check bar_subproof@{Set Set}.