Opened 10 years ago

Closed 10 years ago

Last modified 10 years ago

#397 closed defect (fixed)

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

Reported by: tews Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.1
Component: 2:pg-emacs Keywords:
Cc:

Description

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.

Attachments (1)

proof-script-activate.patch (2.8 KB) - added by David Aspinall 10 years ago.
Attempt to fix from Jan

Download all attachments as: .zip

Change History (5)

comment:1 Changed 10 years ago by 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.

comment:2 Changed 10 years ago by David Aspinall

Status: newaccepted

Changed 10 years ago by David Aspinall

Attachment: proof-script-activate.patch added

Attempt to fix from Jan

comment:3 Changed 10 years ago by David Aspinall

Resolution: fixed
Status: acceptedclosed

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

comment:4 Changed 10 years ago by 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.

Note: See TracTickets for help on using tickets.