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
