ProofGeneral
Why does PG show stale goals?
I don't know what happened of late, but over the last few years it's become more and more common that I have to ask PG to refresh the goal explicitly. Often the goal window stays blank, or it shows an outdated goal. If a comment follows a bit of code and both are processed together, PG doesn't show the goal. And so on.
What's going on? It's come to the point that C-c C-p is one of the first PG keybindings I teach my students. Is it our fault, or is it on Coq's side?
I would say it is the silent processing together with the difficulty to reliably insert something in proof-action-list. I believe it is our fault. With 8d545bca and 14ea1a3f it will become easier to insert stuff into proof-action-list.
Thanks. Then I think we should treat your work as critical-priority. At the moment, PG is basically unusable for newcomers. Teaching a Coq class is a real reality check on that front.
It is our fault for sure, but it also comes from coq slowly changing its behaviour. I think it spontaneously prints the goal less often. We definitely need to refactor the "Show" stuff.
@hendriktews is it really a problem of adding to the action list? It looks to me that we need a way to issue a "Goal" precisely when there is nothing left in the action list (and there is an open proof). Without cleaning the response buffer.
I opened a PR with tests where PG does not show any goal or the wrong one. They cover the cases of
- Proof
- comment at the end of the queue region
- auto
- error in the proof script
If you know another way to get no or the wrong goal in PG, please add a test or tell here about it.
This is likely due coqtop not printing a goal again if it didn't change. For example, after Proof..
Only reliable fix is to actually move to a model where PG queries for goals, and stops playing weird games with Coq output [ PG will always lose]
