proof-stat: add feature to annotate failing proofs with FAIL

... see documentation of proof-check-annotate

CHANGES

@@ -14,9 +14,11 @@ 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
+*** New command `proof-check-report' to generates the proof status
     of all opaque proofs. Currently only available for Coq, see Coq
     changes below for more details.
+*** New command `proof-check-annotate' to annotate all failing proofs
+    with FAIL comments.
 
 ** Coq changes
 *** support Coq 8.19
@@ -26,7 +28,7 @@ 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 command `proof-check-proofs' to generates the proof status
+*** New command `proof-check-report 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
@@ -35,6 +37,9 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
     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 command `proof-check-annotate' to annotate all failing proofs
+    with FAIL comments. Useful in the development process as described
+    above to ensure all currently failing proofs are marked as such.
 *** 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

ci/simple-tests/Makefile

@@ -26,14 +26,14 @@ qrhl-all: $(QRHL_SUCCESS)
 	&& touch $@
 
 # The following tests the batch mode functionality of
-# proof-check-proofs. It generates human readable and TAP output for
+# proof-check-report. 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:
 	emacs -batch -l ../../generic/proof-site.el proof_stat.v \
-	      --eval '(proof-check-proofs nil "proof_stat.human.gen-out")'
+	      --eval '(proof-check-report nil "proof_stat.human.gen-out")'
 	emacs -batch -l ../../generic/proof-site.el proof_stat.v \
-	      --eval '(proof-check-proofs t "proof_stat.tap.gen-out")'
+	      --eval '(proof-check-report t "proof_stat.tap.gen-out")'
 	cmp proof_stat.human.gen-out proof_stat.human.exp-out && \
 	        cmp proof_stat.tap.gen-out proof_stat.tap.exp-out && \
 		touch coq-proof-stat-batch-test

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

@@ -9,7 +9,7 @@
 
 ;;; Commentary:
 ;;
-;; Test proof-check-proofs.
+;; Tests for proof-check-report and proof-check-annotate.
 
 (defun reset-coq ()
   "Reset Coq and Proof General.
@@ -24,14 +24,14 @@ source file."
 
 
 (ert-deftest proof-check-correct-stat ()
-  "Test `proof-check-proofs' on a file that is correct in non-opaque parts.
+  "Test `proof-check-report' 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)
+  (proof-check-report nil)
 
   ;; the result buffer should exist
   (should (buffer-live-p (get-buffer "*proof-check-report*")))
