diff --git a/ci/simple-tests/coq-test-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el index 891343370..2204d0e91 100644 --- a/ci/simple-tests/coq-test-omit-proofs.el +++ b/ci/simple-tests/coq-test-omit-proofs.el @@ -178,7 +178,6 @@ In particular, test that with proof-omit-proofs-option configured: (should (eq (first-overlay-face) 'proof-locked-face))) (ert-deftest omit-proofs-never-omit-hints () - :expected-result :failed "Test that proofs containing Hint are never omitted. This test only checks that the face in the middle of the proof is the normal `proof-locked-face'. diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index e485449b9..9071ffa4b 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1428,6 +1428,11 @@ different." (defconst coq-command-decl-regexp (coq-add-command-prefix coq-keywords-decl)) (defconst coq-command-defn-regexp (coq-add-command-prefix coq-keywords-defn)) +(defconst coq-lowercase-command-regexp "^[a-z]" + "Regular expression matching commands starting with a lowercase letter. +Used in `coq-cmd-prevents-proof-omission' to identify tactics +that only have proof-local effects.") + ;; must match: ;; "with f x y :" (followed by = or not) ;; "with f x y (z:" (not followed by =) diff --git a/coq/coq.el b/coq/coq.el index 5de2374fa..127f77800 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -745,6 +745,18 @@ If locked span already has a state number, then do nothing. Also updates ;; (message "Unknown command, hopes this won't desynchronize ProofGeneral") ;; t)))) +(defun coq-cmd-prevents-proof-omission (cmd) + "Instanciation for `proof-script-cmd-prevents-proof-omission'. +This predicate decides whether a command inside a proof might +have effects outside the proof, which would prohibit omitting the +proof, see `proof-script-omit-proofs'. + +Commands starting lower case are deemed as tactics that have +proof local effect only. Everything else is checked against the +STATECH field in the coq syntax data base, see coq-db.el." + (if (proof-string-match coq-lowercase-command-regexp cmd) + nil + (not (coq-state-preserving-p cmd)))) (defun coq-hide-additional-subgoals-switch () "Function invoked when the user switches option `coq-hide-additional-subgoals'." @@ -1954,7 +1966,8 @@ at `proof-assistant-settings-cmds' evaluation time.") proof-script-proof-start-regexp coq-proof-start-regexp proof-script-proof-end-regexp coq-proof-end-regexp proof-script-definition-end-regexp coq-definition-end-regexp - proof-script-proof-admit-command coq-omit-proof-admit-command) + proof-script-proof-admit-command coq-omit-proof-admit-command + proof-script-cmd-prevents-proof-omission #'coq-cmd-prevents-proof-omission) (setq proof-cannot-reopen-processed-files nil) diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 8f057a78f..f04022d6f 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1187,10 +1187,14 @@ match of @samp{@code{proof-script-proof-end-regexp}}, are omitted (not send to the proof assistant) and replaced by @samp{@code{proof-script-proof-admit-command}}. If a match for @samp{@code{proof-script-definition-end-regexp}} is found while searching -forward for the proof end, the current proof (up to and including -the match of @samp{@code{proof-script-definition-end-regexp}}) is considered -to be not opaque and not omitted, thus all these proof commands -_are_ sent to the proof assistant. +forward for the proof end or if +@samp{@code{proof-script-cmd-prevents-proof-omission}} recognizes a proof +command that prevents proof omission then the current proof (up +to and including the match of +@samp{@code{proof-script-definition-end-regexp}} or +@samp{@code{proof-script-proof-end-regexp}}) is considered to be not opaque +and not omitted, thus all these proof commands _are_ sent to the +proof assistant. The feature does not work for nested proofs. If a match for @samp{@code{proof-script-proof-start-regexp}} is found before the next match diff --git a/generic/proof-config.el b/generic/proof-config.el index 506a0e1fb..81b24cb68 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -715,10 +715,14 @@ match of `proof-script-proof-end-regexp', are omitted (not send to the proof assistant) and replaced by `proof-script-proof-admit-command'. If a match for `proof-script-definition-end-regexp' is found while searching -forward for the proof end, the current proof (up to and including -the match of `proof-script-definition-end-regexp') is considered -to be not opaque and not omitted, thus all these proof commands -_are_ sent to the proof assistant. +forward for the proof end or if +`proof-script-cmd-prevents-proof-omission' recognizes a proof +command that prevents proof omission then the current proof (up +to and including the match of +`proof-script-definition-end-regexp' or +`proof-script-proof-end-regexp') is considered to be not opaque +and not omitted, thus all these proof commands _are_ sent to the +proof assistant. The feature does not work for nested proofs. If a match for `proof-script-proof-start-regexp' is found before the next match @@ -759,6 +763,18 @@ See `proof-omit-proofs-configured'." :type 'string :group 'proof-script) +(defcustom proof-script-cmd-prevents-proof-omission nil + "Optional predicate recognizing proof commands that prevent proof omission. +If set, this option should contain a function that takes a proof +command (as string) as argument and returns t or nil. If set, the +function is called on every proof command inside a proof while +scanning for proofs to omit. The predicate should return t if the +command has effects ouside the proof, potentially breaking the +script if the current proof is omitted. If the predicate returns +t, the proof is considered to be not opaque and thus not omitted." + :type 'function + :group 'proof-script) + ;; ;; Proof script indentation diff --git a/generic/proof-script.el b/generic/proof-script.el index be884c115..20f47caf5 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2028,6 +2028,8 @@ start is found inside a proof." maybe-result inside-proof proof-start-span-start proof-start-span-end + ;; t if the proof contains state changing commands and must be kept + proof-must-be-kept ;; the current vanilla item item ;; the command of the current item @@ -2061,7 +2063,12 @@ start is found inside a proof." (line-number-at-pos (span-end (car item)))))) ;; else - no nested proof, but still inside-proof - (if (string-match proof-script-proof-end-regexp cmd) + (if (and (string-match proof-script-proof-end-regexp cmd) + (not proof-must-be-kept)) + ;; End of opaque proof recognized and we didn't + ;; 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. @@ -2102,15 +2109,27 @@ start is found inside a proof." (setq inside-proof nil)) ;; else - no nested proof, no opaque proof, but still inside - (if (string-match proof-script-definition-end-regexp cmd) + (if (or (string-match proof-script-definition-end-regexp cmd) + (and (string-match proof-script-proof-end-regexp cmd) + proof-must-be-kept)) ;; A proof ending in Defined or something similar. + ;; Or a proof containing a state changing command + ;; 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))) (setq maybe-result nil) (setq inside-proof nil)) - ;; normal proof command - maybe it belongs to a + + ;; else - inside proof, no proof termination recognized + ;; Normal proof command - maybe it belongs to a ;; Defined, keep it separate, until we know. + (when (and proof-script-cmd-prevents-proof-omission + (not (eq (span-property (car item) 'type) 'comment)) + (not proof-must-be-kept) + (funcall proof-script-cmd-prevents-proof-omission + cmd)) + (setq proof-must-be-kept t)) (push item maybe-result))))) ;; else - outside proof @@ -2121,7 +2140,8 @@ start is found inside a proof." (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)) + (setq inside-proof t) + (setq proof-must-be-kept nil)) ;; outside, no proof start - keep it unmodified (push item result))) (setq vanillas (cdr vanillas)))