[isabelle-dev] performance regression of typedef command
brianh at cs.pdx.edu
Fri Mar 26 08:43:04 CET 2010
Recently I was working on a theory file containing several typedefs. I
noticed that Isabelle seemed sluggish when executing the typedef
commands, so I loaded up the old heap image from Isabelle 2009 to
compare. Here's the simple typedef command I tested:
typedef 'a foo = "UNIV :: 'a set set"
In Isabelle 2009, the typedef takes about 5 hundredths of a second on
my machine, with another few hundredths for the "by simp" part.
In the current development version, with the new "local theory"
typedef package, the typedef takes nearly *half a second*. With
software in general, I think slowdowns of 10 or 15% are tolerable when
there is some significant benefit (better reliability, for example) to
offset the performance penalty. But this is TEN TIMES AS SLOW! The "by
simp" part has a similar slowdown factor, and takes another quarter of
In exchange for the extreme slowness, we get the ability to use
typedef commands inside locales.
Could someone explain to me why they think this is a good tradeoff?
More information about the isabelle-dev