Re: [isabelle] qed and done take long for large goal states

On 10/08/16 14:50, Andreas Lochbihler wrote:
> I had thought that results are printed asynchronously already. At least,
> the Isabelle NEWS file for 2013-1 says
>   * Support for asynchronous print functions, as overlay to existing
>   document content.
> If results do not take part in that so far, I think this would be a good
> time to do so.

The asynchronous printing of 2013 only applies to official command
transaction states, i.e. the subsequent proof state.

We are talking about unofficial side-results here: verbosity produced by
certain commands on their own account.

To make this asynchronous requires some care, because the order of
results should remain stable.

> By the way, I remember two particular "lemmas" commands in JinjaThreads
> (Compiler/J1JVMBisim around line 1055) which manipulate induction rules
> for inductively defined bisiumlation relations (especially "split_format
> (complete)"). Their processing took ages back then with ProofGeneral
> because of the pretty printing.

I can imagine that the system spends a good portion of time on
"potentially useful output", often more than performing proof steps.


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