"No more goals" hides other message (in completely-silent mode)

[SkySkimmer]

eg

Goal True.
Proof.
  exact I.
  Check 0.

It seems impossible to see the message from Check 0.
Even an error (eg from Check 0 0.) gets hidden by "No more goals".

[SkySkimmer]

(with rocq 9.2 and master)

[Matafou]

Thx!
Indeed there is a problem when Show triggers a message. I will have a look at it. I think we should just prevent response clearing when issuing a Show.
Pinging @hendriktews too.

[Matafou]

After testing it is just that we need to ignore coq-run-completely-silent when coq >=9.2. I will try to push something quickly.
I think we are close to have a "working" PG, compared to the last years.
Edit: Nope. Simply setting coq-run-completely-silent to nil does not work.

[cpitclaudel]

Can we fix this upstream? Ideally rocq repl would change without a corresponding PG overlay, since PG is the only consumer of the reply outside of coqrst.

[Matafou]

We have a PR that make things better (only for rocq 9.2). But it does not fix things perfectly. More precisely things are still not displayed when there a not focused goals (the message signaling this hides the previous messages).
We could merge it anyways because it makes things better, and try to fix things completely later on.
ping @hendriktews.