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

hendriktews · 2024-04-17T15:57:58Z

This is another attempt towards fixing #568.

hendriktews · 2024-05-12T14:04:33Z

@Matafou , @erikmd , @cpitclaudel : With the option coq-run-completely-silent to switch back to old behavior, I believe the risk of breaking a use case of some user is manageable. Therefore I suggest to merge this in about a week.

erikmd · 2024-05-12T21:47:14Z

Hi @hendriktews!

(I just quickly skimmed the PR code but) LGTM, thanks.

With the option ..., I believe the risk of breaking a use case of some user is manageable. Therefore I suggest to merge this in about a week.

Agree

Matafou · 2024-05-13T14:02:54Z

Maybe I need to test how it interacts with debug mode. I don't have much time this week though.

Matafou · 2024-09-10T08:53:06Z

@hendriktews can you tell us what remains to be tested/adapted pls? I think this PR should not rot.
You said elsewhere that the prefix arg C-u for queries like coq-Print wouldn't work. What else?

hendriktews · 2024-09-12T15:19:26Z

I use this code on a daily basis, so it is working for me. Remaining things that I know:

coq-Print with prefix arg
prooftree - I have local fixes on top of the commits in this PR to get prooftree working, but they need to be polished before uploading
I have never tried diff or debug mode, it would be nice, if somebody who knows what to expect could try this
Not sure if this is a problem: When you issue a search command (either via C-c C-a C-a or by typing Search into the buffer) inside a proof in two-pane mode (i.e., no response buffer visible), then the search results pop up in the response buffer only if there are results. That is, if you search for (3 + 4) you will be shown the current proof state. This might make the impression, search does not work at all. Outside a proof you will see an empty response buffer, making it obvious, that the search did not yield results.

Matafou · 2024-09-12T16:26:54Z

I use this code on a daily basis, so it is working for me. Remaining things that I know:

* coq-Print with prefix arg

* prooftree - I have local fixes on top of the commits in this PR to get prooftree working, but they need to be polished before uploading

* I have never tried diff or debug mode, it would be nice, if somebody who knows what to expect could try this

I can test this.

* Not sure if this is a problem: [...] This might make the impression, search does not work at all.

I think this is a problem. I must admit I am always in 3 windows mode.

hendriktews · 2024-09-16T14:52:33Z

Not sure if this is a problem: [...] This might make the impression, search does not work at all.

I think this is a problem. I must admit I am always in 3 windows mode.

So it is not a problem for you. It is only a problem when there is no window showing the response buffer when you issue the command. Note that any nonempty response from the search command is correctly shown.

Meanwhile I discovered another problem:

When you are in proof mode without goals, i.e., just before you type QED, then no response from a search or locate command is visible, even in case these commands yield results.

Matafou · 2024-09-19T20:26:58Z

Not sure if this is a problem: [...] This might make the impression, search does not work at all.

I think this is a problem. I must admit I am always in 3 windows mode.

So it is not a problem for you. It is only a problem when there is no window showing the response buffer when you issue the command. Note that any nonempty response from the search command is correctly shown.

No it is not a problem for me, but the lack of user feedback in this case is a (small) problem.

Meanwhile I discovered another problem:

* When you are in proof mode without goals, i.e., just before you type QED, then no response from a search or locate command is visible, even in case these commands yield results.

Indeed. It also happens after other messages like "This subproof is complete, ...".

The reason is that the search command is now followed by a Show. In this case the Show command triggers a response "No more goals.", which is detected as another response message instead of a goal message. Hence it immediately overwrites the response to the query.

I tested and adding "No more goals." to proof-shell-start-goals-regexp solves this problem, but it seems to trigger other problems, e.g. the message "No more goals." is not displayed in goals as expected. I think it is because "No more goals." is already in proof-shell-clear-goals-regexp and proof-shell-proof-completed-regexp. Understanding the interaction between these 3 variables is needed I guess.

Matafou · 2025-04-21T10:43:17Z

I support merging this now.
And see what happens with C-u prefix, debug mode (probably both rarely used) and anything else interacting with this. If ever we get an avalanche of bug reports then we will just switch the default value of coq-run-completely-silent to nil while we look for solutions.

