Re: [PG-devel] overlapping calls to proof-shell-filter
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 many packages are vulnerable to this problem, although they usually don't suffer from it. The most common case where they do suffer from it is when you try to Edebug the process filter. I believe it would be good to have a process-specific flag that inhibits overlapping parallel calls to the same process filter. Emacs could accept output but buffer it until the previous filter terminates. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] overlapping calls to proof-shell-filter
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 mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] overlapping calls to proof-shell-filter
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
Re: [PG-devel] overlapping calls to 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 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.
