diff --git a/ci/simple-tests/coq-test-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el index d676ab34b..1779f372a 100644 --- a/ci/simple-tests/coq-test-omit-proofs.el +++ b/ci/simple-tests/coq-test-omit-proofs.el @@ -92,10 +92,11 @@ configured there may be taken from faces with less priority." "Test the omit proofs feature. In particular, test that with proof-omit-proofs-option configured: - the proof _is_ processed when using a prefix argument -- in this case the proof as normal locked color +- 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" (setq proof-omit-proofs-option t proof-three-window-enable nil) (reset-coq) @@ -175,6 +176,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..264270efe 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 span-start-first-proof-cmd span-end-first-proof-cmd proof-cmds-reversed) + +The last, 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 +second 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 line-number-nested-proof cmds-reversed) + +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 + (line-number-at-pos (span-end (car item))) + (nconc (nreverse vanillas) maybe-result)) + 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 + proof-start-span-start + proof-start-span-end + (cons item maybe-result)) + 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,104 @@ 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 1 chunk))) + (setq result (nreverse (nth 2 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* ((proof-start-span-start (nth 1 chunk)) + (proof-start-span-end (nth 2 chunk)) + (cmds-rev (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")))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;