hendriktews · 2025-04-22T19:34:35Z

OK, let's wait for another few days, in case somebody else wants to try it.
I have a simple fix for C-c C-a C-a with empty response, that also fixes C-c C-a C-a just before Qed. The same idea should also work for C-u coq-Print, I just need to roll it out.

hendriktews · 2025-05-12T13:10:33Z

Please excuse the delay, I thought it would be good to first add tests for the searches that get broken by this PR. Hopefully they are now ready, see #827

This is a step towards fixing ProofGeneral#568. It fixes the cases after Proof, comments, auto, errors, Search and Check, leaving now 2 instead of 8 failing tests in ci/simple-tests/test-goals-present.el. Admitted is not handled correctly any more, which is a regression. Using proof-shell-handle-delayed-output-hook and proof-shell-handle-error-or-interrupt-hook we issue a Show command as a priority action item when the last (normal) action item has been processed. The new action item flag 'keep-response tells the generic machinery to not clear the response buffer and to keep it present in two-pane mode in case an error was detected or the last command was a Search or Check that produced a response. The new action item flag 'dont-show-when-silent is used to distinguish the additional Show commands and to avoid an endless loop of Show commands. Set proof-shell-last-output-kind now in proof-shell-handle-delayed-output such that it correctly reflects the cases of goals and response (which has not been the case since commit 037dc9b from 2009. This commit breaks coq-show-proof-stepwise to some extend. Expect 080_coq-test-regression-show-proof-stepwise to fail. Additionally: - update manuals - expect errors in tests 020_coq-test-definition, 090_coq-test-regression-Fail and 091_coq-test-regression-Fail because messages are not printed in silent mode

This solves the remaining known problems from ProofGeneral#568. Fixes ProofGeneral#568.

Add user option coq-run-completely-silent, which, when disabled, switches Coq to old behavior where Coq is dynamically switched to silent on longer action item lists.

- Inside the urgent prooftree action, call now the proof assistant specific function `proof-tree-assistant-specific-urgent-action'. For Coq/Rocq this adds a show command which calls `proof-tree-display-goal-callback' in its callback, which processes the output and sends appropriate commands to prooftree. - Move the call of the urgent prooftree action before calling adding `proof-shell-empty-action-list-command', such that these last actions happen after the show command. - In `proof-shell-filter-manage-output', save the end of the previous command in new variable `proof-shell-old-proof-marker-position' such that callbacks running after the next command has been sent to Coq can access it. This is used inside `proof-tree-display-goal-callback'. - proof-tree display is now only supported when Coq runs completely silent. Supporting it in the other mode should not be too difficult, but I don't think it is worth the effort.

hendriktews · 2025-05-14T13:27:56Z

The last update rebases this PR onto #827 and marks some of these new tests as expected to fail. If nobody objects, I'll merge this Friday.

Matafou · 2025-05-16T10:48:20Z

ci/coq-tests.el

@@ -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


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

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

Matafou · 2025-05-16T12:29:14Z

ci/coq-tests.el

@@ -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


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

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

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

Matafou · 2025-05-16T12:29:48Z

This works like a charm. Thanks a lot @hendriktews for this work.

Matafou · 2025-05-27T07:52:31Z

After a few days of work the only annoying thing for me is the "Set some option; do the command; unset the option" triggered by the C-u prefix. Like C-u C-a C-b eq RET. The commans are sent, but the last unset command makes the response buffer immediately empty.

hendriktews · 2025-05-27T09:13:54Z

Do you mean C-u C-c C-a C-b, i.e., coq-About? Have you tried PR #831, which is supposed to fix these cases? (See also the tests response-buffer-visible-coq-check-print-all-inside-poof and response-buffer-visible-coq-check-print-all-poof-end in ci/simple-tests/coq-test-goals-present.el)
The problem that is still left is when you type About eq. in your proof script buffer just before a Qed after you saw the No more goals message.

Matafou · 2025-05-27T11:31:43Z

Right! I forgot to use the fix.

proux01 · 2025-08-18T10:01:06Z

