Why does PG show stale goals?

[cpitclaudel]

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?

[hendriktews]

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 8d545bc and 14ea1a3 it will become easier to insert stuff into proof-action-list.

[cpitclaudel]

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.

[Matafou]

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.

[Matafou]

@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.

[cpitclaudel]

Thanks @Matafou.

[hendriktews]

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.

[ejgallego]

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]