doc: update documentation for recent omit-proofs changes

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

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