FWIW, I found the suppression of infomsg really bad. As a user I'm expecting them during interactive sessions.
A least, thanks for adding the coq-run-completely-silent variable that enables to disable this bad behavior, but it should be the default.

hendriktews · 2025-08-19T07:15:52Z

Please open an issue that describes under which situations you miss a message. Then we can add a test and maybe fix it.

proux01 · 2025-08-19T07:21:54Z

Here it is: #842 but it's basically all over the place, not a single instance. Virtually any command can produce a worthwile infomsg.

hendriktews force-pushed the silent-2 branch 3 times, most recently from b7cb334 to 0758343 Compare April 22, 2024 09:17

hendriktews force-pushed the silent-2 branch from 0758343 to 140e076 Compare April 25, 2024 19:46

hendriktews force-pushed the silent-2 branch from 140e076 to 46f6f40 Compare May 12, 2024 13:37

hendriktews mentioned this pull request Sep 2, 2024

Coq: make printing parentheses flag accessible #785

Merged

hendriktews force-pushed the silent-2 branch 2 times, most recently from 942720d to 837fae8 Compare September 30, 2024 11:29

hendriktews force-pushed the silent-2 branch 2 times, most recently from 5bdedad to cf3398a Compare April 20, 2025 19:13

hendriktews added 4 commits May 14, 2025 10:44

clear goals buffer after Qed and Admitted when running silent

f87fdda

This solves the remaining known problems from ProofGeneral#568. Fixes ProofGeneral#568.

add option to disable silent and switch back to old (buggy) behavior

1e57bba

Add user option coq-run-completely-silent, which, when disabled, switches Coq to old behavior where Coq is dynamically switched to silent on longer action item lists.

hendriktews force-pushed the silent-2 branch from cf3398a to 41d0e20 Compare May 14, 2025 11:45

hendriktews merged commit f5d929e into ProofGeneral:master May 16, 2025
146 checks passed

hendriktews deleted the silent-2 branch May 16, 2025 09:13

Matafou reviewed May 16, 2025

View reviewed changes

Matafou mentioned this pull request May 27, 2025

Fix response #831

Merged

This was referenced Jun 2, 2025

experiment for #188 and #429 -- insert show after error in silent mode #467

Closed

Experiments to fix the goals not showing on errors. #429

Closed

hendriktews mentioned this pull request Jun 23, 2025

Show command with diffs rocq-prover/rocq#20793

Open

proux01 mentioned this pull request Aug 19, 2025

Disappearance of all infomsg #842

Open

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

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

Uh oh!

Conversation

hendriktews commented Apr 17, 2024

Uh oh!

hendriktews commented May 12, 2024

Uh oh!

erikmd commented May 12, 2024

Uh oh!

Matafou commented May 13, 2024

Uh oh!

Matafou commented Sep 10, 2024

Uh oh!

hendriktews commented Sep 12, 2024

Uh oh!

Matafou commented Sep 12, 2024

Uh oh!

hendriktews commented Sep 16, 2024

Uh oh!

Matafou commented Sep 19, 2024

Uh oh!

Matafou commented Apr 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hendriktews commented Apr 22, 2025

Uh oh!

hendriktews commented May 12, 2025

Uh oh!

hendriktews commented May 14, 2025

Uh oh!

Uh oh!

Matafou May 16, 2025

Choose a reason for hiding this comment

Uh oh!

hendriktews May 19, 2025

Choose a reason for hiding this comment

Uh oh!

Matafou May 16, 2025

Choose a reason for hiding this comment

Uh oh!

hendriktews May 19, 2025

Choose a reason for hiding this comment

Uh oh!

Matafou May 19, 2025

Choose a reason for hiding this comment

Uh oh!

Matafou commented May 16, 2025

Uh oh!

Matafou commented May 27, 2025

Uh oh!

hendriktews commented May 27, 2025

Uh oh!

Matafou commented May 27, 2025

Uh oh!

proux01 commented Aug 18, 2025

Uh oh!

hendriktews commented Aug 19, 2025

Uh oh!

proux01 commented Aug 19, 2025

Uh oh!

Uh oh!

Matafou commented Apr 21, 2025 •

edited

Loading