From fb442fd31a36385503c92b735c6bc2c61aa3f697 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sun, 7 Apr 2024 17:16:51 +0200 Subject: [PATCH] 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 e036bd969..98c8faf71 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 @@ -226,24 +235,24 @@ which action the goals buffer should have been reset." (ert-deftest goals-after-proof () "Test goals are present after ``Proof''." - (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." - (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''." - (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 () :expected-result :failed @@ -281,6 +290,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))) @@ -293,9 +303,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))