[isabelle-dev] performance regression for simp_all

Brian Huffman brianh at cs.pdx.edu
Sat Aug 13 02:00:12 CEST 2011


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.

- Brian



More information about the isabelle-dev mailing list