branch: elpa/proof-general
commit 6cace58d0d632c4eafa18959319a484fb5c07238
Author: Hendrik Tews <hend...@askra.de>
Commit: hendriktews <hend...@askra.de>
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 | 16 +++++++++++++++-
ci/simple-tests/README.md | 4 ++++
ci/simple-tests/coq-test-proof-stat.el | 5 -----
ci/simple-tests/proof_stat.exp-out | 16 ++++++++++++++++
generic/pg-user.el | 10 ++++++++++
5 files changed, 45 insertions(+), 6 deletions(-)
diff --git a/ci/simple-tests/Makefile b/ci/simple-tests/Makefile
index 786ce60676..70b15a1fd9 100644
--- a/ci/simple-tests/Makefile
+++ b/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
diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md
index 140e729875..553448f9b6 100644
--- a/ci/simple-tests/README.md
+++ b/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
diff --git a/ci/simple-tests/coq-test-proof-stat.el
b/ci/simple-tests/coq-test-proof-stat.el
index 2db6a001c2..821077da83 100644
--- a/ci/simple-tests/coq-test-proof-stat.el
+++ b/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
diff --git a/ci/simple-tests/proof_stat.exp-out
b/ci/simple-tests/proof_stat.exp-out
new file mode 100644
index 0000000000..9f4f0aa5d2
--- /dev/null
+++ b/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
+
+
diff --git a/generic/pg-user.el b/generic/pg-user.el
index e8736fb1f6..05b3c46f88 100644
--- a/generic/pg-user.el
+++ b/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)))
