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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel


_______________________________________________
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