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/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..8483f974f 100644 --- a/generic/pg-user.el +++ b/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)))