[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 360dc8cf4e 2/2: test-omit-proofs: add tests
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/proof-general 360dc8cf4e 2/2: test-omit-proofs: add tests for #688 and #687 |
Date: |
Fri, 17 Mar 2023 17:02:13 -0400 (EDT) |
branch: elpa/proof-general
commit 360dc8cf4e3e5993310b43e0bcdf91a8b22bd681
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>
test-omit-proofs: add tests for #688 and #687
---
ci/simple-tests/omit_test.v | 38 +++++++++++++++++++++++++++
ci/simple-tests/test-omit-proofs.el | 52 +++++++++++++++++++++++++++++++++++++
2 files changed, 90 insertions(+)
diff --git a/ci/simple-tests/omit_test.v b/ci/simple-tests/omit_test.v
index b8d177cc08..417e239513 100644
--- a/ci/simple-tests/omit_test.v
+++ b/ci/simple-tests/omit_test.v
@@ -1,3 +1,20 @@
+(*
+ * Coq sources for test-omit-proofs.el
+ *
+ * Up to test marker 4 the sources are used for
+ * omit-proofs-omit-and-not-omit: The proof of the first lemma
+ * classic_excluded_middle should not be omitted, while the proof of the
+ * second classic_excluded_middle is.
+ *
+ * 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.
+ *
+ * Lemma never_omit_let is for test omit-proofs-never-omit-lets: Proofs of
+ * let-theorems should never be omitted.
+ *
+ *)
+
Definition classical_logic : Prop := forall(P : Prop), ~~P -> P.
@@ -23,3 +40,24 @@ Proof using.
Qed.
(* automatic test marker 4 *)
+
+Lemma never_omit_hints : 1 + 1 = 2.
+Proof using.
+ #[local] Hint Resolve classic_excluded_middle : core.
+ (* automatic test marker 5 *)
+ auto.
+Qed.
+
+(* automatic test marker 6 *)
+
+Section let_test.
+
+ Let never_omit_let : 1 + 1 = 2.
+ Proof using.
+ (* automatic test marker 7 *)
+ auto.
+ Qed.
+
+End let_test.
+
+(* automatic test marker 8 *)
diff --git a/ci/simple-tests/test-omit-proofs.el
b/ci/simple-tests/test-omit-proofs.el
index edc8491b9c..45a99ffb55 100644
--- a/ci/simple-tests/test-omit-proofs.el
+++ b/ci/simple-tests/test-omit-proofs.el
@@ -42,6 +42,17 @@ If so, return the first non-nil value returned by PRED."
;; to process.
(accept-process-output nil 0.1)))
+(defun reset-coq ()
+ "Reset Coq and Proof General.
+Do `proof-shell-exit' to kill Coq and reset the locked region and
+a lot of other internal state of Proof General. Used at the
+beginning of the test when several tests work on the same Coq
+source file."
+ (when (and (boundp 'proof-shell-buffer)
+ (buffer-live-p proof-shell-buffer))
+ (proof-shell-exit t)
+ (message "Coq and Proof General reseted")))
+
(defun overlay-less (a b)
"Compare two overlays.
Return t if overlay A has smaller size than overlay B and should
@@ -76,7 +87,9 @@ In particular, test that with proof-omit-proofs-option
configured:
- stuff before the proof still has normal color "
(setq proof-omit-proofs-option t
proof-three-window-enable nil)
+ (reset-coq)
(find-file "omit_test.v")
+ (goto-char (point-min))
;; 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")
@@ -152,3 +165,42 @@ In particular, test that with proof-omit-proofs-option
configured:
(should (eq (first-overlay-face) 'proof-locked-face))
(should (search-forward "automatic test marker 2" nil t))
(should (eq (first-overlay-face) 'proof-locked-face)))
+
+(ert-deftest omit-proofs-never-omit-hints ()
+ :expected-result :failed
+ "Test that proofs containing Hint are never omitted.
+This test only checks that the face in the middle of the proof is
+the normal `proof-locked-face'."
+ (setq proof-omit-proofs-option t
+ proof-three-window-enable nil)
+ (reset-coq)
+ (find-file "omit_test.v")
+ (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))
+ (forward-line -1)
+ (proof-goto-point)
+ (wait-for-coq)
+ (should (search-backward "automatic test marker 5" nil t))
+ (should (eq (first-overlay-face) 'proof-locked-face)))
+
+
+(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'."
+ (setq proof-omit-proofs-option t
+ proof-three-window-enable nil)
+ (reset-coq)
+ (find-file "omit_test.v")
+ (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))
+ (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)))