test suite: make target to regenerate failing output tests

2 files changed, 25 insertions, 4 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index f41fb5b1e..32e245e36 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -362,26 +362,33 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
+	  output=$*.out.real; \
 	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
 	    | grep -v "^<W>" \
 	    | sed 's/File "[^"]*"/File "stdin"/' \
-	    > $$tmpoutput; \
-	  diff -u --strip-trailing-cr $*.out $$tmpoutput 2>&1; R=$$?; times; \
+	    > $$output; \
+	  diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
+	    rm $$output; \
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (unexpected output)"; \
 	    $(FAIL); \
 	  fi; \
-	  rm $$tmpoutput; \
 	} > "$@"
 
+.PHONY: approve-output
+approve-output: output
+	$(HIDE)for f in output/*.out.real; do \
+	  mv "$$f" "$${f%.real}"; \
+	  echo "Updated $${f%.real}!"; \
+	done
+
 # the expected output for the MExtraction test is
 # /plugins/micromega/micromega.ml except with additional newline
 output/MExtraction.out: ../plugins/micromega/micromega.ml
diff --git a/test-suite/README.md b/test-suite/README.md
index 4572c98cf..ef2e574ec 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -76,3 +76,17 @@ There are also output tests in `test-suite/output` which consist of a `.v` file
 
 There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit`
 unit-test framework, as described at http://ounit.forge.ocamlcore.org/.  Use `make unit-tests' in the unit-tests directory to run them.
+
+## Fixing output tests
+
+When an output test `output/foo.v` fails, the output is stored in
+`output/foo.out.real`. Move that file to the reference file
+`output/foo.out` to update the test, approving the new output. Target
+`approve-output` will do this for all failing output tests
+automatically.
+
+Don't forget to check the updated `.out` files into git!
+
+Note that `output/MExtraction.out` is special: it is copied from
+`micromega/micromega.ml` in the plugin source directory. Automatic
+approval will incorrectly update the copy.