Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

coq: run silently and explicitly Show when necessary #742

Closed
wants to merge 5 commits into from
Closed

coq: run silently and explicitly Show when necessary #742

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
b984de6
coq: run silently and explicitly Show when necessary
hendriktews Mar 2, 2024
2d307a6
fix tests for preceding commit
hendriktews Mar 3, 2024
1414157
CI test-goals-present: two more tests for resetting the goals buffer
hendriktews Mar 8, 2024
fb442fd
CI: extend goals present tests to check for errors if applicable
hendriktews Apr 7, 2024
0b42f93
coq: fix goals update after error
hendriktews Apr 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions ci/coq-tests.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -196,6 +196,8 @@ For example, COMMENT could be (*test-definition*)"


(ert-deftest 020_coq-test-definition ()
;; There are no infomsgr when running silent.
:expected-result :failed
"Test *response* output after asserting a Definition."
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
Expand Down Expand Up @@ -317,6 +319,10 @@ For example, COMMENT could be (*test-definition*)"


(ert-deftest 090_coq-test-regression-Fail()
;; When running silent, the message about indeed failing is not
;; shown. One might fix this test by checking that there is no
;; error, which would be shown without Fail.
:expected-result :failed
"Test for Fail"
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
Expand All @@ -338,6 +344,13 @@ Tactic failure: Cannot solve this goal." "*coq*")))))
;; (coq-should-buffer-regexp (regexp-quote "The command has indeed failed with message: Tactic failure: Cannot solve this goal.") "*response*")

(ert-deftest 091_coq-test-regression-Fail()
;; XXX What is the difference between this test and
;; 090_coq-test-regression-Fail?

;; When running silent, the message about indeed failing is not
;; shown. One might fix this test by checking that there is no
;; error, which would be shown without Fail.
:expected-result :failed
"Test for Fail"
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
Expand Down
162 changes: 114 additions & 48 deletions ci/simple-tests/coq-test-goals-present.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -121,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)
Expand All @@ -141,78 +163,114 @@ 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
(with-current-buffer buffer
(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)
(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 ()
:expected-result :failed
"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
"Proof using" "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."
:expected-result :failed
(message "update-goals-after-error: Check goals are updated after error")
(setq proof-three-window-enable nil)
(let (buffer)
Expand All @@ -230,6 +288,7 @@ goals buffer is not empty afterwards."
;; (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)))
Expand All @@ -242,9 +301,16 @@ goals buffer is not empty afterwards."
;; (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))
Expand Down
Loading
Loading