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
Next Next commit
Add tests and flags system
  • Loading branch information
@CyrilAnac
CyrilAnac committed May 29, 2020
commit 5b1b8ac75056773b4452ce7a41518258010b2bbe
69 changes: 54 additions & 15 deletions ci/coq-tests.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@

(defun coq-test-exit ()
"Exit the Coq process."
(proof-shell-exit t))
(proof-shell-exit t))

; (coq-test-on-file nil (message (buffer-file-name)) (message "OK") 42)

Expand Down Expand Up @@ -110,8 +110,13 @@
#'proof-done-invisible
'no-error-display 'no-response-display 'no-goals-display))

(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)))
)
CyrilAnac marked this conversation as resolved.
Show resolved Hide resolved

(defun coq-fixture-on-file (file body)

(defun coq-fixture-on-file (file body &rest flags)
CyrilAnac marked this conversation as resolved.
Show resolved Hide resolved
"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 @@ -142,8 +147,10 @@ then evaluate the BODY function and finally tear-down (exit Coq)."
(with-current-buffer buffer
(setq proof-splash-enable nil)
(normal-mode) ;; or (coq-mode)
(coq-set-flags t flags)
(coq-mock body))))
(coq-test-exit)
(coq-set-flags nil flags)
(not-modified nil) ; Clear modification
(kill-buffer buffer)
(when rmfile (message "Removing file %s ..." rmfile))
Expand All @@ -166,12 +173,18 @@ For example, COMMENT could be (*test-definition*)"
(with-current-buffer "*response*"
(buffer-substring-no-properties (point-min) (point-max)))))))

(defun coq-should-buffer (message)
CyrilAnac marked this conversation as resolved.
Show resolved Hide resolved
(should (string-match-p message
(string-trim
(with-current-buffer "*coq*"
(buffer-substring-no-properties (point-min) (point-max)))))))

;; 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 @@ -180,8 +193,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 @@ -191,8 +204,8 @@ 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"
CyrilAnac marked this conversation as resolved.
Show resolved Hide resolved
(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-after "(*test-definition*)")
(proof-goto-point)
Expand All @@ -202,8 +215,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
CyrilAnac marked this conversation as resolved.
Show resolved Hide resolved
(coq-test-full-path "test_stepwise.v")
(lambda ()
(coq-test-goto-before " (*test-lemma*)")
(let ((proof-point (point)))
Expand All @@ -214,8 +227,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 @@ -230,8 +243,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 @@ -256,13 +269,39 @@ 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)
(goto-char (point-min))
(insert "(*.*)")
(should (equal (proof-queue-or-locked-end) 1)))))

(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")
(lambda ()
(coq-test-goto-before " (*test-insert*)")
(proof-goto-point)
(proof-shell-wait)
(coq-should-response "(fun (A : Prop) (proof_of_A : A) => ?Goal)"))
CyrilAnac marked this conversation as resolved.
Show resolved Hide resolved
'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")
(lambda ()
(coq-test-goto-before " (*test-insert*)")
(proof-goto-point)
(proof-shell-wait)
(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>"))
'show-proof-stepwise 'diffs-on))


(provide 'coq-tests)

;;; coq-tests.el ends here