@@ -50,8 +50,8 @@ Test that the report buffer contains the expected output."
 
 
 (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."
+  "Test `proof-check-report' with errors in non-opaque parts.
+Check that `proof-check-report' signals an error with the expected message."
   (setq proof-three-window-enable nil)
   (reset-coq)
   (let (buffer)
@@ -66,10 +66,10 @@ Check that `proof-check-proofs' signals an error with the expected message."
           (end-of-line)
           (insert " X ")
 
-          ;; proof-check-proofs should abort now with an error
+          ;; proof-check-report should abort now with an error
           (condition-case err-desc
               (progn
-                (proof-check-proofs nil)
+                (proof-check-report nil)
                 ;; Still here? Make test fail!
                 (should nil))
             (error

coq/coq.el

@@ -1963,7 +1963,7 @@ 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
+  ;; proof-check-report/proof-check-annotate config
   (setq
    proof-get-proof-info-fn #'coq-get-proof-info-fn
    proof-retract-command-fn #'coq-retract-command)
@@ -2282,7 +2282,7 @@ Function for `proof-tree-display-stop-command'."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; proof-check-proofs support
+;; proof-check-report/proof-check-annotate support
 ;;
 
 (defun coq-get-proof-info-fn ()

doc/PG-adapting.texi

@@ -1280,17 +1280,18 @@ asserted together.
 @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
+The commands @code{proof-check-report} and @code{proof-check-annotate}
+build on the omit-proofs feature. Using its machinery,
+@code{proof-check-proofs}, the inner working horse of both commands,
+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 it 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

doc/ProofGeneral.texi

@@ -2261,18 +2261,27 @@ the proof assistant to automatically process other files.
 @section Proof status statistic
 @cindex Proof status statistic
 
-The command @code{proof-check-proofs} (menu @code{Proof-General ->
+The command @code{proof-check-report} (menu @code{Proof-General ->
 Check Opaque Proofs}) generates the proof status of all opaque proofs
 in the current buffer, i.e., it generates an overview that shows which
 of the opaque proofs in the current buffer are currently valid and
 which are failing. When used interactively, the proof status is shown
 in the buffer @code{*proof-check-report*} (as long as
 @code{proof-check-report-buffer} is not changed).
 
-Currently @code{proof-check-proofs} does only work for Coq.
+The command @code{proof-check-annotate} (menu @code{Proof-General ->
+Annotate Failing Proofs}) modifies the current buffer and places
+comments containing @code{FAIL} on all failing opaque proofs. With
+prefix argument also the passing proofs are annotated with
+@code{PASS}. For configuring the position of these comments, see
+@code{proof-check-annotate-position} and
+@code{proof-check-annotate-right-margin}.
 
-@c TEXI DOCSTRING MAGIC: proof-check-proofs
-@deffn Command proof-check-proofs tap &optional batch
+Currently @code{proof-check-report} and @code{proof-check-annotate}
+only work for Coq.
+
+@c TEXI DOCSTRING MAGIC: proof-check-report
+@deffn Command proof-check-report tap &optional batch
 Generate an overview about valid and invalid proofs.@*
 This command completely processes the current buffer and
 generates an overview about all the opaque proofs in it and
@@ -2297,29 +2306,74 @@ command runs in batch mode.
 In the same way as the omit-proofs feature, this command only
 tolerates errors inside scripts of opaque proofs. Any other error
 is reported to the user without generating an overview. The
-overview only contains those names of theorems whose proofs
+overview only contains those names of theorems whose proof
 scripts are classified as opaque by the omit-proofs feature. For
 Coq for instance, among others, proof scripts terminated with
 @code{'Defined'} are not opaque and do not appear in the generated
 overview.
 
 Note that this command does not (re-)compile required files.
-Files must be required before running this commands, for instance
-by asserting all require commands beforehand.
+Dependencies must be compiled before running this commands, for
+instance by asserting all require commands beforehand.
+@end deffn
+
+@c TEXI DOCSTRING MAGIC: proof-check-annotate
+@deffn Command proof-check-annotate annotate-passing &optional save-buffer
+Annotate failing proofs in current buffer with a "@var{fail}" comment.@*
+This function modifies the current buffer in place. Use with
+care!
+
+Similarly to @samp{@code{proof-check-report}}, check all opaque proofs in the
+current buffer. Instead of generating a report, failing proofs
+are annotated with "@var{fail}" in a comment. With prefix argument
+(or when @var{annotate-passing} is non-nil) also passing proofs are
+annotated with a "@var{pass}" comment. Pass and fail comments can be
+placed at the last or second last statement before the opaque
+proof. For Coq this corresponds to the proof using and the
+theorem statement, respectively. In both cases the comment is
+placed at the right margin of the first line, see
+@samp{@code{proof-check-annotate-position}} and
+@samp{@code{proof-check-annotate-right-margin}}.
+
+Interactively, this command does not save the current buffer
+after placing the annotations. With @var{save-buffer} non-nil, the
+current buffer is saved if it has been modified.
 @end deffn
 
+@c TEXI DOCSTRING MAGIC: proof-check-annotate-position
+@defvar proof-check-annotate-position 
+Line for annotating proofs with "@var{pass}" or "@var{fail}" comments.@*
+This option determines the line where @samp{@code{proof-check-annotate}} puts
+comments with "@var{pass}" and "@var{fail}". Value `'theoren' uses the
+first line of the second last statement before the start of the
+opaque proof, which corresponds to the line containing a Theorem
+keyword for Coq. Value `'proof-using' uses the first line of the
+last statement before the opaque proof, which corresponds to the
+Proof using line for Coq.
+@end defvar
+
+@c TEXI DOCSTRING MAGIC: proof-check-annotate-right-margin
+@defvar proof-check-annotate-right-margin 
+Right margin for "@var{pass}" and "@var{fail}" comments.@*
+This option determines the right margin to which
+@samp{@code{proof-check-annotate}} right-aligns the comments with "@var{pass}"
+and "@var{fail}". If nil, the value of @samp{@code{fill-column}} is used.
+@end defvar
+
+
 @xref{Quick and inconsistent compilation} for enabling vos compilation
 inside Proof General and see @xref{Omitting proofs for speed} for the
 omit-proofs feature.
 
-The interactive use of this commands is limited because it only works
-on the current buffer. However, this commands can also be run in batch
-mode in a script, for instance in a continuous integration
-environment. To run this command on a file in batch mode, use
+The interactive use of @code{proof-check-report} and
+@code{proof-check-annotate} is limited because they only work on the
+current buffer. However, these commands can also be run in batch mode
+in a script, for instance in a continuous integration environment. To
+run @code{proof-check-report} on a file in batch mode, use
 
 @verbatim
 emacs -batch -l <your-pg-dir>/generic/proof-site.el <file> \
-      --eval '(proof-check-proofs <tap> <output>)'
+      --eval '(proof-check-report <tap> <output>)'
 @end verbatim
 
 where @code{<tap>} should be @code{nil} for human readable output and
@@ -2331,6 +2385,11 @@ quotes. Then the proof status is written to this file. (If
 into the @code{*proof-check-report*} buffer, which does not make much
 sense in a batch command as the one above.)
 
+Using a similar command also @code{proof-check-annotate} can run in
+batch mode in a continuous integration environment, for instance for
+checking that all failing proofs are annotated with @code{FAIL}
+via @code{git diff --exit-code}.
+
 
 @node Automatic multiple file handling
 @section Automatic multiple file handling
@@ -5253,7 +5312,7 @@ non-opaque, even if they have proof-local effect only, such as
 @node Proof status statistic for Coq
 @section Proof status statistic for Coq
 
-The command @code{proof-check-proofs} (menu @code{Proof-General ->
+The command @code{proof-check-report} (menu @code{Proof-General ->
 Check Opaque Proofs}) generates the proof status of all opaque proofs
 in the current buffer, i.e., it generates an overview that shows which
 of the opaque proofs in the current buffer are currently valid and
@@ -5262,7 +5321,14 @@ where invalid proofs are permitted and vos compilation (@xref{Quick
 and inconsistent compilation}) and the omit proofs feature
 (@xref{Omitting proofs for speed}) are used to work at the most
 interesting or challenging point instead of on the first invalid
-proof. See @xref{Proof status statistic} for more details.
+proof.
+
+The command @code{proof-check-annotate} (menu @code{Proof-General ->
+Annotate Failing Proofs}) can then be used to consistently annotate
+failing proofs with a @code{FAIL} comment or to check, e.g., in
+continuous integration, that such comments are present.
+
+See @xref{Proof status statistic} for more details.
 
 
 @node Editing multiple proofs