Skip to content

Coq: run silently and explicitly Show when necessary - second attempt #762

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

Merged
hendriktews merged 4 commits into from
May 16, 2025
Merged

Coq: run silently and explicitly Show when necessary - second attempt #762

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
faeaf21
coq: run silently and explicitly Show when necessary
hendriktews Apr 17, 2024
f87fdda
clear goals buffer after Qed and Admitted when running silent
hendriktews Apr 18, 2024
1e57bba
add option to disable silent and switch back to old (buggy) behavior
hendriktews May 12, 2024
41d0e20
fix prooftree for Coq/Rocq running completely silent
hendriktews Apr 17, 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
5 changes: 5 additions & 0 deletions CHANGES
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,11 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
during auto compilation.
*** Fix issues #687 and #688 where the omit-proofs feature causes
errors on correct code.
*** Run Coq completely silent to fix #568. If you experience unexpected
behavior, please report a bug and disable
`coq-run-completely-silent' to switch back to old behavior. Note
that external proof tree display is only supported if Coq/Rocq
runs completely silent.


* Changes of Proof General 4.5 from Proof General 4.4
Expand Down
16 changes: 16 additions & 0 deletions ci/coq-tests.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,6 +200,8 @@ For example, COMMENT could be (*test-definition*)"


(ert-deftest 020_coq-test-definition ()
;; There are no infomsgr when running silent.
:expected-result :failed

@Matafou Matafou May 16, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should probably test this when only one command is sent at a time.

@hendriktews hendriktews May 19, 2025

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AFAICT there is only one command processed in this test. Even if you process one definition alone, there is no infomsg when running silent.

@Matafou Matafou May 19, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You are right. this behaviour is ok for me. I wonder if someone really care about this fonfirmation messages outside pure textual coqtop use.

"Test *response* output after asserting a Definition."
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
Expand Down Expand Up @@ -366,6 +368,9 @@ For example, COMMENT could be (*test-definition*)"

(ert-deftest 080_coq-test-regression-show-proof-stepwise()
"Regression test for the \"Show Proof\" option"
;; When running silent, the Show Proof command is issued, but its
;; output is not (yet) kept in the response buffer.
:expected-result :failed
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(lambda ()
Expand All @@ -392,6 +397,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 @@ -413,6 +422,13 @@ For example, COMMENT could be (*test-definition*)"
;; (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

@Matafou Matafou May 16, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The point in coq file is not the same: "(FailNoTrace)" vs "(FailTrace)". Concretelty the difference is the command Local Unset Ltac Backtrace..

@hendriktews hendriktews May 19, 2025

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK, it would be nice if the documentation in that file would describe what is tested there.

;; 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
13 changes: 5 additions & 8 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 @@ -283,17 +283,14 @@ which action the goals buffer should have been reset."

(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" nil))

(ert-deftest goals-after-comment ()
"Test goals are present after a comment."
:expected-result :failed
(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" nil))

(ert-deftest goals-after-simpl ()
Expand All @@ -302,7 +299,6 @@ which action the goals buffer should have been reset."

(ert-deftest goals-after-error ()
"Test goals are present after an error."
:expected-result :failed
(goals-after-test coq-src-error "error" t))

(ert-deftest goals-reset-after-admitted ()
Expand All @@ -315,7 +311,6 @@ which action the goals buffer should have been reset."
"Lemma a" "no more goals"))

(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"))
Expand Down Expand Up @@ -381,7 +376,6 @@ two-pane mode."

(ert-deftest goals-up-to-date-at-error ()
"Check that goals are updated before showing the error."
:expected-result :failed
(update-goals-when-response coq-src-update-goal-after-error
"Lemma foo"
"H : eq_one 1 -> False"
Expand All @@ -404,7 +398,6 @@ This test checks several commands inside a proof with a final
Search command. After processing these commands, the goals buffer
should have been updated and the response buffer should contain
something and be visible in two-pane mode."
:expected-result :failed
(update-goals-when-response coq-src-update-goal-after-search
"Lemma g"
"2 = 2"
Expand All @@ -427,7 +420,6 @@ This test checks several commands inside a proof with a final
Check command. After processing these commands, the goals buffer
should have been updated and the response buffer should contain
something and be visible in two-pane mode."
:expected-result :failed
(update-goals-when-response coq-src-update-goal-after-check
"Lemma h"
"3 = 3"
Expand Down Expand Up @@ -578,6 +570,7 @@ window."
(check-response-present #'coq-Search 6 "(0 <= 2)" "Nat.le_0_2"))

(ert-deftest response-buffer-visible-coq-search-something-proof-end ()
:expected-result :failed
"Check response for coq-Search on (0 <= 2) at proof end.
Skipped for 8.14 and 8.15, there Coq reacts with an error when searching
in proof mode with no more goals."
Expand All @@ -592,11 +585,13 @@ in proof mode with no more goals."
(check-response-present #'coq-Search 3 "(0 <= 2)" "Nat.le_0_2"))

(ert-deftest response-buffer-visible-coq-search-empty-inside-proof ()
:expected-result :failed
"Check empty response for coq-Search on 42 inside proof"
(message "Check empty response for Search 42 is shown inside proof")
(check-response-present #'coq-Search 6 "42" t))

(ert-deftest response-buffer-visible-coq-search-empty-proof-end ()
:expected-result :failed
"Check empty response for coq-Search on 42 at proof end.
Skipped for 8.14 and 8.15, there Coq reacts with an error when searching
in proof mode with no more goals."
Expand All @@ -611,13 +606,15 @@ in proof mode with no more goals."
(check-response-present #'coq-Search 3 "42" t))

(ert-deftest response-buffer-visible-coq-check-print-all-inside-poof ()
:expected-result :failed
"Check response for coq-Check on Nat.add_comm inside proof with printing all."
(message
"Check response for Check Nat.add_comm inside proof with printing all")
(check-response-present
#'(lambda() (coq-Check t)) 6 "Nat.add_comm" "@eq nat (Nat.add n m)"))

(ert-deftest response-buffer-visible-coq-check-print-all-poof-end ()
:expected-result :failed
"Check response for coq-Check on Nat.add_comm at proof end with printing all."
(message
"Check response for Check Nat.add_comm at proof end with printing all")
Expand Down
Loading
Loading