From 6cace58d0d632c4eafa18959319a484fb5c07238 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 15 Apr 2024 13:36:30 +0200 Subject: [PATCH] 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(-) create mode 100644 ci/simple-tests/proof_stat.exp-out diff --git a/ci/simple-tests/Makefile b/ci/simple-tests/Makefile index 786ce6067..70b15a1fd 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 140e72987..553448f9b 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 2db6a001c..821077da8 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 000000000..9f4f0aa5d --- /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 e8736fb1f..05b3c46f8 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)))