sometimes I see prooftree crashes with a cold disk cache (eg
after reboot or after "sync; sudo sh -c 'echo 3 >

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?


ProofGeneral-devel mailing list

Reply via email to