From cf80d2ca0b961b694f6277239eecde15bb935a25 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 26 Mar 2023 19:42:18 +0200 Subject: [PATCH] doc: update documentation for recent omit-proofs changes --- CHANGES | 8 +++++ doc/PG-adapting.texi | 44 ++++++++++++++++++++++++++ doc/ProofGeneral.texi | 73 ++++++++++++++++++++++++++++++++++--------- 3 files changed, 111 insertions(+), 14 deletions(-) diff --git a/CHANGES b/CHANGES index 0f2590b5d..b84ed4606 100644 --- a/CHANGES +++ b/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 diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index f04022d6f..54d834c73 100644 --- a/doc/PG-adapting.texi +++ b/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 diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index d3a28b069..6ddf7638a 100644 --- a/doc/ProofGeneral.texi +++ b/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