omit-proofs: handle Let declarations

Add support for recognizing proof-script commands that prevent the
omission of proofs that follow them directly, such as a Let
declaration with a proof script in Coq.

Fixes #687

ci/simple-tests/coq-test-omit-proofs.el

@@ -201,10 +201,11 @@ The sources for the test contain a local attribute in form of
 
 
 (ert-deftest omit-proofs-never-omit-lets ()
-  :expected-result :failed
-  "Test that proofs for Let local declarations are never omitted.
-This test only checks that the face in the middle of the proof is
-the normal `proof-locked-face'."
+  "Test for Let and proof omission.
+Test that proofs for Let local declarations are never omitted and
+that proofs of theorems following a Let definition are omitted.
+
+This test only checks the faces in the middle of the proof."
   (setq proof-omit-proofs-option t
         proof-three-window-enable nil)
   (reset-coq)
@@ -216,5 +217,10 @@ the normal `proof-locked-face'."
   (forward-line -1)
   (proof-goto-point)
   (wait-for-coq)
-  (should (search-backward "automatic test marker 7" nil t))
-  (should (eq (first-overlay-face) 'proof-locked-face)))
+  (should (search-backward "automatic test marker 7-1" nil t))
+  (should (eq (first-overlay-face) 'proof-locked-face))
+
+  ;; Check that theorems behind Let definitions are omitted.
+  (message "Check that theorems behind Let definitions are omitted.")
+  (should (search-forward "automatic test marker 7-2" nil t))
+  (should (eq (first-overlay-face) 'proof-omitted-proof-face)))

ci/simple-tests/omit_test.v

@@ -44,8 +44,16 @@ Qed.
 Section let_test.
 
   Let never_omit_let : 1 + 1 = 2.
+  (* some comment between let and proof start *)
   Proof.
-    (* automatic test marker 7 *)
+    (* automatic test marker 7-1 *)
+    auto.
+  Qed.
+
+  Let two : nat := 2.
+  Lemma behind_let : 1 + 1 = 2.
+  Proof using.
+    (* automatic test marker 7-2 *)
     auto.
   Qed.
 

coq/coq-syntax.el

@@ -1433,6 +1433,15 @@ different."
 Used in `coq-cmd-prevents-proof-omission' to identify tactics
 that only have proof-local effects.")
 
+(defcustom coq-cmd-force-next-proof-kept "Let"
+  "Instantiating for `proof-script-cmd-force-next-proof-kept'.
+Regular expression for commands that prevent omitting the next
+proof. A Let declaration with an admitted proof yields a warning,
+see Proof General issue #687 and Coq issue #17199. Therefore,
+proofs for a Let declaration should not be omitted."
+  :type 'regexp
+  :group 'coq)
+
 ;; must match:
 ;; "with f x y :" (followed by = or not)
 ;; "with f x y (z:" (not followed by =)

coq/coq.el

@@ -1967,7 +1967,8 @@ at `proof-assistant-settings-cmds' evaluation time.")
    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-cmd-prevents-proof-omission #'coq-cmd-prevents-proof-omission)
+   proof-script-cmd-prevents-proof-omission #'coq-cmd-prevents-proof-omission
+   proof-script-cmd-force-next-proof-kept coq-cmd-force-next-proof-kept)
 
   (setq proof-cannot-reopen-processed-files nil)
 

generic/proof-config.el

@@ -764,7 +764,7 @@ See `proof-omit-proofs-configured'."
   :group 'proof-script)
 
 (defcustom proof-script-cmd-prevents-proof-omission nil
-  "Optional predicate recognizing proof commands that prevent proof omission.
+  "Optional predicate to match commands that prevent omitting the current proof.
 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
@@ -775,6 +775,22 @@ t, the proof is considered to be not opaque and thus not omitted."
   :type 'function
   :group 'proof-script)
 
+(defcustom proof-script-cmd-force-next-proof-kept nil
+  "Optional regexp for commands that prevent omitting the next proof.
+If set, this option should contain a regular expression that
+matches proof-script commands that prevent the omission of proofs
+dirctly following this command. When scanning the newly asserted
+region for proofs to omit, every proof-script command outside
+proofs is matched against this regexp. If it matches and the next
+command matches `proof-script-proof-start-regexp' this following
+proof will not be omitted.
+
+Note that recognition of commands with this regular expression
+does only work if the command and the following proof are
+asserted together."
+  :type 'regexp
+  :group 'proof-script)
+
 
 ;;
 ;; Proof script indentation

generic/proof-script.el

@@ -2030,6 +2030,8 @@ start is found inside a 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
+        ;; t if there was a command forcing the next proof to be kept
+        next-proof-must-be-kept
         ;; the current vanilla item
         item
         ;; the command of the current item
@@ -2122,14 +2124,16 @@ start is found inside a proof."
                       (setq inside-proof nil))
 
                   ;; else - inside proof, no proof termination recognized
-                  ;; Normal proof command - maybe it belongs to a
-                  ;; Defined, keep it separate, until we know.
+                  ;; Check if current command prevents this proof to
+                  ;; be omitted.
                   (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))
+                  ;; Normal proof command - maybe it belongs to a
+                  ;; Defined, keep it separate, until we know.
                   (push item maybe-result)))))
 
         ;; else - outside proof
@@ -2141,8 +2145,18 @@ start is found inside a proof."
               (setq proof-start-span-start (span-start (car item)))
               (setq proof-start-span-end (span-end (car item)))
               (setq inside-proof t)
-              (setq proof-must-be-kept nil))
-          ;; outside, no proof start - keep it unmodified
+              (setq proof-must-be-kept next-proof-must-be-kept)
+              (setq next-proof-must-be-kept nil))
+
+          ;; outside, no proof start
+          ;; check if current item prevents omitting the next proof
+          (when (and proof-script-cmd-force-next-proof-kept
+                     (not (eq (span-property (car item) 'type) 'comment)))
+            (if (proof-string-match proof-script-cmd-force-next-proof-kept cmd)
+                (setq next-proof-must-be-kept t)
+              (setq next-proof-must-be-kept nil)))
+
+          ;; keep current item unmodified
           (push item result)))
       (setq vanillas (cdr vanillas)))