Merge PR #10412: Add output-coqtop test directory that runs output tests with coqtop

Reviewed-by: gares
Ack-by: jfehrle

2 files changed, 30 insertions, 3 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index ec61f60791..c0bdb29fab 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -97,7 +97,7 @@ COMPLEXITY := $(if $(bogomips),complexity)
 BUGS := bugs/opened bugs/closed
 INTERACTIVE := interactive
 UNIT_TESTS := unit-tests
-VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
+VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \
   output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
   coqdoc ssr arithmetic ltac2
 
@@ -164,6 +164,7 @@ summary:
 	  $(call summary_dir, "Failure tests", failure); \
 	  $(call summary_dir, "Bugs tests", bugs); \
 	  $(call summary_dir, "Output tests", output); \
+	  $(call summary_dir, "Output tests with coqtop", output-coqtop); \
 	  $(call summary_dir, "Output (modulo time changes) tests", output-modulo-time); \
 	  $(call summary_dir, "Interactive tests", interactive); \
 	  $(call summary_dir, "Micromega tests", micromega); \
@@ -425,8 +426,32 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	  fi; \
 	} > "$@"
 
+$(addsuffix .log,$(wildcard output-coqtop/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
+	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  output=$*.out.real; \
+	  $(coqtop) < "$<" $(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"/' \
+	    > $$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; \
+	} > "$@"
+
 .PHONY: approve-output
-approve-output: output
+approve-output: output output-coqtop
 	$(HIDE)for f in output/*.out.real; do \
 	  mv "$$f" "$${f%.real}"; \
 	  echo "Updated $${f%.real}!"; \
diff --git a/test-suite/README.md b/test-suite/README.md
index e81da0830f..a2d5905710 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -76,7 +76,9 @@ The error "(bug seems to be opened, please check)" when running
 compile.
 
 There are also output tests in [`output`](output) which consist of a `.v` file
-and a `.out` file with the expected output.
+and a `.out` file with the expected output.  Output tests in this directory are
+run with coqc in -test-mode.  Output tests in [`output-coqtop`](output-coqtop)
+work the same way, but are run with coqtop.
 
 There are unit tests of OCaml code in [`unit-tests`](unit-tests). These tests
 are contained in `.ml` files, and rely on the `OUnit` unit-test framework, as