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