From e52c7b75e4863a64fc77fe830f36a616e2220898 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 25 Mar 2024 13:57:45 +0100 Subject: [PATCH 1/9] omit-proofs: split command processing into two phases The first phase only classifies proofs to be omitted and stuff not to be omitted. The second phase does the actual replacement and adjusts the overlays/spans. Feature wise this commit does not change anything but it enables reusing the first phase for new features. Additionally, slightly extend the omit proofs test. --- ci/simple-tests/coq-test-omit-proofs.el | 20 +- generic/proof-script.el | 261 +++++++++++++++++------- 2 files changed, 207 insertions(+), 74 deletions(-) diff --git a/ci/simple-tests/coq-test-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el index f2c140bc3..ed7aea8d5 100644 --- a/ci/simple-tests/coq-test-omit-proofs.el +++ b/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 () diff --git a/generic/proof-script.el b/generic/proof-script.el index 854bd6bf8..afa2e50b6 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1985,6 +1985,15 @@ Assumes that point is at the end of a command." ;; buffer content has been converted to vanilla spans, ;; `proof-script-omit-proofs' searches for complete opaque proofs in ;; there and replaces them with `proof-script-proof-admit-command'. +;; +;; The replacement works in two phases. First, +;; `proof-script-omit-filter' transfers the list of vanilla spans into +;; a list of lists of these spans, where each sublist is tagged with +;; either `'proof' or `'no-proof'. Second, `proof-script-omit-proofs' +;; replaces the proof parts with admit commands. Partitioning into two +;; phases makes it possible to reuse the first phase for different +;; features. See the documentation of `proof-script-omit-filter' for a +;; specification of the list of lists result type. (defun proof-move-over-whitespace-to-next-line (pos) "Return position of next line if one needs only to jump over white space. @@ -1999,33 +2008,78 @@ line, otherwise POS." (if (eolp) (1+ (point)) pos))) - -(defun proof-script-omit-proofs (vanillas) - "Return a copy of VANILLAS with complete opaque proofs omitted. + +(defun proof-script-omit-filter (vanillas) + "Classify VANILLAS into those which are inside and those outside of proofs. +Classify the list of vanilla spans VANILLAS into those belonging +to a proof script that can be omitted by the omit proofs feature +and those which can not be omitted (either outside proofs or +inside proofs that cannot be omitted). + See `proof-omit-proofs-configured' for the description of the omit proofs feature. This function uses `proof-script-proof-start-regexp', `proof-script-proof-end-regexp' and `proof-script-definition-end-regexp' to search for complete -opaque proofs in the action list VANILLAS. Complete opaque proofs -are replaced by `proof-script-proof-admit-command'. The span of -the admit command contains an 'omitted-proof-region property with -the region of the omitted proof. This is used in -`proof-done-advancing-save' to colour the omitted proof with -`proof-omitted-proof-face'. - -Report an error to the (probably surprised) user if another proof -start is found inside a proof." +opaque proofs in the action list VANILLAS. Additionally, it uses +`proof-script-cmd-prevents-proof-omission' and +`proof-script-cmd-force-next-proof-kept' to detect proofs that +cannot be omitted. + +The result is a list of chunks, where each chunk is a list that +contains a type tag as first element. The chunk list is returned +in reversed order, i.e., the first vanilla span in VANILLAS is +inside the last chunk. + +There are three types of chunks: 'proof for commands inside a +proof that can be omitted, 'no-proof for commands that are +outside a proof or cannot be omitted, and 'nested for commands +that contain a nested proof. Note that there may be several +adjacent 'no-proof chunks, for instance for commands outside a +proof followed by a proof that cannot be omitted. + +The 'proof chunk has 4 elements: + +('proof proof-cmds-reversed span-start-first-proof-cmd span-end-first-proof-cmd) + +The second, proof-cmds-reversed, contains the vanilla spans from +VANILLAS corresponding to commands belonging to a proof, +excluding the first that matched +`proof-script-proof-start-regexp' and including the last that +matched `proof-script-proof-end-regexp' in reversed order. The +third element span-start-first-proof-cmd is the position of the +start of the command that matched +`proof-script-proof-start-regexp' and span-end-first-proof-cmd is +the position of the end of that command. + +The 'no-proof chunk has 2 elements. + +('no-proof cmds-reversed) + +cmds-reversed contains the vanilla spans of VANILLAS in reversed +order. + +The 'nested-proof chunk has 3 elements. + +('nested-proof cmds-reversed line-number-nested-proof) + +line-number-nested-proof is the line number where the nested +proof was detected. cmds-reversed is the tail of VANILLAS, +containing the start of the nested proof, in reversed order. If +there is a 'nested-proof chunk in the result, it is the first +chunk." (cl-assert (and proof-omit-proofs-configured proof-script-proof-start-regexp proof-script-proof-end-regexp proof-script-definition-end-regexp proof-script-proof-admit-command) nil "proof-script omit proof feature not properly configured") - (let (;; result vanillas with omitted proofs in reverse order - result - ;; commands of current proof before deciding opaqueness in reverse order + (let (;; result in reversed order + result-chunks + ;; accumulated commands in reversed order before they are put + ;; into a result chunk maybe-result + ;; flag: is the processing loop currently inside a proof or not? inside-proof proof-start-span-start proof-start-span-end ;; t if the proof contains state changing commands and must be kept @@ -2045,25 +2099,18 @@ start is found inside a proof." (progn (if (string-match proof-script-proof-start-regexp cmd) ;; Found another proof start inside a proof. - ;; Stop omitting and pass the remainder unmodified. - ;; The result in `result' is aggregated in reverse - ;; order, need to reverse vanillas. + ;; Stop classifying and return the remainder as + ;; 'no-proof chunk. The commands in `result-chunks' + ;; are in reverse order, need to reverse the remaining + ;; vanillas. (progn - (setq result (nconc (nreverse vanillas) maybe-result result)) + (push (list 'nested-proof + (nconc (nreverse vanillas) maybe-result) + (line-number-at-pos (span-end (car item)))) + result-chunks) (setq maybe-result nil) ;; terminate the while loop - (setq vanillas nil) - ;; for Coq nobody will notice the warning, because - ;; the error about nested proofs will pop up shortly - ;; afterwards - (display-warning - '(proof-script) - ;; use the end of the span, because the start is - ;; usually on the preceding line - (format (concat "found second proof start at line %d" - " - are there nested proofs?") - (line-number-at-pos (span-end (car item)))))) - + (setq vanillas nil)) ;; else - no nested proof, but still inside-proof (if (and (string-match proof-script-proof-end-regexp cmd) (not proof-must-be-kept)) @@ -2071,43 +2118,13 @@ start is found inside a proof." ;; recognize a state changing command inside the ;; proof that would prohibit throwing the proof ;; away. - (let - ;; Reuse the Qed span for the whole proof, - ;; including the faked Admitted command. - ;; `proof-done-advancing' expects such a span. - ((cmd-span (car item))) - (span-set-property cmd-span 'type 'omitted-proof) - (span-set-property cmd-span - 'cmd proof-script-proof-admit-command) - (span-set-endpoints cmd-span proof-start-span-end - (span-end (car item))) - ;; Throw away all commands between start of proof - ;; and the current point, in particular, delete - ;; all the spans. - (mapc - (lambda (item) (span-detach (car item))) - maybe-result) + (progn + (push (list 'proof + (cons item maybe-result) + proof-start-span-start + proof-start-span-end) + result-chunks) (setq maybe-result nil) - ;; Record start and end point for the fancy - ;; colored span that marks the skipped proof. The - ;; span will be created in - ;; `proof-done-advancing-save' when - ;; `proof-script-proof-admit-command' is retired. - (span-set-property - cmd-span 'omitted-proof-region - ;; for the start take proper line start if possible - (list (proof-move-over-whitespace-to-next-line - proof-start-span-start) - ;; For the end, don't extend to the end of - ;; the line, because then the fancy color - ;; span is behind the end of the proof span - ;; and will get deleted when undoing just - ;; behind that proof. - (span-end (car item)))) - (push (list cmd-span - (list proof-script-proof-admit-command) - 'proof-done-advancing nil) - result) (setq inside-proof nil)) ;; else - no nested proof, no opaque proof, but still inside @@ -2119,7 +2136,9 @@ start is found inside a proof." ;; such that the proof-must-be-kept. ;; Need to keep all commands from the start of the proof. (progn - (setq result (cons item (nconc maybe-result result))) + (push (list 'no-proof + (cons item maybe-result)) + result-chunks) (setq maybe-result nil) (setq inside-proof nil)) @@ -2139,9 +2158,12 @@ start is found inside a proof." ;; else - outside proof (if (string-match proof-script-proof-start-regexp cmd) (progn + (push (list 'no-proof + ;; Keep the Proof using command in the + ;; 'no-proof chunk. + (cons item maybe-result)) + result-chunks) (setq maybe-result nil) - ;; Keep the Proof using command in any case. - (push item result) (setq proof-start-span-start (span-start (car item))) (setq proof-start-span-end (span-end (car item))) (setq inside-proof t) @@ -2157,12 +2179,105 @@ start is found inside a proof." (setq next-proof-must-be-kept nil))) ;; keep current item unmodified - (push item result))) + (push item maybe-result))) (setq vanillas (cdr vanillas))) - ;; end of loop - return filtered vanillas - (nreverse (nconc maybe-result result)))) + ;; end of loop - keep remaining items + (when maybe-result + (push (list 'no-proof maybe-result) result-chunks)) + result-chunks)) +(defun proof-script-omit-proofs (vanillas) + "Return a copy of VANILLAS with complete opaque proofs omitted. +See `proof-omit-proofs-configured' for the description of the +omit proofs feature. This function uses +`proof-script-proof-start-regexp', +`proof-script-proof-end-regexp' and +`proof-script-definition-end-regexp' to search for complete +opaque proofs in the action list VANILLAS. Additionally, it uses +`proof-script-cmd-prevents-proof-omission' and +`proof-script-cmd-force-next-proof-kept' to detect proofs that +cannot be omitted. Complete opaque proofs are replaced by +`proof-script-proof-admit-command'. The span of the admit command +contains an 'omitted-proof-region property with the region of the +omitted proof. This is used in `proof-done-advancing-save' to +colour the omitted proof with `proof-omitted-proof-face'. + +Display a warning if another proof start is found inside a +proof." + (let ((chunks (proof-script-omit-filter vanillas)) + result) + (dolist (chunk chunks result) + (cond + ((eq (car chunk) 'nested-proof) + ;; chunk: ('nested-proof line-number-nested-proof cmds-reversed) + ;; + ;; A nested-proof chunk can only appear at the head when + ;; result is still empty. + (cl-assert (null result) nil + "proof-script-omit internal error: nested-proof not at head") + ;; Display a warning and keep the commands unmodified. + ;; + ;; For Coq nobody will notice the warning, because the error + ;; about nested proofs will pop up shortly afterwards. + (display-warning + '(proof-script) + ;; use the end of the span, because the start is + ;; usually on the preceding line + (format (concat "found second proof start at line %d" + " - are there nested proofs?") + (nth 2 chunk))) + (setq result (nreverse (nth 1 chunk)))) + + ((eq (car chunk) 'no-proof) + ;; chunk: ('no-proof cmds-reversed) + ;; + ;; keep all commands unmodified + (setq result (nconc (nreverse (nth 1 chunk)) result))) + + ((eq (car chunk) 'proof) + ;; chunk: ('proof span-start-first-proof-cmd + ;; span-end-first-proof-cmd + ;; proof-cmds-reversed) + (let* ((cmds-rev (nth 1 chunk)) + (proof-start-span-start (nth 2 chunk)) + (proof-start-span-end (nth 3 chunk)) + + (last-cmd-span (caar cmds-rev))) + ;; Reuse the span of the last proof command (Qed) for the + ;; whole proof, including the faked Admitted. + (span-set-property last-cmd-span 'type 'omitted-proof) + (span-set-property last-cmd-span 'cmd proof-script-proof-admit-command) + (span-set-endpoints last-cmd-span + proof-start-span-end + (span-end last-cmd-span)) + ;; Commands inside the proof are thrown away. Thererfore + ;; delete all their spans, except the span of the last proof + ;; command, which is reused here. + (mapc + (lambda (item) (span-detach (car item))) + (cdr cmds-rev)) + ;; Record start and end point for the fancy colored span + ;; that marks the skipped proof. The span will be created in + ;; `proof-done-advancing-save' when + ;; `proof-script-proof-admit-command' is retired. + (span-set-property + last-cmd-span 'omitted-proof-region + (list + ;; for the start take proper line start if possible + (proof-move-over-whitespace-to-next-line proof-start-span-start) + ;; For the end, don't extend to the end of the line, + ;; because then the fancy color span is behind the end of + ;; the proof span and will get deleted when undoing just + ;; behind that proof. + (span-end last-cmd-span))) + ;; replace proof commands by admit + (push (list last-cmd-span (list proof-script-proof-admit-command) + 'proof-done-advancing nil) + result))) + (t + (cl-assert nil nil + "proof-script-omit internal error: unknown chunk type")))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; From e26110323a3eb9331aae976f9d7d74eebdaa30a4 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 27 Mar 2024 20:50:45 +0100 Subject: [PATCH 2/9] proof-check: new feature for listing passing and failing tests M-x proof-check-proofs checks all proofs in one buffer and displays a list with which tests currently pass or fail. This is a Proof General implementation of coq/coq#1147. It enables a PVS-like workflow where files are processed with -vos and proof-omit-proofs-option enabled such that one can focus on the most interesting/difficult proof instead of the first failing one. --- ci/simple-tests/proof_stat.v | 24 +++++ coq/coq.el | 25 +++++ generic/pg-user.el | 180 +++++++++++++++++++++++++++++++++++ generic/proof-config.el | 39 ++++++++ 4 files changed, 268 insertions(+) create mode 100644 ci/simple-tests/proof_stat.v diff --git a/ci/simple-tests/proof_stat.v b/ci/simple-tests/proof_stat.v new file mode 100644 index 000000000..49411eeeb --- /dev/null +++ b/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. + diff --git a/coq/coq.el b/coq/coq.el index a036acde3..b6354bd1f 100644 --- a/coq/coq.el +++ b/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 diff --git a/generic/pg-user.el b/generic/pg-user.el index d4115a4ba..a45797ca3 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -597,6 +597,186 @@ last use time, to discourage saving these into the users database." + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Check validity of proofs +;; + +(defun proof-check-report (proof-results) + "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." + (let* ((ok-fail (seq-group-by #'car proof-results)) + (frmt " %-4s %s") + (frmt-face (propertize frmt 'face 'error)) + coq-proj-dir src-file) + ;; determine a relative file name for current buffer + (when buffer-file-name + (setq coq-proj-dir (locate-dominating-file buffer-file-name + coq-project-filename))) + (if coq-proj-dir + (setq src-file (file-relative-name buffer-file-name coq-proj-dir)) + (setq src-file (buffer-name))) + + ;; generate header + (with-current-buffer (get-buffer-create proof-check-report-buffer) + (erase-buffer) + (insert + (propertize (concat "Proof check results for " src-file) 'face 'bold) + "\n\n") + (insert + (format + (propertize "%d opaque proofs recognized: %d successful " 'face 'bold) + (length proof-results) + (length (cdr (assoc t ok-fail))))) + (insert (format (propertize "%d FAILING" 'face 'error 'face 'bold) + (length (cdr (assoc nil ok-fail))))) + (insert "\n\n") + ;; generate actual proof results + (dolist (pr proof-results) + (insert (format (if (car pr) frmt frmt-face) + (if (car pr) "OK " "FAIL") + (cadr pr))) + (insert "\n")) + (goto-char (point-min)) + (display-buffer (current-buffer))))) + +(defun proof-check-chunks (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 +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) + (while chunks + (let* ((chunk (car chunks)) ; cdr at end + (this-mode (car chunk)) + (next-mode (car-safe (car-safe (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))) + 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-add-to-queue (nreverse vanillas-rev-updated) 'advancing) + (proof-shell-wait) + ;; (redisplay) + (unless (eq lspan-end + (and proof-locked-span (span-end proof-locked-span))) + ;; not all the spans have been asserted - there was some error + (setq error t)) + (when (and error (eq this-mode 'no-proof)) + ;; all non-opaque stuff should be error free, abort and tell + ;; the user + (goto-char (proof-unprocessed-begin)) + (when (looking-at "$") + (forward-line 1)) + (error "Error encountered outside opaque proofs after line %d" + (line-number-at-pos))) + + (cond + ((and (eq this-mode 'no-proof) (eq next-mode 'proof)) + ;; non-opaque stuff has been processed error free, next + ;; chunk is an opaque proof - record information needed next + ;; round + (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")) + + ((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) + ;; opaque proof failed, retract, admit, and record error + (proof-add-to-queue + (list + (list nil (list (funcall proof-retract-command-fn + (car current-proof-state-and-name))) + 'proof-done-invisible (list 'invisible)) + (list nil (list proof-script-proof-admit-command) + 'proof-done-invisible (list 'invisible))) + 'advancing) + (proof-shell-wait) + (proof-set-locked-end lspan-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)))) + (setq chunks (cdr chunks)))) + (nreverse proof-results))) + +(defun proof-check-proofs () + "Generate overview about valid and invalid proofs in current buffer. +This command completely processes the current buffer and +generates an overview in the `proof-check-report-buffer' about +all the opaque proofs in it and whether their proof scripts are +valid or invalid. + +This command makes sense for a development process where invalid +proofs are permitted and vos compilation and the omit proofs +feature (see `proof-omit-proofs-configured') are used to work at +the most interesting or challenging point instead of on the first +invalid proof. + +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 +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." + (interactive) + (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))) + + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; diff --git a/generic/proof-config.el b/generic/proof-config.el index 39436918a..d8ede58f9 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -792,6 +792,45 @@ asserted together." :group 'proof-script) +;; proof-check-proofs configuration + +;; The omit-proofs feature must be fully configured for +;; `proof-check-proofs', see `proof-omit-proofs-configured'. + +(defcustom proof-get-proof-info-fn nil + "Return proof name and state number for `proof-check-proofs'. +Proof assistant specific function for `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 `proof-retract-command-fn'. +Processing the command returned by `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 +`proof-tree-get-proof-info'.)" + :type 'function + :group 'proof-script) + +(defcustom proof-retract-command-fn nil + "Function for retract command to a certain state. +This function takes a state as argument as returned by +`proof-get-proof-info-fn'. It should return a command that brings +the proof assistant back to the same state." + :type 'function + :group 'proof-script) + +(defconst proof-check-report-buffer "*proof-check-report*" + "Buffer name for the report of `proof-check-proofs'.") + + ;; ;; Proof script indentation ;; From 3c0a9891cb3c33cbb94fb9133a0e3633f13c0860 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 28 Mar 2024 21:29:29 +0100 Subject: [PATCH 3/9] CI: add proof-check tests --- ci/simple-tests/README.md | 4 +- ci/simple-tests/coq-test-proof-stat.el | 89 ++++++++++++++++++++++++++ 2 files changed, 92 insertions(+), 1 deletion(-) create mode 100644 ci/simple-tests/coq-test-proof-stat.el diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md index 523975c6e..140e72987 100644 --- a/ci/simple-tests/README.md +++ b/ci/simple-tests/README.md @@ -15,9 +15,11 @@ 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 # 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 new file mode 100644 index 000000000..d725d01e5 --- /dev/null +++ b/ci/simple-tests/coq-test-proof-stat.el @@ -0,0 +1,89 @@ +;; This file is part of Proof General. +;; +;; © Copyright 2024 Hendrik Tews +;; +;; Authors: Hendrik Tews +;; Maintainer: Hendrik Tews +;; +;; SPDX-License-Identifier: GPL-3.0-or-later + +;;; Commentary: +;; +;; 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 +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) + + ;; 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) + ;; 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))))) From a9f453d680df1378054516ecaed811c7bffb5096 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 1 Apr 2024 16:30:45 +0200 Subject: [PATCH 4/9] proof-stat: add batch mode and TAP support --- ci/simple-tests/coq-test-proof-stat.el | 4 +- generic/pg-user.el | 93 ++++++++++++++++++-------- 2 files changed, 67 insertions(+), 30 deletions(-) diff --git a/ci/simple-tests/coq-test-proof-stat.el b/ci/simple-tests/coq-test-proof-stat.el index d725d01e5..2db6a001c 100644 --- a/ci/simple-tests/coq-test-proof-stat.el +++ b/ci/simple-tests/coq-test-proof-stat.el @@ -36,7 +36,7 @@ Test that the report buffer contains the expected output." (find-file "proof_stat.v") ;; run check on file where all errors are in opaque parts - (proof-check-proofs) + (proof-check-proofs nil) ;; the result buffer should exist (should (buffer-live-p (get-buffer "*proof-check-report*"))) @@ -74,7 +74,7 @@ Check that `proof-check-proofs' signals an error with the expected message." ;; proof-check-proofs should abort now with an error (condition-case err-desc (progn - (proof-check-proofs) + (proof-check-proofs nil) ;; Still here? Make test fail! (should nil)) (error diff --git a/generic/pg-user.el b/generic/pg-user.el index a45797ca3..e8736fb1f 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -603,14 +603,20 @@ last use time, to discourage saving these into the users database." ;; Check validity of proofs ;; -(defun proof-check-report (proof-results) +(defun proof-check-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." +`proof-check-report-buffer' in human readable form or, if TAP is +not nil, in test anything protocol (TAP). If BATCH is not nil, +report the results via message, such that they appear on stdout +when Emacs runs in batch mode or, when BATCH is a string, append +the results to the file denoted by BATCH." (let* ((ok-fail (seq-group-by #'car proof-results)) (frmt " %-4s %s") (frmt-face (propertize frmt 'face 'error)) + (count 1) coq-proj-dir src-file) + ;; determine a relative file name for current buffer (when buffer-file-name (setq coq-proj-dir (locate-dominating-file buffer-file-name @@ -622,25 +628,43 @@ Report the results of `proof-check-proofs' in buffer ;; generate header (with-current-buffer (get-buffer-create proof-check-report-buffer) (erase-buffer) - (insert - (propertize (concat "Proof check results for " src-file) 'face 'bold) - "\n\n") - (insert - (format - (propertize "%d opaque proofs recognized: %d successful " 'face 'bold) - (length proof-results) - (length (cdr (assoc t ok-fail))))) - (insert (format (propertize "%d FAILING" 'face 'error 'face 'bold) - (length (cdr (assoc nil ok-fail))))) - (insert "\n\n") - ;; generate actual proof results + (if tap + (insert (format "TAP version 13\n1..%d\n" (length proof-results))) + ;; human output + (insert + (propertize (concat "Proof check results for " src-file) 'face 'bold) + "\n\n") + (insert + (format + (propertize "%d opaque proofs recognized: %d successful " 'face 'bold) + (length proof-results) + (length (cdr (assoc t ok-fail))))) + (insert (format (propertize "%d FAILING" 'face 'error 'face 'bold) + (length (cdr (assoc nil ok-fail))))) + (insert "\n\n")) (dolist (pr proof-results) - (insert (format (if (car pr) frmt frmt-face) - (if (car pr) "OK " "FAIL") - (cadr pr))) - (insert "\n")) - (goto-char (point-min)) - (display-buffer (current-buffer))))) + (if tap + (progn + (insert (format "%sok %d - %s\n" + (if (car pr) "" "not ") + count + (cadr pr))) + (setq count (1+ count))) + ;; human readable + (insert (format (if (car pr) frmt frmt-face) + (if (car pr) "OK " "FAIL") + (cadr pr))) + (insert "\n"))) + (if batch + (progn + (insert "\n\n") + (if (stringp batch) + (append-to-file (point-min) (point-max) batch) + (message "%s" + (buffer-substring-no-properties + (point-min) (point-max))))) + (goto-char (point-min)) + (display-buffer (current-buffer)))))) (defun proof-check-chunks (chunks) "Worker function for `proof-check-proofs for processing CHUNKS. @@ -727,12 +751,11 @@ as reported by `proof-get-proof-info-fn'." (setq chunks (cdr chunks)))) (nreverse proof-results))) -(defun proof-check-proofs () - "Generate overview about valid and invalid proofs in current buffer. +(defun proof-check-proofs (tap &optional batch) + "Generate an overview about valid and invalid proofs. This command completely processes the current buffer and -generates an overview in the `proof-check-report-buffer' about -all the opaque proofs in it and whether their proof scripts are -valid or invalid. +generates an overview about all the opaque proofs in it and +whether their proof scripts are valid or invalid. This command makes sense for a development process where invalid proofs are permitted and vos compilation and the omit proofs @@ -740,6 +763,16 @@ feature (see `proof-omit-proofs-configured') are used to work at the most interesting or challenging point instead of on the first invalid proof. +Argument TAP, which can be set by a prefix argument, controls the +form of the generated overview. Nil, without prefix, gives an +human readable overview, otherwise it's test anything +protocol (TAP). Argument BATCH controls where the overview goes +to. If nil, or in an interactive call, the overview appears in +`proof-check-report-buffer'. If BATCH is a string, it should be a +filename and the overview is appended there. Otherwise the +overview is output via `message' such that it appears on stdout +when this 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 @@ -747,8 +780,12 @@ overview only contains those names of theorems whose proofs 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." - (interactive) +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." + (interactive "P") (unless (and proof-omit-proofs-configured proof-get-proof-info-fn proof-retract-command-fn) @@ -773,7 +810,7 @@ overview." 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))) + (proof-check-report proof-results tap batch))) From 4f8e276ecd03de6ec25578a4152955e447bb8050 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Fri, 5 Apr 2024 21:55:05 +0200 Subject: [PATCH 5/9] PG manual: add documentation for proof-check-proofs --- doc/ProofGeneral.texi | 90 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 90 insertions(+) diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 3d1eac28d..9520d5cc3 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1916,6 +1916,7 @@ General covered in this chapter. * View of processed files :: * Retracting across files:: * Asserting across files:: +* Proof status statistic:: * Automatic multiple file handling:: * Escaping script management:: * Editing features:: @@ -2256,6 +2257,80 @@ unmodified buffers. This is particularly useful as assertion may cause the proof assistant to automatically process other files. +@node Proof status statistic +@section Proof status statistic +@cindex Proof status statistic + +The command @code{proof-check-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. + +@c TEXI DOCSTRING MAGIC: proof-check-proofs +@deffn Command proof-check-proofs 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 +whether their proof scripts are valid or invalid. + +This command makes sense for a development process where invalid +proofs are permitted and vos compilation and the omit proofs +feature (see @samp{@code{proof-omit-proofs-configured}}) are used to work at +the most interesting or challenging point instead of on the first +invalid proof. + +Argument @var{tap}, which can be set by a prefix argument, controls the +form of the generated overview. Nil, without prefix, gives an +human readable overview, otherwise it's test anything +protocol (@var{tap}). Argument @var{batch} controls where the overview goes +to. If nil, or in an interactive call, the overview appears in +@samp{@code{proof-check-report-buffer}}. If @var{batch} is a string, it should be a +filename and the overview is appended there. Otherwise the +overview is output via @samp{message} such that it appears on stdout +when this 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 +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. +@end deffn + +@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 buffer in batch mode, use + +@verbatim +emacs -batch -l /generic/proof-site.el \ + --eval '(proof-check-proofs )' +@end verbatim + +where @code{} should be @code{nil} for human readable output and +@code{t} for test anything protocol. If @code{} is @code{t} +the proof status appears in the standard output of the Emacs process. +Otherwise @code{} should be a filename as string in double +quotes. Then the proof status is appended to this file. (If +@code{output} is @code{nil} or omitted, the proof status is only put +into the @code{*proof-check-report*} buffer, which does not make much +sense in a batch command as the one above.) + + @node Automatic multiple file handling @section Automatic multiple file handling @@ -4232,6 +4307,7 @@ assistant. It supports most of the generic features of Proof General. * Proof using annotations:: * Multiple File Support:: * Omitting proofs for speed:: +* Proof status statistic for Coq:: * Editing multiple proofs:: * User-loaded tactics:: * Indentation tweaking:: @@ -5173,6 +5249,20 @@ non-opaque, even if they have proof-local effect only, such as @end itemize +@node Proof status statistic for Coq +@section Proof status statistic for Coq + +The command @code{proof-check-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. This command is useful for +a development process 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. + + @node Editing multiple proofs @section Editing multiple proofs From be3f8c992c24177bb3ba5c1ab5e315991fa3eb88 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sat, 6 Apr 2024 11:47:16 +0200 Subject: [PATCH 6/9] proof-stat: add menu item for proof-check-proofs --- doc/ProofGeneral.texi | 34 ++++++++++++++++++---------------- generic/proof-menu.el | 6 +++++- 2 files changed, 23 insertions(+), 17 deletions(-) diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 9520d5cc3..de74c7c1d 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -2261,12 +2261,13 @@ the proof assistant to automatically process other files. @section Proof status statistic @cindex Proof status statistic -The command @code{proof-check-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). +The command @code{proof-check-proofs} (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. @@ -2314,7 +2315,7 @@ 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 buffer in batch mode, use +environment. To run this command on a file in batch mode, use @verbatim emacs -batch -l /generic/proof-site.el \ @@ -5252,15 +5253,16 @@ 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} 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. This command is useful for -a development process 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. +The command @code{proof-check-proofs} (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. This command is useful for a development process +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. @node Editing multiple proofs diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 77bc05a84..35f6741a9 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -702,7 +702,11 @@ without adjusting window layout." :active pg-next-error-regexp] ["Scripting Active" proof-toggle-active-scripting :style toggle - :selected (eq proof-script-buffer (current-buffer))]) + :selected (eq proof-script-buffer (current-buffer))] + ["Check Opaque Proofs" proof-check-proofs + :active (and proof-omit-proofs-configured + proof-get-proof-info-fn + proof-retract-command-fn)]) "The Proof General generic menu for scripting buffers.") From 4f7f5b13cc702d37e16bb173aba4a43c988e2c29 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sat, 6 Apr 2024 18:38:57 +0200 Subject: [PATCH 7/9] proof-stat: add documentation for proof-check-proofs in PG-adapting --- doc/PG-adapting.texi | 53 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 3e5e72e39..d6adccdbf 100644 --- a/doc/PG-adapting.texi +++ b/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 From 3d5055da895e4e721f799094e47b5b239e0a837d Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sat, 6 Apr 2024 18:58:27 +0200 Subject: [PATCH 8/9] proof-stat: add CHANGES entry --- CHANGES | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/CHANGES b/CHANGES index b8d846b91..f0dbcf664 100644 --- a/CHANGES +++ b/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 From 1440ac2d0c7aba5104406fabe394c6462ce23341 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 15 Apr 2024 13:36:30 +0200 Subject: [PATCH 9/9] 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)))