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>