omit-proofs: handle commands that may have global effects

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'.

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 =)

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)
 

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

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

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)))