[isabelle-dev] performance regression for simp_all

Makarius makarius at sketis.net
Mon Aug 15 22:18:57 CEST 2011

On Fri, 12 Aug 2011, Brian Huffman wrote:

> On Fri, Aug 12, 2011 at 4:07 PM, Makarius <makarius at sketis.net> wrote:
>> http://isabelle.in.tum.de/repos/isabelle/rev/aaaa13e297dc improves startup
>> time of the worker thread farm significantly, and I've got real times in the
>> range of 0.003s -- 0.005s on my "old" machine from 2 years ago with Proof
>> General.
> Thanks for the quick response; with this new patch everything looks much 
> better. Proving "True" and "True" with simp_all in Proof General now 
> takes only 0.002s on my machine.

It also improves the reactivity of Isabelle/jEdit, which has to restart 
the worker farm after some pause in editing.  (Measuring transaction time 
alone is not sufficient.)

These real time interactivity (and interruptibility) issues are hard to 
manage systematically.  If anybody notices similar things, please let me 
know, and I will do my best http://tinyurl.com/3untc57


More information about the isabelle-dev mailing list