ProofGeneral
Disappearance of all infomsg
Since https://github.com/ProofGeneral/PG/pull/762 all infomsg disappeared, for instance (but it's all over the place)
Definition n := 42.
used to produce
<infomsg>n is defined</infomsg>
which is now gone.
Immediate workaround is to unset the variable coq-run-completely-silent.
My understanding is that Set Silent only makes sense for "compile to point" actions (C-c C-RET) but not "compile line" (C-c C-n), but I may be wrong.
It is reasonable to ask to see the message when using proof-assert-next-command-interactive. @hendriktews maybe we can just modify this function to put Unset Silent. and Set Silent. around the command?
Sadly this command can be issued (even repeatedly) while previous commands are still being processed (in which case it only extends the command queue). I even suspect some users use this feature heavily.
@proux01 Thanks for filing the issue.
Even running only single commands not silent will reopen (parts of) #568, because Coq/Rocq does not always makes the effort to print the current goal (eg. Proof and auto).
There is quite a bit of machinery for printing goals while keeping errors that is enabled for running silent. Therefore wrapping one command in unset/set silent won't have the desired effect. Some parts of this machinery can currently not be deconfigured, this is why the manual says you have to restart PG after changing coq-run-completely-silent.
IMO, similar to re-printing the current goal, there should be a Coq/Rocq command that re-prints any messages.
IMO, similar to re-printing the current goal, there should be a Coq/Rocq command that re-prints any messages.
That would require a notion of "current messages" which doesn't make sense.
That being said, I'm still of the opinion that the default value of coq-run-completely-silent is bad. Completely missing output (it's not even in the coq buffer) is much worse than having to hit C-c C-p from time to time.
I think rocq having an option Print Goal Spontaneously that we could unset would solve most of our problems. @hendriktews what do you think?
The whole change we made was to ensure that the goal displayed in the goals buffer is accurate. For this we had to disable completely the spontaneous goal printing of coqtop (which is much less systematic than it used to be). The only way to do this was to Set Silent but hiding the other messages is a side effect we did not want. So an option that only disable goal spontaneous printing would be great I think.
I think rocq having an option
Print Goal Spontaneouslythat we could unset would solve most of our problems.
I'd expect this to be rather easy to implement. It could even be made the default in emacs mode.
I think rocq having an option
Print Goal Spontaneouslythat we could unset would solve most of our problems.
Yes, this could help to solve this issue.
Could you please open an issue on https://github.com/rocq-prover/rocq/ I'll fix it in a PR and hopefully we'll have that in 9.2.
That would require a notion of "current messages" which doesn't make sense.
In this formulation it does not make sense. However, a command to reprint the last message or even all messages since a certain state does make sense IMO.
That being said, I'm still of the opinion that the default value of
coq-run-completely-silentis bad. Completely missing output (it's not even in the coq buffer) is much worse than having to hit C-c C-p from time to time.
OK, acknowledged. My impression is that the missing and outdated goals were the bigger problem for most people.
That would require a notion of "current messages" which doesn't make sense.
In this formulation it does not make sense. However, a command to reprint the last message or even all messages since a certain state does make sense IMO.
Indeed, still more work (needs to clarify the spec, add a buffer,...) and seems more error prone than just having Rocq (not) print correct things in the first place.
That being said, I'm still of the opinion that the default value of
coq-run-completely-silentis bad. Completely missing output (it's not even in the coq buffer) is much worse than having to hit C-c C-p from time to time.OK, acknowledged. My impression is that the missing and outdated goals were the bigger problem for most people.
I agree it's bad too, and maybe more impacting for beginner users.
That would require a notion of "current messages" which doesn't make sense.
In this formulation it does not make sense. However, a command to reprint the last message or even all messages since a certain state does make sense IMO.
Indeed, still more work (needs to clarify the spec, add a buffer,...) and seems more error prone than just having Rocq (not) print correct things in the first place.
The existing protocols for interactiing with rocq do register messages from each commands, don't they? Anyway we probably have found a solution (for coming versions of rocq) with the introduction of a new rocq option which silences only the goal (spontaneous) printings.