[isabelle-dev] performance regression for simp_all

[Brian Huffman]

Hello all,

Recently I've been hacking on a bunch of proof scripts using the
development version of Isabelle, and I noticed that when processing
proof scripts, I often get a noticeable pause at uses of "simp_all".
The same pause does not occur with Isabelle2011.

Below is a minimal theory file to demonstrate the problem; I ran it
with global timing turned on.

theory Scratch imports "~~/src/HOL/HOL" begin

lemma shows "True" and "True"
by (simp, simp)
(* 0.001s elapsed time, 0.000s cpu time, 0.000s GC time *)

lemma shows "True" and "True"
by simp_all
(* 0.253s elapsed time, 0.004s cpu time, 0.000s GC time *)

I'm using an old, slow machine, so maybe 0.253s is a bit long compared
to what most people will see. On the other hand, in terms of the
slowdown ratio, 0.1s or even 0.05s would be pretty bad.

Here's what I learned by doing "hg bisect":

The first bad revision is:
changeset:   42372:6cca8d2a79ad
user:        wenzelm
date:        Sat Apr 16 23:41:25 2011 +0200
summary:     PARALLEL_GOALS for method "simp_all";

http://isabelle.in.tum.de/repos/isabelle/rev/6cca8d2a79ad

Was this change supposed to *improve* performance? Was the performance
impact tested? Maybe the performance penalty only appears when
interactively stepping through proofs, and not in batch mode?

- Brian