From 20e0a93ff8e43db87116ee5bf97d9423760d64f1 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 26 Mar 2023 12:20:12 +0200 Subject: [PATCH 1/2] 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 | 18 ++++++++++++------ ci/simple-tests/omit_test.v | 10 +++++++++- coq/coq-syntax.el | 9 +++++++++ coq/coq.el | 3 ++- generic/proof-config.el | 18 +++++++++++++++++- generic/proof-script.el | 22 ++++++++++++++++++---- 6 files changed, 67 insertions(+), 13 deletions(-) diff --git a/ci/simple-tests/coq-test-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el index 2204d0e91..d676ab34b 100644 --- a/ci/simple-tests/coq-test-omit-proofs.el +++ b/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))) diff --git a/ci/simple-tests/omit_test.v b/ci/simple-tests/omit_test.v index 53ccfbd3a..97e43fcd4 100644 --- a/ci/simple-tests/omit_test.v +++ b/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. diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 9071ffa4b..03b3f9089 100644 --- a/coq/coq-syntax.el +++ b/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 =) diff --git a/coq/coq.el b/coq/coq.el index 127f77800..54ae01ad0 100644 --- a/coq/coq.el +++ b/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) diff --git a/generic/proof-config.el b/generic/proof-config.el index 81b24cb68..39436918a 100644 --- a/generic/proof-config.el +++ b/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 diff --git a/generic/proof-script.el b/generic/proof-script.el index 20f47caf5..854bd6bf8 100644 --- a/generic/proof-script.el +++ b/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))) From ac6f65c96f71ef6c264334f1db3ea0306a0abe71 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 26 Mar 2023 19:42:18 +0200 Subject: [PATCH 2/2] 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