poor PG man's workaround for coq/coq#11479

CHANGES

@@ -14,6 +14,9 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
     Proof-tree visualization is currently only supported for Coq. The
     prooftree support has been substantially rewritten, making use of
     the much better support since Coq version 8.11.
+*** New command `proof-check-proofs' to generates the proof status
+    of all opaque proofs. Currently only available for Coq, see Coq
+    changes below for more details.
 
 ** Coq changes
 *** support Coq 8.19
@@ -23,15 +26,21 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
      modules as coqdep error.
 *** Renew support for proof-tree visualization, see description in
     generic changes above.
-
-
-**** New options coq-compile-extra-coqc-arguments and
-     coq-compile-extra-coqdep-arguments to configure additional
-     command line arguments to calls of, respetively, coqc and coqdep
-     during auto compilation.
-
-**** Fix issues #687 and #688 where the omit-proofs feature causes
-     errors on correct code.
+*** New command `proof-check-proofs' to generates the proof status
+    of all opaque proofs. This command is useful for a development
+    process where invalid proofs are permitted and vos compilation and
+    the omit proofs feature are used to work at the most interesting
+    or challenging point instead of on the first invalid proof. The
+    command generates a list of all opaque proofs in the current
+    buffer together with the information whether the proof script is
+    currently valid or invalid. The command can also be run in batch
+    mode, for instance in a continuous integration environment.
+*** New options coq-compile-extra-coqc-arguments and
+    coq-compile-extra-coqdep-arguments to configure additional
+    command line arguments to calls of, respetively, coqc and coqdep
+    during auto compilation.
+*** Fix issues #687 and #688 where the omit-proofs feature causes
+    errors on correct code.
 
 
 * Changes of Proof General 4.5 from Proof General 4.4

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

@@ -15,9 +15,15 @@ coq-test-prelude-correct
 coq-test-goals-present
 : test that Proof General shows goals correctly in various
   situations
-coq-test-three-window.el
+coq-test-three-window
 : Test three-pane mode for different frame sizes, including ones that
   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-omit-proofs.el

@@ -95,7 +95,8 @@ In particular, test that with proof-omit-proofs-option configured:
 - in this case the proof has normal locked color
 - without prefix arg, the proof is omitted
 - the proof has omitted color then
-- stuff before the proof still has normal color "
+- stuff before the proof still has normal color
+- trailing incomplete proofs are not omitted"
   (message "omit-proofs-omit-and-not-omit: Check several omit proofs features")
   (setq proof-omit-proofs-option t
         proof-three-window-enable nil)
