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