proof-stat: address review comments

- read-only and no undo in report buffer
- add a batch mode test for proof-check-proofs; require seq library to
  make this work in Emacs 26

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/coq-test-proof-stat.el

@@ -11,11 +11,6 @@
 ;;
 ;; Test proof-check-proofs.
 
-;; For seq-group-by inside `proof-check-report'. This is
-;; apparently not automatically loaded in Emacs 26.3. Though in a real
-;; PG session it is apparently present.
-(require 'seq)
-
 (defun reset-coq ()
   "Reset Coq and Proof General.
 Do `proof-shell-exit' to kill Coq and reset the locked region and

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

@@ -26,6 +26,13 @@
 
 (require 'proof-script)	        ; we build on proof-script
 
+;; For seq-group-by inside `proof-check-report'. This is apparently
+;; not automatically loaded in Emacs 26.3. In a real PG session it is
+;; apparently present, but not if `proof-check-proof' is invoked from
+;; the shell as described in the user manual.
+;; XXX Delete this when support for Emacs 26 is dropped (hopefully in Q4/2025).
+(require 'seq)
+
 (eval-when-compile (require 'cl-lib))   ;cl-decf
 (defvar which-func-modes)               ; Defined by which-func.
 
@@ -615,6 +622,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 +635,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)))