Rocq: enable messages for Rocq >= 9.2

[hendriktews]

Disable Set Silent for Rocq >= 9.2, which does not print any goals any more. See also PR 21038 for Rocq.

Fixes #842 #849 #843

[Matafou]

@Hendrik is there a reason we don't merge this right now?

[Matafou]

well except for the tests.

[Matafou]

@hendriktews I tested :expected-result (if (coq--version< (coq-version) "9.2alpha") :failed :passed) on these three tests and it seems to work. We should merge this right now I think. So that people using coq master can (setq coq-pinned-version "9.2beta") and have a better experience. What do you think?

[hendriktews]

@Hendrik is there a reason we don't merge this right now?

As is, the added line breaks our CI because it throws an error when there is no Coq/Rocq available. Therefore I am strongly opposing to merge this PR in this form. I try to allocate some time this week to bring this PR into shape.

[Matafou]

Hi Hendrik.

As is, the added line breaks our CI

You mean the line I propose to add in the tests? Or the PR itself?

because it throws an error when there is no Coq/Rocq available.

Sorry for the dumb question: why is it bad that a test fails when some of its dependencies is not available? Our CI is supposed to provide coq/rocq isn't it ?

Therefore I am strongly opposing to merge this PR in this form.
I try to allocate some time this week to bring this PR into shape.

Thanks!

[hendriktews]

As is, the added line breaks our CI

You mean the line I propose to add in the tests? Or the PR itself?

I mean the coq--version test that the PR adds in coq.el. I haven't yet looked at your proposal.

Sorry for the dumb question: why is it bad that a test fails when some of its dependencies is not available? Our CI is supposed to provide coq/rocq isn't it ?

Yes, but not for all tests. The check-doc and the indentation tests run without Coq/Rocq. We also have a test that checks that PG does not crash if it cannot find any Coq/Rocq, which, for obvious reasons, runs such that Coq/Rocq is apparently not available. Further, the early crash when loading coq.el may hide other errors.

The PR, as it is now, makes PG crash if some user happens to load it without Coq/Rocq, which some users, quite understandable, find irritating, see #551.

[Matafou]

Thanks for the explanation. Yes this call to coq should be protected indeed.

[monnier]

It's also an instance of the general rule that merely loading an ELisp file should not significantly affect Emacs's behavior: signaling an error is significant.

[Matafou]

@hendriktews. Since I have time right now and want this to be merged quickly I propose something upon your PR in this branch. Feel free to use it (or not).

In short:

• I emit a warning message (not a "real" emacs warning) when no coq version is detected.
• coq-version< returns nil instead of failing.
• I added the conditionals in the CI tests that should fail with coq < 9.2alpha.
• I did NOT yet update doc strings magic.

One question that remains but can wait another PR: should we have a CI test with a VM where no coq is intalled? So that we check that PG works correctly in this case.

[Matafou]

I have been using this version for a while and I still experience losses of messages. I detected at least one situation where this is due to the call to Show which may create new responses (together with the goal output) and it causes the previous response to be overwritten instead of catenated.

For instance:

Lemma foo: forall n:nat, n = 0 \/ exists m, n = S m.
Proof.
  destruct n.
  - Time (left;reflexivity).

Only prints the "... Focus next goal with bullet -.", but not the Finisehd transaction... information.
The coq content is the following:

<prompt>foo < 28 |foo| 0 < </prompt>Time (left;reflexivity).
Finished transaction in 0. secs (0.u,0.s) (successful)

<prompt>foo < 30 |foo| 0 < </prompt>Show.
<infomsg>
This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.
</infomsg>
1 goal

goal 1 (ID 12) is:
 S n = 0 \/ (exists m : nat, S n = S m)
<prompt>foo < 30 |foo| 0 < </prompt>

[Matafou]

Summing up again the bug with 9.2:

• a command is detected as the last one in the stack
• so a Show is inserted after it in the stack with a few tags.
  • In particular the tag keep-response is set so that the response buffer is not cleared during the Show
  • But actually there is still a case where the response buffer is cleared anyway: when Show produces a new "response". In this case PG clears out the previous responses anyway. I see at least two case's where Show produces a response:
    1. When Show displays No more goal. which is detected as response.
    2. When Show displays `This subproof is complete, but there are some unfocused goals. ... which is also detected as response.

For example the following script

Goal forall n m: nat, n = m -> True.
Proof.
  intros n m H.  
  destruct n.
  - exact I.
    Check 0.

Generates an output ending with:

<prompt>Unnamed_thm < 73 |branch| 0 < </prompt>Check 0.
0
     : nat

<prompt>Unnamed_thm < 74 |branch| 0 < </prompt>Show.
<infomsg>This subproof is complete, but there are some unfocused goals.
         Focus next goal with bullet -.
         </infomsg>
1 goal

goal 1 (ID 17) is:
 True

<prompt>Unnamed_thm < 74 |branch| 0 < </prompt>

Check 0's output is immediately replaced by the <infomsg>.

So we need a way to

• either make this infomsg to be dispatched in the goals buffer so that the response buffer is not cleared.
• or avoid clearing the response buffer when issuing the Show

Both solutions (I prefer the second one) are a bit involved because of PG's way of dealing with messages. Not mentioning the fact that we need to remain compatible with coq < 9.2.