You don't see the error any more, because we have now double
- first the buffer is retract because of
- second coqtop is killed on switching the active scripting
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.
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
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")
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
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.