Omit let fix

CHANGES

@@ -5,6 +5,10 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
 
 * Changes of Proof General 4.6 from Proof General 4.5
 
+** Generic changes
+*** Improve the omit-proofs feature to handle a number of cases where
+    proofs must not be omitted.
+
 ** Coq changes
 
 *** support Coq 8.19
@@ -14,6 +18,10 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
      is +module-not-found to let Proof General reliably detect missing
      modules as coqdep error.
 
+**** 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
 
 ** Generic changes

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)
 

doc/PG-adapting.texi

@@ -1164,6 +1164,21 @@ proofs are not nested. If a nested proof is found, a warning is
 displayed and omitting proofs stops at that location for the
 currently asserted region.
 
+In Coq, commands with non-local effects, such as @code{Hint}, may
+appear inside proofs. Additionally, admitting a proof of a @code{Let}
+declaration causes a warning in Coq. To treat such cases, the
+predicate @code{proof-script-cmd-prevents-proof-omission} is applied
+to all commands inside proofs and the regular expression
+@code{proof-script-cmd-force-next-proof-kept} is matched against all
+commands outside proofs. In case of a hit, the current or,
+respectively, the next proof is treated as non-opaque and is not
+omitted. Note that a match of
+@code{proof-script-cmd-force-next-proof-kept} is only handled if the
+matching command and the following proof appear in the same asserted
+region. If the proof is asserted separately, the information about the
+match in the previously asserted region is lost and the proof may thus
+be omitted.
+
 To enable the omit proofs feature, the following settings must be
 configured.
 
@@ -1231,6 +1246,35 @@ See @samp{@code{proof-omit-proofs-configured}}.
 @defvar proof-script-proof-admit-command 
 Proof command to be inserted instead of omitted proofs.
 @end defvar
+
+@c TEXI DOCSTRING MAGIC: proof-script-cmd-prevents-proof-omission
+@defvar proof-script-cmd-prevents-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
+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.
+@end defvar
+
+@c TEXI DOCSTRING MAGIC: proof-script-cmd-force-next-proof-kept
+@defvar proof-script-cmd-force-next-proof-kept 
+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 @samp{@code{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.
+@end defvar
+
 @node Safe (state-preserving) commands
 @section Safe (state-preserving) commands
 

doc/ProofGeneral.texi

@@ -1527,16 +1527,31 @@ omit complete opaque proofs when larger chunks are asserted. A
 proof is opaque, if its proof script or proof term cannot
 influence the following code. In Coq, opaque proofs are finished
 with @code{Qed}, non-opaque ones with @code{Defined}. When this
-omit proofs feature is configured, complete opaque proofs are
-silently replace with a suitable cheating command
+omit-proofs feature is configured, complete opaque proofs are
+silently replaced with a suitable cheating command
 (@code{Admitted} for Coq) before sending the proof to the proof
 assistant. For files with big proofs this can bring down the
 processing time to 10% with the obvious disadvantage that errors
-in the omitted proofs go unnoticed. For checking the proofs
-occasionally, a prefix argument for @code{proof-goto-point} and
-@code{proof-process-buffer} causes these commands to disregard
-the setting of @code{proof-omit-proofs-option}. Currently, the
-omit proofs feature is only supported for Coq.
+in the omitted proofs go unnoticed. Currently, the omit-proofs
+feature is only supported for Coq.
+
+A prefix argument for @code{proof-goto-point} and
+@code{proof-process-buffer} toggles the omit-proofs feature
+temporarily for this invocation. That is, if
+@code{proof-omit-proofs-option} has been set to @code{t}, a prefix
+argument switches the omit-proofs feature off for these commands. Vice
+versa, if @code{proof-omit-proofs-option} is @code{nil}, a prefix
+argument switches the omit-proofs feature temporarily on for one
+invocation.
+
+Note that the omit-proof feature works by examining the asserted
+region with different regular expressions to recognize proofs and to
+differentiate opaque from non-opaque proofs. This approach is
+necessarily imprecise and it may happen that certain non-opaque proofs
+are classified as opaque ones, thus being omitted and that the proof
+script therefore fails unexpectedly at a later point. Therefore, if a
+proof script fails unexpectedly try processing it again after
+disabling the omit-proofs feature.
 @item
 An often used poor man's solution is to collect all new material
 at the end of one file, regardless where the material really
@@ -5080,10 +5095,13 @@ General will perform some unnecessary compilations.
 @section Omitting proofs for speed
 @cindex Omitting proofs for speed
 
-To speed up asserting larger chunks, Proof General can omit
-complete opaque proofs by silently replacing the whole proof
-script with @code{Admitted}, @ref{Script processing commands}.
-This works when
+To speed up asserting larger chunks, Proof General can omit complete
+opaque proofs by silently replacing the whole proof script with
+@code{Admitted}, @ref{Script processing commands}. For files with big
+proofs this can bring down the processing time to 10% with the obvious
+disadvantage that errors in the omitted proofs go unnoticed.
+
+The omit-proof feature works when
 @itemize
 @item
 proofs are not nested
@@ -5103,9 +5121,8 @@ To enable omitting proofs, configure
 @code{proof-omit-proofs-option} or select @code{Proof-General ->
 Quick Options -> Processing -> Omit Proofs}.
 
-With a prefix argument, both @code{proof-goto-point} and
-@code{proof-process-buffer} will temporarily disable the omit
-proofs feature and send the full proof script to Coq.
+For both, @code{proof-goto-point} and @code{proof-process-buffer}, a
+prefix argument toggles the omit-proofs feature for one invocation.
 
 If a nested proof is detected while searching for opaque proofs
 to omit, a warning is displayed and the complete remainder of the
@@ -5122,6 +5139,34 @@ form being e.g. @code{Proof using Type} if no section hypothesis is
 used), see the menu command @code{Coq > "Proof using" mode} and
 @ref{Proof using annotations} for details.
 
+Note that the omit-proof feature works by examining the asserted
+region with different regular expressions to recognize proofs and to
+differentiate opaque from non-opaque proofs. This approach is
+necessarily imprecise and the omit-proofs feature may therefore cause
+unexpected errors in the proof script. Currently, Proof General
+correctly handles the following cases for Coq.
+@itemize
+@item
+Commands, such as @code{Hint}, that may appear inside proofs but may
+have effects outside the proof cause the proof to be considered as
+non-opaque.
+@item
+A @code{Let} declaration followed by a proof to supply the term causes
+this proof to be considered as non-opaque. Note that such declarations
+are only handled correctly if the @code{Let} and the proof are
+asserted together. If the proof is asserted separately it may be
+treated as opaque and thus be omitted.
+@end itemize
+
+The following cases are currently not handled correctly.
+@itemize
+@item
+All capitalized commands make Proof General believe the proof is
+non-opaque, even if they have proof-local effect only, such as
+@code{Focus} or @code{Unshelve}.
+@end itemize
+
+
 @node Editing multiple proofs
 @section Editing multiple proofs
 

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