branch: elpa/proof-general
commit b777d3bf70de5af8489bb26fa6ff65ba7c98c469
Author: Hendrik Tews <hend...@askra.de>
Commit: hendriktews <hend...@askra.de>
CI: extend goals present tests to check for errors if applicable
Extend the goals present tests to additionally check that the response
buffer contains some text (i.e., an error message) in those cases
where an error is expected.
---
ci/simple-tests/coq-test-goals-present.el | 35 +++++++++++++++++++++++--------
1 file changed, 26 insertions(+), 9 deletions(-)
diff --git a/ci/simple-tests/coq-test-goals-present.el
b/ci/simple-tests/coq-test-goals-present.el
index 3de11f8ac7..86b1cc74f9 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -141,10 +141,12 @@ BUF should be a string."
;;; define the tests
-(defun goals-after-test (coq-src msg)
+(defun goals-after-test (coq-src msg check-response-nonempty)
"Test that Proof General shows goals after processing COQ-SRC.
Process COQ-SRC in a new buffer in one step and check that the
-goals buffer is not empty afterwards."
+goals buffer is not empty afterwards. If CHECK-RESPONSE-NONEMPTY
+is non-nil, additionally check that the response buffer is
+non-empty, i.e., shows some error message."
(message "goals-after-test: Check goals are present after %s." msg)
(setq proof-three-window-enable nil)
(let (buffer)
@@ -161,7 +163,14 @@ goals buffer is not empty afterwards."
;; check that there is a goal in the goals buffer
(with-current-buffer "*goals*"
(goto-char (point-min))
- (should (looking-at "1 \\(sub\\)?goal (ID"))))
+ (should (looking-at "1 \\(sub\\)?goal (ID")))
+
+ (when check-response-nonempty
+ (message
+ "goals-after-test: Check response buffer is nonempty after %s."
+ msg)
+ (with-current-buffer "*response*"
+ (should (not (equal (point-min) (point-max)))))))
;; clean up
(when buffer
@@ -227,26 +236,26 @@ which action the goals buffer should have been reset."
(ert-deftest goals-after-proof ()
"Test goals are present after ``Proof''."
:expected-result (if coq--post-v87 :failed :passed)
- (goals-after-test coq-src-proof "Proof"))
+ (goals-after-test coq-src-proof "Proof" nil))
(ert-deftest goals-after-comment ()
"Test goals are present after a comment."
:expected-result :failed
- (goals-after-test coq-src-comment "comment"))
+ (goals-after-test coq-src-comment "comment" nil))
(ert-deftest goals-after-auto ()
"Test goals are present after ``auto''."
:expected-result (if coq--post-v87 :failed :passed)
- (goals-after-test coq-src-auto "auto"))
+ (goals-after-test coq-src-auto "auto" nil))
(ert-deftest goals-after-simpl ()
"Test goals are present after ``simpl''."
- (goals-after-test coq-src-simpl "simpl"))
+ (goals-after-test coq-src-simpl "simpl" nil))
(ert-deftest goals-after-error ()
"Test goals are present after an error."
:expected-result :failed
- (goals-after-test coq-src-error "error"))
+ (goals-after-test coq-src-error "error" t))
(ert-deftest goals-reset-after-admitted ()
"The goals buffer is reset after an Admitted."
@@ -283,6 +292,7 @@ which action the goals buffer should have been reset."
;; (record-buffer-content "*goals*")
;; the complete goal should be present
+ (message "Check that the complete goal is present in *goals*")
(with-current-buffer "*goals*"
(goto-char (point-min))
(should (re-search-forward "(eq_one 1 -> False) -> False" nil t)))
@@ -295,9 +305,16 @@ which action the goals buffer should have been reset."
;; (record-buffer-content "*goals*")
;; the hypothesis H should be present
+ (message "Check that the goals buffer has been updated")
(with-current-buffer "*goals*"
(goto-char (point-min))
- (should (re-search-forward "H : eq_one 1 -> False" nil t))))
+ (should (re-search-forward "H : eq_one 1 -> False" nil t)))
+
+ ;; some error should be in the response buffer
+ (message "Check that there is some error message present")
+ (with-current-buffer "*response*"
+ (should (not (equal (point-min) (point-max))))))
+
(when buffer
(with-current-buffer buffer
(set-buffer-modified-p nil))
