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 finished. 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'' argument? 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 ready. (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. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
