From 3cf052e7783ca81d9545ffbdc08427a5204f2d0b Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 26 Mar 2023 12:20:12 +0200 Subject: [PATCH] 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/omit_test.v | 10 +++++++++- ci/simple-tests/test-omit-proofs.el | 18 ++++++++++++------ 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/omit_test.v b/ci/simple-tests/omit_test.v index f0382c5e3..d99120785 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 using. - (* 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/ci/simple-tests/test-omit-proofs.el b/ci/simple-tests/test-omit-proofs.el index 2204d0e91..d676ab34b 100644 --- a/ci/simple-tests/test-omit-proofs.el +++ b/ci/simple-tests/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/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)))