@@ -187,6 +188,23 @@ In particular, test that with proof-omit-proofs-option configured:
   (should (search-backward "automatic test marker 1" nil t))
   (should (eq (first-overlay-face) 'proof-locked-face))
   (should (search-forward "automatic test marker 2" nil t))
+  (should (eq (first-overlay-face) 'proof-locked-face))
+
+  ;; Check 6: check that a partial proof at the end is not omitted
+  (message "6: check that a partial proof at the end is not omitted")
+  (goto-char (point-min))
+  (proof-goto-point)
+  (wait-for-coq)
+  (should (search-forward "automatic test marker 3" nil t))
+  (forward-line 2)
+  (proof-goto-point)
+  (wait-for-coq)
+  ;; there are 2 goals
+  (with-current-buffer "*goals*"
+    (goto-char (point-min))
+    (should (looking-at "2 \\(?:sub\\)?goals")))
+  ;; the line before should be locked
+  (forward-line -1)
   (should (eq (first-overlay-face) 'proof-locked-face)))
 
 (ert-deftest omit-proofs-never-omit-hints ()

ci/simple-tests/coq-test-proof-stat.el

@@ -0,0 +1,84 @@
+;; This file is part of Proof General.
+;; 
+;; © Copyright 2024  Hendrik Tews
+;; 
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hendrik@askra.de>
+;; 
+;; SPDX-License-Identifier: GPL-3.0-or-later
+
+;;; Commentary:
+;;
+;; Test proof-check-proofs.
+
+(defun reset-coq ()
+  "Reset Coq and Proof General.
+Do `proof-shell-exit' to kill Coq and reset the locked region and
+a lot of other internal state of Proof General. Used at the
+beginning of the test when several tests work on the same Coq
+source file."
+  (when (and (boundp 'proof-shell-buffer)
+             (buffer-live-p proof-shell-buffer))
+    (proof-shell-exit t)
+    (message "Coq and Proof General reseted")))
+
+
+(ert-deftest proof-check-correct-stat ()
+  "Test `proof-check-proofs' on a file that is correct in non-opaque parts.
+Test that the report buffer contains the expected output."
+  (setq proof-three-window-enable nil)
+  (reset-coq)
+  (find-file "proof_stat.v")
+
+  ;; run check on file where all errors are in opaque parts
+  (proof-check-proofs nil)
+
+  ;; the result buffer should exist
+  (should (buffer-live-p (get-buffer "*proof-check-report*")))
+  (with-current-buffer "*proof-check-report*"
+    ;; the summary should be correct
+    (goto-char (point-min))
+    (should
+     (search-forward "3 opaque proofs recognized: 1 successful 2 FAILING"
+                     nil t))
+    ;; results for all 3 test lemmas should be correct
+    (mapc
+     (lambda (s) (should (search-forward s nil t)))
+     '("FAIL a1_equal_4"
+       "OK   b_equal_6"
+       "FAIL b2_equal_6"))))
+
+
+(ert-deftest proof-check-error-on-error ()
+  "Test `proof-check-proofs' with errors in non-opaque parts.
+Check that `proof-check-proofs' signals an error with the expected message."
+  (setq proof-three-window-enable nil)
+  (reset-coq)
+  (let (buffer)
+    (unwind-protect
+        (progn
+          (find-file "proof_stat.v")
+          (setq buffer (current-buffer))
+
+          ;; insert an error in non-opaque part
+          (goto-char (point-min))
+          (should (search-forward "automatic test marker 1" nil t))
+          (end-of-line)
+          (insert " X ")
+
+          ;; proof-check-proofs should abort now with an error
+          (condition-case err-desc
+              (progn
+                (proof-check-proofs nil)
+                ;; Still here? Make test fail!
+                (should nil))
+            (error
+             (should
+              (equal (error-message-string err-desc)
+                     "Error encountered outside opaque proofs after line 10")))))
+
+      ;; clean-up modified file in any case
+      (when buffer
+        (with-current-buffer buffer
+          (set-buffer-modified-p nil))
+        (kill-buffer buffer)))))

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
+
+

ci/simple-tests/proof_stat.v

@@ -0,0 +1,24 @@
+
+Definition a : nat := 4.
+
+Lemma a1_equal_4 : a = 2 * 2.
+Proof using.
+  simpl.
+  zzzz.                         (* this proof should fail *)
+  trivial.
+Qed.
+
+Definition b : nat :=
+(* automatic test marker 1 *)
+ 6.
+
+Lemma b_equal_6 : b = 2 * 3.
+Proof using.
+  simpl.
+  trivial.
+Qed.
+
+Lemma b2_equal_6 : b = 2 * 3.
+Proof using.                    (* this proof should fail *)
+Qed.
+

coq/coq.el

@@ -1963,6 +1963,12 @@ at `proof-assistant-settings-cmds' evaluation time.")
    proof-script-cmd-prevents-proof-omission #'coq-cmd-prevents-proof-omission
    proof-script-cmd-force-next-proof-kept coq-cmd-force-next-proof-kept)
 
+  ;; proof-check-proofs config
+  (setq
+   proof-get-proof-info-fn #'coq-get-proof-info-fn
+   proof-retract-command-fn #'coq-retract-command)
+
+
   (setq proof-cannot-reopen-processed-files nil)
 
   (proof-config-done)
@@ -2274,6 +2280,25 @@ Function for `proof-tree-display-stop-command'."
     (coq-proof-tree-evar-command "Unset")))
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; proof-check-proofs support
+;;
+
+(defun coq-get-proof-info-fn ()
+  "Coq instance of `proof-get-proof-info-fn' for `proof-check-proofs'.
+Return state number followed by the name of the current proof of
+nil in a list."
+  (list
+   coq-last-but-one-statenum
+   (car coq-last-but-one-proofstack)))
+
+(defun coq-retract-command (state)
+  "Coq instance of `proof-retract-command-fn' for `proof-check-proofs'.
+Return command that undos to state."
+  (format "BackTo %d." state))
+
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Pre-processing of input string

doc/PG-adapting.texi

@@ -647,6 +647,7 @@ the behaviour of script management.
 * Configuring undo behaviour::
 * Nested proofs::
 * Omitting proofs for speed::
+* Proof status statistic::
 * Safe (state-preserving) commands::
 * Activate scripting hook::
 * Automatic multiple files::
@@ -1275,6 +1276,58 @@ does only work if the command and the following proof are
 asserted together.
 @end defvar
 
+
+@node Proof status statistic
+@section Proof status statistic
+
+The command @code{proof-check-proofs} builds on the omit-proofs
+feature. Using its machinery, it splits the current buffer into opaque
+proofs and all other material. The other material is asserted in the
+usual way and @code{proof-check-proofs} aborts if it detects an error
+in there. For opaque proofs the command first tries to assert them in
+the usual way too. If this succeeds the proof is considered valid.
+Otherwise the proof is replaced with
+@code{proof-script-proof-admit-command} and the proof is considered
+invalid. To associate theorem names with opaque proofs, the function
+@code{proof-get-proof-info-fn} is called, which is identical to
+@code{proof-tree-get-proof-info}, @xref{Proof Tree Elisp
+configuration}.
+
+To enable proof status statistics, the omit-proofs feature must be
+configured, @xref{Omitting proofs for speed}. Additionally, the
+following settings must be configured.
+
+@c TEXI DOCSTRING MAGIC: proof-get-proof-info-fn
+@defvar proof-get-proof-info-fn 
+Return proof name and state number for @samp{@code{proof-check-proofs}}.@*
+Proof assistant specific function for @samp{@code{proof-check-proofs}}. This
+function takes no arguments, it is called after completely
+processing the proof script up to a certain point (including all
+callbacks in spans). It must return a list, which contains, in
+the following order:
+
+* the current state number (as positive integer)
+* the name of the current proof (as string) or nil
+
+The proof assistant should return to the same state when the
+state number is supplied to @samp{@code{proof-retract-command-fn}}.
+Processing the command returned by @samp{@code{proof-retract-command-fn}}
+without processing any other command after calling this function
+should be a no-op.
+
+(This function has the same signature and specification as
+@samp{@code{proof-tree-get-proof-info}}.)
+@end defvar
+
+@c TEXI DOCSTRING MAGIC: proof-retract-command-fn
+@defvar proof-retract-command-fn 
+Function for retract command to a certain state.@*
+This function takes a state as argument as returned by
+@samp{@code{proof-get-proof-info-fn}}. It should return a command that brings
+the proof assistant back to the same state.
+@end defvar
+
+
 @node Safe (state-preserving) commands
 @section Safe (state-preserving) commands