Re: [isabelle] Isabelle 2014 and proof general

On 09/18/2014 12:25 PM, Thomas Sewell wrote:

This explains why Isabelle/jEdit seems so slow in these cases: the goal
states render in order, while the user waits for output where their
cursor actually is.

I find this a bit curious, as it is my understanding that PIDE's "perspective" mechanism should actually deliver the output to the user's cursor. From Makarius' UITP-2014 paper:

"Activation or deactivation of PRINT tasks is subject to the document perspective. The whole theory library that is edited might be big, but only small parts are visible in the editor. PIDE document processing takes the open text windows as indication where to invest resources for continuous processing."

The perspective not only tells the underlying process which windows is open, but also what command spans ('lines') are in view, and in our Coq incarnation of PIDE, we use this fact: each individual proof is handled by a separate worker process, and the proofs that are in the perspective get priority of processing and printing: in our limited practice, we have seen this gives a better feeling of responsiveness of the prover, as the output is reported where the user's cursor is, even in bigger/slower files.


In the parallel case the window goes white
immediately once the print tasks have forked, from which point there is
no indication of progress, giving the impression the system has just
given up.

Ideally I'd like to see some approximation ProofGeneral's behaviour, in
which many commands can be processed and only one goal state rendered.
Yes, my proofs are pathological, full of applications of fast
methods/tactics but with large complex goal states. I suspect, however,
that I'm not alone.



The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited
accepts no liability for any damage caused by this email or its

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.