From d0a9533c03909e50aba40f2e56915c3c6b983e6c Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Sun, 5 Mar 2023 20:48:31 +0100
Subject: [PATCH] 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 b8d177cc0..417e23951 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 edc8491b9..45a99ffb5 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)))