Skip to content

Commit

Permalink
Minor changes
Browse files Browse the repository at this point in the history
  • Loading branch information
@CyrilAnac
CyrilAnac committed May 29, 2020
1 parent cc4b4f6 commit 77fd293
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 36 deletions.
60 changes: 31 additions & 29 deletions ci/coq-tests.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,11 +112,9 @@

(defun coq-set-flags (val flags)
(when (member 'show-proof-stepwise flags) (setq coq-show-proof-stepwise val))
(when (member 'diffs-on flags) (if val (setq coq-diffs 'on) (setq coq-diffs 'off)))
)
(when (member 'diffs-on flags) (if val (setq coq-diffs 'on) (setq coq-diffs 'off))))


(defun coq-fixture-on-file (file body &rest flags)
(defun coq-fixture-on-file (file body &rest flags)
"Fixture to setup the test env: open FILE if non-nil, or a temp file
then evaluate the BODY function and finally tear-down (exit Coq)."
;; AVOID THE FOLLOWING ERROR:
Expand Down Expand Up @@ -167,24 +165,28 @@ For example, COMMENT could be (*test-definition*)"
(goto-char (point-min))
(search-forward comment))

(defun coq-should-response (message)
(should (equal message
(defun coq-should-response (str)
(should (equal str
(string-trim
(with-current-buffer "*response*"
(buffer-substring-no-properties (point-min) (point-max)))))))

(defun coq-should-buffer (message)
(should (string-match-p message
(defun coq-should-buffer-regexp (regexp)
(should (string-match-p regexp
(string-trim
(with-current-buffer "*coq*"
(buffer-substring-no-properties (point-min) (point-max)))))))

(defun coq-should-buffer-string (str)
"Particular case of `coq-should-buffer-regexp'."
(coq-should-buffer-regexp (regexp-quote str)))

;; TODO: Use https://github.com/rejeep/ert-async.el
;; and/or ERT https://www.gnu.org/software/emacs/manual/html_node/ert/index.html

(ert-deftest 010_coq-test-running ()
"Test that the coqtop process is started properly."
(coq-fixture-on-file nil
(coq-fixture-on-file nil
(lambda ()
(coq-test-cmd "Print 0.")
;; (should (process-list)) ; wouldn't be a strong enough assert.
Expand All @@ -193,8 +195,8 @@ For example, COMMENT could be (*test-definition*)"

(ert-deftest 020_coq-test-definition ()
"Test *response* output after asserting a Definition."
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(lambda ()
(coq-test-goto-before "(*test-definition*)")
(proof-goto-point)
Expand All @@ -203,9 +205,9 @@ For example, COMMENT could be (*test-definition*)"


(ert-deftest 021_coq-test-regression-goto-point ()
"Regression test for proof-goto-point after a comment, PR #90"
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
"Regression test for proof-goto-point after a comment, PR #490"
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(lambda ()
(coq-test-goto-after "(*test-definition*)")
(proof-goto-point)
Expand All @@ -215,8 +217,8 @@ For example, COMMENT could be (*test-definition*)"

(ert-deftest 030_coq-test-position ()
"Test locked region after Qed."
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(lambda ()
(coq-test-goto-before " (*test-lemma*)")
(let ((proof-point (point)))
Expand All @@ -227,8 +229,8 @@ For example, COMMENT could be (*test-definition*)"

(ert-deftest 040_coq-test-insert ()
"Test retract on insert from Qed."
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(lambda ()
(coq-test-goto-before " (*test-lemma*)")
(proof-goto-point)
Expand All @@ -243,8 +245,8 @@ For example, COMMENT could be (*test-definition*)"

(ert-deftest 050_coq-test-lemma-false ()
"Test retract on proof error."
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(lambda ()
(coq-test-goto-before " (*test-lemma2*)")
(let ((proof-point (save-excursion (coq-test-goto-after "(*error*)"))))
Expand All @@ -269,8 +271,8 @@ For example, COMMENT could be (*test-definition*)"

(ert-deftest 070_coq-test-regression-wholefile-no-proof ()
"Regression test for no proof bug"
(coq-fixture-on-file
(coq-test-full-path "test_wholefile.v")
(coq-fixture-on-file
(coq-test-full-path "test_wholefile.v")
(lambda ()
(proof-process-buffer)
(proof-shell-wait)
Expand All @@ -280,28 +282,28 @@ For example, COMMENT could be (*test-definition*)"

(ert-deftest 080_coq-test-regression-show-proof-stepwise()
"Regression test for the \"Show Proof\" option"
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(lambda ()
(coq-test-goto-before " (*test-insert*)")
(proof-goto-point)
(proof-shell-wait)
(coq-should-response "(fun (A : Prop) (proof_of_A : A) => ?Goal)"))
(coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)"))
'show-proof-stepwise))


(ert-deftest 081_coq-test-regression-show-proof-diffs()
"Test for Show Proof Diffs"
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(lambda ()
(coq-test-goto-before " (*test-insert*)")
(proof-goto-point)
(proof-shell-wait)
;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show Proof."
(if (coq--post-v811)
(coq-should-buffer "<diff\\.added\\.bg>(fun <diff\\.added>(</diff\\.added>A : Prop<diff\\.added>) (proof_of_A : A)</diff\\.added> => \\?Goal)</diff\\.added\\.bg>")
(coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)")))
(coq-should-buffer-string "<diff.added.bg>(fun <diff.added>(</diff.added>A : Prop<diff.added>) (proof_of_A : A)</diff.added> => ?Goal)</diff.added.bg>")
(coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)")))
'show-proof-stepwise 'diffs-on))


Expand Down
7 changes: 0 additions & 7 deletions coq/coq.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1237,13 +1237,6 @@ should match the `coq-show-proof-diffs-regexp'."
;; the number of nested goals, then Unset Silent and Show the goal
(and (string-match-p "BackTo\\s-" cmd)
(> (length coq-last-but-one-proofstack) coq--retract-naborts)))
;; "Set Diffs" always re-prints the proof context with (if enabled) diffs
;; (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")
;; (when coq-show-proof-stepwise
;; (or
;; (when (eq coq-diffs 'off) "Show Proof.")
;; (when (eq coq-diffs 'on) "Show Proof Diffs.")
;; (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
(let ((showlist (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show."))))
(when coq-show-proof-stepwise
(add-to-list 'showlist
Expand Down

0 comments on commit 77fd293

Please sign in to comment.