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