Coq PG: changing scripting buffer and automatically restarting misses first command

[tews]

The issue is that after changing the active scripting buffer, the first assert operation is lost, because the prover is not running. To reproduce go to coq/ex/test-cases/multiple-files-single-dir and do some scripting in, say, a.v. Then change to a different file (eg b.v) and do some scripting there. To clearly see the effect, make sure the second file (b.v) does not start with a comment.

There is a patch in ​http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000114.html but it needs reviewing.

[David Aspinall]

Here's an experimental patch I wrote a while back to try to fix this. Seems similar to Hendriks. Also needs testing/thought.

[David Aspinall]

Attempt to fix from Jan

[David Aspinall]

The attached patch has now been applied. Hendrik sent some comments on this which I'm posting next.

[David Aspinall]

The main difference between your and my patch is that I execute

  (proof-shell-ready-prover queuemode) 

outside the

  (unless (equal (current-buffer) proof-script-buffer) 

while in your patch it is inside.

I tried to investigate whether there is a difference if the call to proof-shell-ready-prover is inside or outside the big unless in proof-activate-scripting.

To me it looks like there is an invariant saying that proof-script-buffer can only be non-nil if the prover is running. You can only break the invariant by killing the prover in the proof-deactivate-scripting-hook (which is currently happening for Coq).

If you move proof-shell-ready-prover inside the unless then you loose a bit of robustness. Ironically, the robustness you would lose is responsible for the fact that the patch we are discussing now is not really urgent. Currently, if the invariant is broken, then the next assert will silently restart the prover.