From faccf95ba9c03519f7f02c1688039590207d99a0 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 29 Apr 2024 15:22:33 +0200 Subject: [PATCH] proof-stat: add feature to annotate failing proofs with FAIL ... see documentation of proof-check-annotate --- CHANGES | 9 +- ci/simple-tests/Makefile | 6 +- ci/simple-tests/coq-test-proof-stat.el | 14 +- coq/coq.el | 4 +- doc/PG-adapting.texi | 23 +-- doc/ProofGeneral.texi | 94 ++++++++++-- generic/pg-user.el | 198 ++++++++++++++++++------- generic/proof-config.el | 5 +- generic/proof-menu.el | 6 +- generic/proof-useropts.el | 26 ++++ 10 files changed, 290 insertions(+), 95 deletions(-) diff --git a/CHANGES b/CHANGES index f0dbcf664..f27719060 100644 --- a/CHANGES +++ b/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 diff --git a/ci/simple-tests/Makefile b/ci/simple-tests/Makefile index c8a506f48..bda2499fa 100644 --- a/ci/simple-tests/Makefile +++ b/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 diff --git a/ci/simple-tests/coq-test-proof-stat.el b/ci/simple-tests/coq-test-proof-stat.el index 821077da8..86470f954 100644 --- a/ci/simple-tests/coq-test-proof-stat.el +++ b/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 diff --git a/coq/coq.el b/coq/coq.el index b6354bd1f..b48715d55 100644 --- a/coq/coq.el +++ b/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 () diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index d6adccdbf..d63478a38 100644 --- a/doc/PG-adapting.texi +++ b/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 diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index d9a29a164..8ff0a479f 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -2261,7 +2261,7 @@ 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 @@ -2269,10 +2269,19 @@ 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 /generic/proof-site.el \ - --eval '(proof-check-proofs )' + --eval '(proof-check-report )' @end verbatim where @code{} 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 diff --git a/generic/pg-user.el b/generic/pg-user.el index 2818c8ca5..9dffd24e2 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -610,7 +610,45 @@ last use time, to discourage saving these into the users database." ;; Check validity of proofs ;; -(defun proof-check-report (proof-results tap batch) +(defun proof-check-annotate-source (proof-results annotate-passing) + "Annotate proofs in current buffer according to PROOF-RESULTS. +PROOF-RESULTS must be the return value of `proof-check-proofs' or +`proof-check-chunks' for the current buffer. This function +annotates failing proofs with a comment containing \"FAIL\" and, +if annotate-passing is non-nil, also passing proofs with +\"PASS\". The annotation will be right aligned in the line +according to `proof-check-annotate-position'. The position for +right alignment is configured in +`proof-check-annotate-right-margin'." + (let ((goal-column (or proof-check-annotate-right-margin fill-column))) + (save-excursion + (dolist (pr (nreverse proof-results)) + (when (or annotate-passing (not (car pr))) + (let ((pass (car pr)) + (annot-pos + (cond ((eq proof-check-annotate-position 'theorem) + (nth 2 pr)) + ((eq proof-check-annotate-position 'proof-using) + (nth 3 pr)) + (t + (error "Invalid value in `proof-check-annotate-position'")))) + eol-pos fill) + (goto-char annot-pos) + (re-search-forward "[[:blank:]\n]*") + (end-of-line) + (when (looking-back "(\\* \\(PASS\\|FAIL\\) \\*)") + (delete-char -10)) + (delete-horizontal-space) + (setq eol-pos (point)) + (beginning-of-line) + (setq fill (- goal-column (- eol-pos (point)) 10)) + (when (< fill 1) + (setq fill 1)) + (end-of-line) + (insert (make-string fill ? ) + "(* " (if pass "PASS" "FAIL") " *)"))))))) + +(defun proof-check-generate-report (proof-results tap batch) "Report `proof-check-proofs' results in PROOF-RESULTS in special buffer. Report the results of `proof-check-proofs' in buffer `proof-check-report-buffer' in human readable form or, if TAP is @@ -677,45 +715,57 @@ the results to the file denoted by BATCH." (display-buffer (current-buffer)))))) (defun proof-check-chunks (chunks) - "Worker function for `proof-check-proofs for processing CHUNKS. + "Worker function for `proof-check-proofs' for processing CHUNKS. CHUNKS must be the reversed result of `proof-script-omit-filter' for a whole buffer. (Only the top-level must be reversed, the commands inside the chunks must be as returned by `proof-script-omit-filter', that is in reversed order.) CHUNKS must not contain any 'nested-proof chunk. -This function processes the content of CHUNK normally by +This function processes the content of CHUNKS normally by asserting them one by one. Any error reported inside a 'no-proof chunk is reported as error to the user. 'proof chunks containing errors are silently replaced by `proof-script-proof-admit-command'. The result is a list of proof status results, one for each 'proof chunk in the same order. Each -proof-status result is a list with first element `t' or `nil', -depending on whether the proof failed, and the name of the proof -as reported by `proof-get-proof-info-fn'." - (let (proof-results current-proof-state-and-name) +proof-status result is a list of 4 elements as follows. +- 1st: proof status as `t' or `nil'. +- 2nd: the name of the proof as reported by + `proof-get-proof-info-fn'. +- 3rd: Position of the start of the span containing the theorem + to prove. More precisely, it is the second last span of the + 'no-proof chunk before the 'proof chunk. Note that spans + usually contain preceeding white space. Therefore this position + is not necessarily the first letter of the keyword introducing + the theorem statement. +- 4rd: Position of the start of the span containing \"Proof + using\". More precisely, it is the last span in the 'no-proof + chunk before the proof." + (let (proof-results current-proof-state-and-name proof-start-points) (while chunks (let* ((chunk (car chunks)) ; cdr at end (this-mode (car chunk)) - (next-mode (car-safe (car-safe (cdr chunks)))) + (next-mode (car (car (cdr chunks)))) (vanillas-rev (nth 1 chunk)) ;; add 'empty-action-list flag to last item to avoid the ;; call to `proof-shell-empty-action-list-command' - (litem (car vanillas-rev)) - (lspan-end (span-end (car litem))) - (nlitem (list (nth 0 litem) (nth 1 litem) (nth 2 litem) - (cons 'empty-action-list (nth 3 litem)))) - (vanillas-rev-updated (cons nlitem (cdr vanillas-rev))) + (last-item (car vanillas-rev)) + (2nd-last-item (cadr vanillas-rev)) + (last-span-end (span-end (car last-item))) + (new-last-item (list (nth 0 last-item) (nth 1 last-item) + (nth 2 last-item) + (cons 'empty-action-list (nth 3 last-item)))) + (vanillas-rev-updated (cons new-last-item (cdr vanillas-rev))) error) ;; if this is a proof chunk the next must be no-proof or must not exist (cl-assert (or (not (eq this-mode 'proof)) (or (eq next-mode 'no-proof) (eq next-mode nil))) nil "proof-check: two adjacent proof chunks") - (proof-set-queue-endpoints (proof-unprocessed-begin) lspan-end) + (proof-set-queue-endpoints (proof-unprocessed-begin) last-span-end) (proof-add-to-queue (nreverse vanillas-rev-updated) 'advancing) (proof-shell-wait) ;; (redisplay) - (unless (eq lspan-end + (unless (eq last-span-end (and proof-locked-span (span-end proof-locked-span))) ;; not all the spans have been asserted - there was some error (setq error t)) @@ -736,13 +786,14 @@ as reported by `proof-get-proof-info-fn'." (setq current-proof-state-and-name (funcall proof-get-proof-info-fn)) (cl-assert (cadr current-proof-state-and-name) - nil "proof-check: no proof name at proof start")) + nil "proof-check: no proof name at proof start") + (setq proof-start-points + (list (span-start (car 2nd-last-item)) ; start of Lemma + (span-start (car last-item))))) ; start of Proof using ((eq this-mode 'proof) ; implies next-mode is no-proof ;; opaque proof chunk processed - with or without error - (if (not error) - (push (list t (cadr current-proof-state-and-name)) - proof-results) + (when error ;; opaque proof failed, retract, admit, and record error (proof-add-to-queue (list @@ -753,15 +804,56 @@ as reported by `proof-get-proof-info-fn'." 'proof-done-invisible (list 'invisible))) 'advancing) (proof-shell-wait) - (proof-set-locked-end lspan-end) + (proof-set-locked-end last-span-end) (cl-assert (not (cadr (funcall proof-get-proof-info-fn))) - nil "proof-check: still in proof after admitting") - (push (list nil (cadr current-proof-state-and-name)) - proof-results)))) + nil "proof-check: still in proof after admitting")) + (push + (cons (not error) + (cons (cadr current-proof-state-and-name) proof-start-points)) + proof-results))) + (setq chunks (cdr chunks)))) (nreverse proof-results))) -(defun proof-check-proofs (tap &optional batch) +(defun proof-check-proofs () + "Check proofs in current buffer and return a list of proof status results. +This is the internal worker for `proof-check-report' and +`proof-check-annotate'. + +Reset scripting and then check all opaque proof in the current +buffer, relying on the omit-proofs feature, see +`proof-script-omit-filter' and `proof-omit-proofs-configured'. +The results are returned as list of proof status results (a list +of 4-element lists), see `proof-check-chunks'. + +This function does not (re-)compile required files." + (unless (and proof-omit-proofs-configured + proof-get-proof-info-fn + proof-retract-command-fn) + (error + "proof-check-proofs has not been configured for your proof assistant")) + ;; kill proof assistant and retract completely + (when (buffer-live-p proof-shell-buffer) + (proof-shell-exit t)) + ;; initialize scripting - taken from `proof-assert-until-point' + (proof-activate-scripting nil 'advancing) + (let* ((semis (proof-segment-up-to-using-cache (point-max))) + (vanillas (proof-semis-to-vanillas + semis + '(no-response-display no-goals-display))) + (chunks-rev (proof-script-omit-filter vanillas)) + (last-chunk (car chunks-rev)) + (chunks (nreverse chunks-rev)) + proof-results) + (when (eq (car last-chunk) 'nested-proof) + (error "Nested proof detected at line %d" (nth 2 last-chunk))) + (cl-assert (not (eq (caar chunks) 'proof)) + nil "proof-check: first chunk cannot be a proof") + (setq proof-results (proof-check-chunks chunks)) + (proof-shell-exit t) + proof-results)) + +(defun 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 @@ -786,42 +878,42 @@ 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 '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." (interactive "P") - (unless (and proof-omit-proofs-configured - proof-get-proof-info-fn - proof-retract-command-fn) - (error - "proof-check-proofs has not been configured for your proof assistant")) - ;; kill proof assistant and retract completely - (when (buffer-live-p proof-shell-buffer) - (proof-shell-exit t)) - ;; initialize scripting - taken from `proof-assert-until-point' - (proof-activate-scripting nil 'advancing) - (let* ((semis (proof-segment-up-to-using-cache (point-max))) - (vanillas (proof-semis-to-vanillas - semis - '(no-response-display no-goals-display))) - (chunks-rev (proof-script-omit-filter vanillas)) - (last-chunk (car chunks-rev)) - (chunks (nreverse chunks-rev)) - proof-results) - (when (eq (car last-chunk) 'nested-proof) - (error "Nested proof detected at line %d" (nth 2 last-chunk))) - (cl-assert (not (eq (caar chunks) 'proof)) - nil "proof-check: first chunk cannot be a proof") - (setq proof-results (proof-check-chunks chunks)) - (proof-shell-exit t) - (proof-check-report proof-results tap batch))) - + (proof-check-generate-report (proof-check-proofs) tap batch)) + +(defun proof-check-annotate (annotate-passing &optional save-buffer) + "Annotate failing proofs in current buffer with a \"FAIL\" comment. +This function modifies the current buffer in place. Use with +care! + +Similarly to `proof-check-report', check all opaque proofs in the +current buffer. Instead of generating a report, failing proofs +are annotated with \"FAIL\" in a comment. With prefix argument +(or when ANNOTATE-PASSING is non-nil) also passing proofs are +annotated with a \"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 +`proof-check-annotate-position' and +`proof-check-annotate-right-margin'. + +Interactively, this command does not save the current buffer +after placing the annotations. With SAVE-BUFFER non-nil, the +current buffer is saved if it has been modified." + (interactive "P") + (proof-check-annotate-source (proof-check-proofs) annotate-passing) + (when save-buffer + (save-buffer))) diff --git a/generic/proof-config.el b/generic/proof-config.el index d8ede58f9..1c5ede807 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -792,10 +792,11 @@ asserted together." :group 'proof-script) -;; proof-check-proofs configuration +;; configuration for proof-check-report and proof-check-annotate ;; The omit-proofs feature must be fully configured for -;; `proof-check-proofs', see `proof-omit-proofs-configured'. +;; proof-check-report and proof-check-annotate, see +;; `proof-omit-proofs-configured'. (defcustom proof-get-proof-info-fn nil "Return proof name and state number for `proof-check-proofs'. diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 35f6741a9..09b6c3d51 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -703,7 +703,11 @@ without adjusting window layout." ["Scripting Active" proof-toggle-active-scripting :style toggle :selected (eq proof-script-buffer (current-buffer))] - ["Check Opaque Proofs" proof-check-proofs + ["Check Opaque Proofs" proof-check-report + :active (and proof-omit-proofs-configured + proof-get-proof-info-fn + proof-retract-command-fn)] + ["Annotate Failing Proofs" proof-check-annotate :active (and proof-omit-proofs-configured proof-get-proof-info-fn proof-retract-command-fn)]) diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index 0cc92637b..eb0e497c4 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -114,6 +114,32 @@ disables omitting proofs." :type 'boolean :group 'proof-user-options) +(defcustom proof-check-annotate-position 'theorem + "Line for annotating proofs with \"PASS\" or \"FAIL\" comments. +This option determines the line where `proof-check-annotate' puts +comments with \"PASS\" and \"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." + :type + '(radio + (const :tag "line of theorem statement" theorem) + (const :tag "line before the proof (Proof using for Coq)" proof-using)) + :safe (lambda (v) (or (eq v 'theorem) (eq v 'proof-using)))) + +(defcustom proof-check-annotate-right-margin nil + "Right margin for \"PASS\" and \"FAIL\" comments. +This option determines the right margin to which +`proof-check-annotate' right-aligns the comments with \"PASS\" +and \"FAIL\". If nil, the value of `fill-column' is used." + :type + '(choice + (const :tag "use value of `fill-column'" nil) + (integer :tag "right margin")) + :safe (lambda (v) (or (eq v nil) (integerp v)))) + (defcustom pg-show-hints t "*Whether to display keyboard hints in the minibuffer." :type 'boolean