You don't see the error any more, because we have now double
security:
- first the buffer is retract because of
   proof-no-fully-processed-buffer
- second coqtop is killed on switching the active scripting
   buffer


Great! BTW, I think the retraction is a bit clunky in the UI because it makes the pointer leap to the top of the buffer.

At the moment proof-no-fully-processed-buffer is therefore not
necessary, because killing coqtop retracts everything. Eventually
I want coqtop to survive switching the active buffer if the load
path' of the new and old buffer are equal. Then
proof-no-fully-processed-buffer will again be essential.

OK, understood.

    Regarding test case above: the bug mentioned in README is fixed, but
    the behaviour I described earlier (about Coq process being started at
    odd time) still happens when I follow the "To provoke an error"

When do you see coq being restarted? When I follow the old
instructions (that is without disabling the
deactivate-scripting-hook), I see:
- coq starting when I script the first comment in a.v
- coq killed when I script the first comment in b.v
- coq started again when I script the first non-comment line in
   b.v

This is precisely as it should be. (Only that I don't understand
why I can script the first comment in b.v without coq running.)

Yes, I see the same and it is the last point that I was querying.

I suspect what is happening is that you are killing the process at a place in the code that is not expecting this to happen (i.e., deactivating scripting). Whenever a command is sent to the prover, it is cranked up automatically if it is not running already. But comments are skipped in the interface, hence the behaviour above.

This is a concern because it's probably assumed elsewhere in the code that the process is running whenever we have an active script buffer. So we should make sure that the process is cranked up in the script activation code too.

Looking at the code, this is supposed to be done already by proof-shell-ready-prover in proof-activate-scripting. Maybe some state isn't being cleared which makes this function think it has nothing to do. I'll investigate (later...)

Possibly related to this, I see some odd messages in the log from the Coq autotest examples, where the code is trying to find a process connected to a script buffer rather than the *coq* buffer. Run "make test.coq" (see error "Buffer f.v has no process")

 - D.

PS I'd prefer to move this discussion to the trac rather than mailing list. It's a good way of recording the open issues, any way.
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

Reply via email to