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

   At a quick glance this looks like a reasonable way to fix without
   messing with the current filter code.  Luckily, I don't think the str
   argument is used.  

   I'm not completely clear on the error case, is the
   idea just to give up if we hit an error in some call?

If proof-shell-filter signals an error, the error is just
propagated, only the active flag is reset to enable later calls

Or do you mean the case where a parallel, overlapping call is
detected? In this case the -was-blocked flag is set and the
already running instance of the wrapper stays for one more
iteration in the while loop, thus calling proof-shell-filter
after the previous call finished.

This effectively delays Coq until prooftree catches up. This is
just what you want, I believe. 

Under normal circumstances prooftree is much faster than Coq.
Because of the experience with PVS, where the proof tree
visualizer was often the bottleneck, I made some special

- tree layout is linear in the tree depth; for PVS it is
  apparently worse than linear in the number of nodes

- tree display is delayed until no display commands are available
  on input; nevertheless, when asserting large regions, you see
  the tree growing node by node, indicating that prooftree is
  faster than Coq


ProofGeneral-devel mailing list

Reply via email to