[isabelle-dev] performance regression for simp_all

[Makarius]

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


 	Makarius