Add output-coqtop test directory that runs output tests with coqtop

1 files changed, 27 insertions, 2 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index a48a71c159..098ad58b43 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); \
@@ -420,8 +421,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}!"; \