[PG-devel] overlapping calls to proof-shell-filter

2013-01-08 Thread Hendrik Tews
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,

Re: [PG-devel] overlapping calls to proof-shell-filter

2013-01-08 Thread David Aspinall
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