David Aspinall <david.aspin...@ed.ac.uk> writes:

   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?

I don't use the debugger, I let certain functions insert start
and end messages into a dedicated buffer. There, I see 
proof-shell-filter starting before the previous instance

In principle, the problem can also appear without prooftree.
Proof General will block when sending a sufficiently large
command. If the proof assistant generates output before
completely reading the command, proof-shell-filter might get
called a second time. The command has to be really large, because
default pipe size is 64K since Linux 2.6.11.

   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.  

Yes, using a second flag to remember aborted nested calls, such
that proof-shell-filter can call itself recursively if a nested
call was aborted.

Am I right, that proof-shell-filter does not use its ``str''

Because the problem does only appear when starting prooftree with
cold disk caches (which takes more than 1 sec on my laptops), a
partial fix would be to block Proof General until prooftree is

   (Or could you do that just for proof tree?)

I don't understand. The problem appears, because it takes more
than one second until prooftree is ready and Coq + Proof General
generate more than 64K display commands in that time. 


ProofGeneral-devel mailing list

Reply via email to