branch: elpa/proof-general
commit b494b8ee5b2ed377dbfe28536980d975fbda55cb
Author: Hendrik Tews <[email protected]>
Commit: hendriktews <[email protected]>
CI test-goals-present: two more tests for resetting the goals buffer
- goals should be reset when there are no more goals (does work)
- goals should be reset after Qed (does not work)
---
ci/simple-tests/coq-test-goals-present.el | 121 +++++++++++++++++++++---------
1 file changed, 87 insertions(+), 34 deletions(-)
diff --git a/ci/simple-tests/coq-test-goals-present.el
b/ci/simple-tests/coq-test-goals-present.el
index e0784f1bac..3de11f8ac7 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -67,13 +67,33 @@ Proof using.
"Coq source code for checking goals after an error.")
(defconst coq-src-admitted
- "Lemma a : forall(P27X : Prop), P27X.
+ "Lemma a : forall(P : Prop), P.
Proof using.
- intros P27X.
+ intros P.
Admitted.
"
"Coq source for checking that the goals buffer is reset after Admitted.")
+(defconst coq-src-no-more-goals
+ "
+Lemma a : 1 + 1 = 2.
+Proof using.
+ simpl.
+ auto.
+"
+ "Coq source code for checking that the goals buffer is reset when
+no goals are left.")
+
+(defconst coq-src-qed
+ "
+Lemma a : 1 + 1 = 2.
+Proof using.
+ simpl.
+ auto.
+Qed.
+"
+ "Coq source code for checking that the goals buffer is reset after Qed.")
+
(defconst coq-src-update-goal-after-error
"
(* code taken from pull request #429 *)
@@ -149,6 +169,61 @@ goals buffer is not empty afterwards."
(set-buffer-modified-p nil))
(kill-buffer buffer)))))
+(defun goals-buffer-should-be-empty (pos msg)
+ "Check that `*goals*' is empty after asserting/retracting to POS.
+MSG is only used in a message, it should tell after which action
+the goals buffer is expected to be empty."
+ (message "Check that goals buffer is empty after %s" msg)
+ (goto-char pos)
+ (proof-goto-point)
+ (wait-for-coq)
+ ;; (record-buffer-content "*coq*")
+ ;; (record-buffer-content "*goals*")
+
+ ;; check that the goals buffer is empty
+ (with-current-buffer "*goals*"
+ (should (equal (point-min) (point-max)))))
+
+(defun goals-buffer-should-get-reset (coq-src coq-stm msg)
+ "Check that the goals buffer is reset.
+Put the string COQ-SRC into a buffer and assert until the first
+occurrence of COQ-STM, which should be a regular expression. At
+this point the goals buffer needs to contain something. Then
+assert to the end of COQ-SRC and check that the goals buffer has
+been reset. MSG is used in messages only. It shouls say after
+which action the goals buffer should have been reset."
+ (message "Check that goals are reset after %s." msg)
+ (setq proof-three-window-enable nil)
+ (let (buffer)
+ (unwind-protect
+ (progn
+ (find-file "goals.v")
+ (setq buffer (current-buffer))
+ (insert coq-src)
+
+ ;; First fill the goals buffer by asserting until the line
+ ;; after the first occurrence of COQ-STM.
+
+ (goto-char (point-min))
+ (should (re-search-forward coq-stm nil t))
+ (forward-line 1)
+ (message "*goals* should be non-empty after asserting until after %s"
+ coq-stm)
+ (proof-goto-point)
+ (wait-for-coq)
+ ;; there should be something in the goals buffer now
+ (with-current-buffer "*goals*"
+ (should (not (equal (point-min) (point-max)))))
+
+ (goals-buffer-should-be-empty (point-max) msg))
+
+ ;; clean up
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil))
+ (kill-buffer buffer)))))
+
+
(ert-deftest goals-after-proof ()
"Test goals are present after ``Proof''."
:expected-result (if coq--post-v87 :failed :passed)
@@ -175,40 +250,18 @@ goals buffer is not empty afterwards."
(ert-deftest goals-reset-after-admitted ()
"The goals buffer is reset after an Admitted."
- (message
- "goals-reset-after-admitted: Check that goals are reset after Admitted.")
- (setq proof-three-window-enable nil)
- (let (buffer)
- (unwind-protect
- (progn
- (find-file "goals.v")
- (setq buffer (current-buffer))
- (insert coq-src-admitted)
-
- ;; Need to assert the Admitted alone, therefore first assert
- ;; until before the Admitted.
- (goto-char (point-min))
- (should (re-search-forward "intros P27X" nil t))
- (forward-line 1)
- (proof-goto-point)
- (wait-for-coq)
+ (goals-buffer-should-get-reset coq-src-admitted "intros P" "Admitted"))
- (forward-line 1)
- (proof-goto-point)
- (wait-for-coq)
- ;; (record-buffer-content "*coq*")
- ;; (record-buffer-content "*goals*")
+(ert-deftest goals-reset-no-more-goals ()
+ "The goals buffer is reset when there are no more goals."
+ (goals-buffer-should-get-reset coq-src-no-more-goals
+ "Lemma a" "no more goals"))
- ;; check that the old goal is not present in the goals buffer
- (with-current-buffer "*goals*"
- (goto-char (point-min))
- (should (not (re-search-forward "P27X" nil t)))))
-
- ;; clean up
- (when buffer
- (with-current-buffer buffer
- (set-buffer-modified-p nil))
- (kill-buffer buffer)))))
+(ert-deftest goals-reset-qed ()
+ :expected-result :failed
+ "The goals buffer is reset after Qed."
+ (goals-buffer-should-get-reset coq-src-qed
+ "Proof using" "Qed"))
(ert-deftest update-goals-after-error ()
"Test goals are updated after an error."
