is there viewvc and cvshistory running on the Proof General cvs?

There's a handy view via Mercurial here courtesy of Markarius Wenzel (hopefully he won't mind me advertising)

    I've committed a patch to proof-protected-process-or-retract
    now which fixes this problem and I think your test case works.

I don't see this. Here, coqtop still survives when I kill a
completely asserted active scripting buffer. The reason seems to
be that the unless now causes proof-protected-process-or-retract
to return nil and then the progn in
proof-deactivate-scripting-auto, which contains the deactivation
hooks, is skipped.

OK, let me take a look, I probably missed that the return value was being used. I saw the killing but maybe it was happening at the wrong moment which prompted my question below...

    But there may be some further issues (try the coq autotest

OK, I do "make test.coq" and then I see some flickering and
finally emacs hangs. What is the proposed way to use the

Just as you did, Emacs shouldn't hang! But that might be a bug in the test as I tried to put in a multiple file test. You can set debug-on-signal to interrupt and get a backtrace.

coqtop is killed via proof-shell-exit inside
proof-deactivate-scripting-hook, that's inside the deactivation
action, isn't it?

    but I'm seeing it being started
    after switching buffers and beginning scripting somewhere
    else, e.g. on the first non-comment element of the file.

Yes, that's the desired behavior: You can freely switch buffers,
but as soon as you start scripting in a buffer different from the
active scripting buffer, then the coptop process is killed.

OK, "as soon as you start scripting" includes comments, i.e. on making the buffer active for scripting? That's what I expected (and maybe what you intended!).


 - D.
ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to