Andreas Lochbihler

2016-07-07 08:09:17 UTC

Dear Isar experts,

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?

As the delays also appear inside proofs (i.e., not for top-level lemma statements), I

suspect that attributes and propagation of facts to locale interpretations are not to be

blamed.

My machine is still the usual one:

Linux lenovoal 3.13.0-91-generic #138-Ubuntu SMP Fri Jun 24 17:00:34 UTC 2016 x86_64

x86_64 x86_64 GNU/Linux

Intel(R) Core(TM) i7-3630QM CPU @ 2.40GHz

16GB of RAM

Thanks in advance,

Andreas

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?

As the delays also appear inside proofs (i.e., not for top-level lemma statements), I

suspect that attributes and propagation of facts to locale interpretations are not to be

blamed.

My machine is still the usual one:

Linux lenovoal 3.13.0-91-generic #138-Ubuntu SMP Fri Jun 24 17:00:34 UTC 2016 x86_64

x86_64 x86_64 GNU/Linux

Intel(R) Core(TM) i7-3630QM CPU @ 2.40GHz

16GB of RAM

Thanks in advance,

Andreas