Hello Hendrik
Quick thoughts: this sounds like a pretty fundamental problem and
surprising if we hadn't come across it before. Do you definitely see
this in the ordinary running code, not just when using the debugger?
Maybe prooftree input is different case to prover input.
If we need to fix it, I suppose we could try to exit the PG filter
function early using our own flag to detect nested calls. A more robust
mechanism might be to try to send new input from the main event loop
instead, but that would be a significant reworking. (Or could you do
that just for proof tree?)
- David
On 08/01/13 10:41, Hendrik Tews wrote:
Hi,
sometimes I see prooftree crashes with a cold disk cache (eg
after reboot or after "sync; sudo sh -c 'echo 3 >
/proc/sys/vm/drop_caches'").
What apparently happens is that at some stage process-send-string
blocks because the pipe to prooftree is full. This happens inside
proof-shell-filter, because the prooftree display commands are
created and sent when output arrives from Coq.
When I/O blocks, Emacs automatically accepts output processes. So
it calls proof-shell-filter again before the previous call
finished. Finally some garbage or truncated messages is written
to the pipe and prooftree crashes.
It should definitely not happen that proof-shell-filter is called
while another instance is still running. Does anybody know a way
to ensure this?
Bye,
Hendrik
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
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.
