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

[hendriktews]

This is another attempt towards fixing #568.

[hendriktews]

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

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]

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

[Matafou]

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

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]

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]

• 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]

• 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.