Proof General may be forced to run Rocq completely silent for Rocq 9.2

[hendriktews]

Since PR #762 has been merged, Proof General sets option Silent in coq/rocq and never clears it, such that the background coq/rocq runs completely silent. This fixes many problems with missing goals and outdated goals, see #568. Proof General also provides the option coq-run-completely-silent to switch back to the old behavior, if running completely silent causes problems. To check whether your Proof General switches coq/rocq to run completely silent, simply process Proof. or Proof using.: If you see a goal, coq/rocq runs completely silent for you. As a result to #842, upstream Rocq discusses now a change that effectively will eliminate the possibility to switch back to old behavior with Rocq 9.2, see rocq-prover/rocq#21038. We therefore invite all Proof General users to try out the new behavior and report any problems. Apart from the missing info messages (#762) we know that proof diffs are not working when running completely silent, see #835 and rocq-prover/rocq#20793.

[hendriktews]

@erikmd @Matafou @cpitclaudel @RalfJung: Please consider to spread this to other PG users.

[SkySkimmer]

It seems the Fail output gets silenced in "completely silent" mode (eg Fail Check 0 : 0.)

[Matafou]

@hendriktews now that the -emacs option does not print goals, we don't need the Set Silent anymore do we?

[Matafou]

Of course I mean when the next Rocq is detected.