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



On 07/07/16 10:02, Andreas Lochbihler wrote:
> 
> I am looking for ways to speed up the processing of some of my Isar
> proofs. Something I noticed is that when there are no subgoals left,
> "done" and "qed" nevertheless take between 2 and 7 seconds of processing
> (according to the Isabelle timing panel in jEdit).
> 
> I guess that the delays must have something to do with the size of the
> statement being proved. They only occur for large proof states. For
> example, large elimination rules (with approx. 20 cases) or the cases
> for induction proves about functions defined with partial_function. The
> delays are particularly annoying for the latter case, because each
> induction proof has many subcases and the delay occurs for each of the
> subcases.
> 
> Are there any options or tweaks to speed up the processing of qed/done?

There might be various "after_qed" bookkeeping steps that take long,
notably in derived definitional packages like 'function' or
'partial_function'.

Moreover, there could be genuine bottle-necks in the standard export
operations and re-adjustment operations performed at the end of a proof.


If you can point to a concrete example that is particularly slow, I can
take a look at profiling information and make more educated guesses.


	Makarius





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