Stefan Monnier monn...@iro.umontreal.ca writes:
I think this deserves an Emacs bug report.
see http://debbugs.gnu.org/cgi/bugreport.cgi?bug=13400
There are definitely some documentation problems.
process-send-string is not mentioned as function that might
trigger a filter call.
I think
I wrote:
here is a patch that solves the problem for me. Any comments?
I committed now. I deleted the argument of proof-shell-filter, to
make sure, nobody will use it. Reasons are described in the doc
comments.
Hendrik
___
ProofGeneral-devel
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,
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
