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

Improve PG support of Show Proof Diffs #490

Merged
merged 13 commits into from
May 29, 2020
Merged

Improve PG support of Show Proof Diffs #490

Changes from 1 commit
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
8e12eee
First try for feature #487
CyrilAnac May 11, 2020
ecb4747
All case for Show and regex variable
CyrilAnac May 14, 2020
aba3f2b
Fix name clash & rephrase some strings
erikmd May 15, 2020
04aff70
WIP for #487
CyrilAnac May 18, 2020
22681a3
Apply reviews of @erikmd
CyrilAnac May 20, 2020
ff9b5b1
test: Add regression test (currently failing)
erikmd May 20, 2020
411ebb2
fix: Do "Show Proof…" (with "?Goal") as soon as the proof is started
erikmd May 20, 2020
3ab3f5e
fix: backtrack wrong type argument
CyrilAnac May 25, 2020
8627fba
fix: backtrack for "Show Proof" disabled
CyrilAnac May 28, 2020
5b1b8ac
Add tests and flags system
CyrilAnac May 28, 2020
cc4b4f6
Fix the test 081
CyrilAnac May 28, 2020
77fd293
Minor changes
CyrilAnac May 29, 2020
9c82b71
refactor: Remove unneeded coq-should-response
erikmd May 29, 2020
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
Prev Previous commit
refactor: Remove unneeded coq-should-response
  • Loading branch information
@erikmd
erikmd committed May 29, 2020
commit 9c82b71d396b425337592f96f2e9b6a1d97be0c0
34 changes: 15 additions & 19 deletions ci/coq-tests.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -165,21 +165,17 @@ For example, COMMENT could be (*test-definition*)"
(goto-char (point-min))
(search-forward comment))

(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-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)
(defun coq-should-buffer-regexp (regexp &optional buffer-name)
"Check REGEXP matches in BUFFER-NAME (*response* if nil)."
(should (string-match-p
regexp
(string-trim
(with-current-buffer (or buffer-name "*response*")
(buffer-substring-no-properties (point-min) (point-max)))))))

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

;; TODO: Use https://github.com/rejeep/ert-async.el
;; and/or ERT https://www.gnu.org/software/emacs/manual/html_node/ert/index.html
Expand All @@ -201,7 +197,7 @@ For example, COMMENT could be (*test-definition*)"
(coq-test-goto-before "(*test-definition*)")
(proof-goto-point)
(proof-shell-wait)
(coq-should-response "trois is defined"))))
(coq-should-buffer-string "trois is defined"))))


(ert-deftest 021_coq-test-regression-goto-point ()
Expand Down Expand Up @@ -252,7 +248,7 @@ For example, COMMENT could be (*test-definition*)"
(let ((proof-point (save-excursion (coq-test-goto-after "(*error*)"))))
(proof-goto-point)
(proof-shell-wait)
(coq-should-response "Error: Unable to unify \"false\" with \"true\".")
(coq-should-buffer-string "Error: Unable to unify \"false\" with \"true\".")
(should (equal (proof-queue-or-locked-end) proof-point))))))


Expand Down Expand Up @@ -282,7 +278,7 @@ 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-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(lambda ()
(coq-test-goto-before " (*test-insert*)")
Expand All @@ -294,15 +290,15 @@ For example, COMMENT could be (*test-definition*)"

(ert-deftest 081_coq-test-regression-show-proof-diffs()
"Test for Show Proof Diffs"
(coq-fixture-on-file
(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-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 "<diff.added.bg>(fun <diff.added>(</diff.added>A : Prop<diff.added>) (proof_of_A : A)</diff.added> => ?Goal)</diff.added.bg>" "*coq*")
(coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)")))
'show-proof-stepwise 'diffs-on))

Expand Down