From f5cde4424f4e31a24eae818e1a7029075955c46a Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 11 Jun 2024 16:44:30 +0200 Subject: [PATCH] omit-proofs tests: add new test for bullets and braces Currently bullets and braces are classified as commands that prevent proof omission, therefore proofs containing bullets or braces are never omitted. The new tests is therefore expected to fail. --- ci/simple-tests/coq-test-omit-proofs.el | 50 ++++++++++++++++++------- ci/simple-tests/omit_test.v | 24 ++++++++++-- 2 files changed, 56 insertions(+), 18 deletions(-) diff --git a/ci/simple-tests/coq-test-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el index ed7aea8d5..68dcf21e3 100644 --- a/ci/simple-tests/coq-test-omit-proofs.el +++ b/ci/simple-tests/coq-test-omit-proofs.el @@ -106,7 +106,7 @@ In particular, test that with proof-omit-proofs-option configured: ;; Check 1: check that the proof is valid and omit can be disabled (message "1: check that the proof is valid and omit can be disabled") - (should (search-forward "automatic test marker 4" nil t)) + (should (search-forward "automatic test marker 4 " nil t)) (forward-line -1) ;; simulate C-u prefix argument (proof-goto-point '(4)) @@ -140,19 +140,19 @@ In particular, test that with proof-omit-proofs-option configured: ;; Check 2: check proof-locked-face is active at marker 2 and 3 (message "2: check proof-locked-face is active at marker 2 and 3") - (should (search-backward "automatic test marker 2" nil t)) + (should (search-backward "automatic test marker 2 " nil t)) (should (eq (first-overlay-face) 'proof-locked-face)) - (should (search-forward "automatic test marker 3" nil t)) + (should (search-forward "automatic test marker 3 " nil t)) (should (eq (first-overlay-face) 'proof-locked-face)) ;; Check 3: check that the second proof is omitted (message "3: check that the second proof is omitted") ;; first retract - (should (search-backward "automatic test marker 1" nil t)) + (should (search-backward "automatic test marker 1 " nil t)) (proof-goto-point) (wait-for-coq) ;; move forward again - (should (search-forward "automatic test marker 4" nil t)) + (should (search-forward "automatic test marker 4 " nil t)) (forward-line -1) (proof-goto-point) (wait-for-coq) @@ -174,7 +174,7 @@ In particular, test that with proof-omit-proofs-option configured: ;; Check 4: check proof-omitted-proof-face is active at marker 3 (message "4: check proof-omitted-proof-face is active at marker 3") - (should (search-backward "automatic test marker 3" nil t)) + (should (search-backward "automatic test marker 3 " nil t)) ;; debug overlay order ;; (mapc ;; (lambda (ov) @@ -185,9 +185,9 @@ In particular, test that with proof-omit-proofs-option configured: ;; Check 5: check proof-locked-face is active at marker 1 and 2 (message "5: check proof-locked-face is active at marker 1 and 2") - (should (search-backward "automatic test marker 1" nil t)) + (should (search-backward "automatic test marker 1 " nil t)) (should (eq (first-overlay-face) 'proof-locked-face)) - (should (search-forward "automatic test marker 2" nil t)) + (should (search-forward "automatic test marker 2 " nil t)) (should (eq (first-overlay-face) 'proof-locked-face)) ;; Check 6: check that a partial proof at the end is not omitted @@ -195,7 +195,7 @@ In particular, test that with proof-omit-proofs-option configured: (goto-char (point-min)) (proof-goto-point) (wait-for-coq) - (should (search-forward "automatic test marker 3" nil t)) + (should (search-forward "automatic test marker 3 " nil t)) (forward-line 2) (proof-goto-point) (wait-for-coq) @@ -223,11 +223,11 @@ The sources for the test contain a local attribute in form of (goto-char (point-min)) ;; Check that proofs with Hint commands are never omitted (message "Check that proofs with Hint commands are never omitted") - (should (search-forward "automatic test marker 6" nil t)) + (should (search-forward "automatic test marker 6 " nil t)) (forward-line -1) (proof-goto-point) (wait-for-coq) - (should (search-backward "automatic test marker 5" nil t)) + (should (search-backward "automatic test marker 5 " nil t)) (should (eq (first-overlay-face) 'proof-locked-face))) @@ -245,14 +245,36 @@ This test only checks the faces in the middle of the proof." (goto-char (point-min)) ;; Check that proofs for Let local declarations are never omitted. (message "Check that proofs for Let local declarations are never omitted.") - (should (search-forward "automatic test marker 8" nil t)) + (should (search-forward "automatic test marker 8 " nil t)) (forward-line -1) (proof-goto-point) (wait-for-coq) - (should (search-backward "automatic test marker 7-1" nil t)) + (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 (search-forward "automatic test marker 7-2 " nil t)) (should (eq (first-overlay-face) 'proof-omitted-proof-face))) + +(ert-deftest omit-proofs-omit-bullets-and-braces () + :expected-result :failed + (let ((proof-omit-proofs-option t) + pos-10) + (message "omit-proofs-omit-bullets-and-braces: Check bullets and braces") + (reset-coq) + (find-file "omit_test.v") + (goto-char (point-min)) + ;; Check that proofs with bullets and braces are omitted + (message "Check that proofs with bullets and braces are omitted") + (should (search-forward "automatic test marker 10 " nil t)) + (setq pos-10 (point)) + (forward-line 1) + (proof-goto-point) + (wait-for-coq) + (goto-char pos-10) + ;; Comment behind should be locked + (should (eq (first-overlay-face) 'proof-locked-face)) + ;; Proof with bullets and braces should be omitted + (should (search-backward "automatic test marker 9 " 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 97e43fcd4..7082067bf 100644 --- a/ci/simple-tests/omit_test.v +++ b/ci/simple-tests/omit_test.v @@ -8,14 +8,17 @@ * * Lemma never_omit_hints is for test omit-proofs-never-omit-hints: Proofs * containing commands should never be skipped (except for a few white-listed - * commands. + * commands). * - * Lemma never_omit_let is for test omit-proofs-never-omit-lets: Proofs of - * let-theorems should never be omitted. + * Lemma never_omit_let and behind_let is for test + * omit-proofs-never-omit-lets: Proofs of let-theorems should never be + * omitted while proofs behind let declarations should. * + * Lemma omit_bullets_and_braces is for test + * omit-proofs-omit-bullets-and-braces: Proofs with bullets and braces + * should be omitted. *) - Definition classical_logic : Prop := forall(P : Prop), ~~P -> P. (* automatic test marker 1 *) @@ -70,3 +73,16 @@ Proof using. Qed. (* automatic test marker 6 *) + +Lemma omit_bullets_and_braces : True /\ (True /\ True). +Proof using. + split. + - trivial. + - { split. + ++ trivial. + (* automatic test marker 9 *) + ++ trivial. + } +Qed. + +(* automatic test marker 10 *)