proof-stat: address review comments

- read-only and no undo in report buffer
- add a batch mode test for proof-check-proofs

ci/simple-tests/Makefile

@@ -15,7 +15,7 @@ COQ_SUCCESS:=$(COQ_TESTS:.el=.success)
 QRHL_SUCCESS:=$(QRHL_TESTS:.el=.success)
 
 .PHONY: coq-all
-coq-all: $(COQ_SUCCESS)
+coq-all: $(COQ_SUCCESS) coq-proof-stat-batch-test
 
 .PHONY: qrhl-all
 qrhl-all: $(QRHL_SUCCESS)
@@ -25,6 +25,20 @@ qrhl-all: $(QRHL_SUCCESS)
 		-f ert-run-tests-batch-and-exit \
 	&& touch $@
 
+# The following tests the batch mode functionality of
+# proof-check-proofs. It generates human readable and TAP output for
+# proof_stat.v and compares it with the expected output in file
+# proof_stat.exp-out.
+coq-proof-stat-batch-test:
+	rm -rf proof_stat.gen-out
+	emacs -batch -l ../../generic/proof-site.el proof_stat.v \
+	      --eval '(proof-check-proofs nil "proof_stat.gen-out")'
+	emacs -batch -l ../../generic/proof-site.el proof_stat.v \
+	      --eval '(proof-check-proofs t "proof_stat.gen-out")'
+	cmp proof_stat.gen-out proof_stat.exp-out && \
+		touch coq-proof-stat-batch-test
+
 .PHONY: clean
 clean:
 	rm -f *.vo *.glob *.vio *.vos *.vok .*.aux *.success
+	rm -f coq-proof-stat-batch-test proof_stat.gen-out

ci/simple-tests/README.md

@@ -20,6 +20,10 @@ coq-test-three-window
   are too small for three windows.
 coq-test-proof-stat
 : test proof-check-proofs
+coq-proof-stat-batch-test
+: Batch mode test for proof-check-proofs. There is no Emacs lisp file
+  for this test. It is programmed out in the Makefile goal
+  coq-proof-stat-batch-test.
 
 # Overview of existing tests for qRHL
 

ci/simple-tests/proof_stat.exp-out

@@ -0,0 +1,16 @@
+Proof check results for proof_stat.v
+
+3 opaque proofs recognized: 1 successful 2 FAILING
+
+  FAIL a1_equal_4
+  OK   b_equal_6
+  FAIL b2_equal_6
+
+
+TAP version 13
+1..3
+not ok 1 - a1_equal_4
+ok 2 - b_equal_6
+not ok 3 - b2_equal_6
+
+

generic/pg-user.el

@@ -615,6 +615,7 @@ the results to the file denoted by BATCH."
          (frmt "  %-4s %s")
          (frmt-face (propertize frmt 'face 'error))
          (count 1)
+         (inhibit-read-only t)          ; for the report buffer, below
          coq-proj-dir src-file)
 
     ;; determine a relative file name for current buffer
@@ -627,6 +628,8 @@ the results to the file denoted by BATCH."
 
     ;; generate header
     (with-current-buffer (get-buffer-create proof-check-report-buffer)
+      (read-only-mode)
+      (buffer-disable-undo)
       (erase-buffer)
       (if tap
           (insert (format "TAP version 13\n1..%d\n" (length proof-results)))