[isabelle-dev] performance regression of typedef command

[Brian Huffman]

Hello all,

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"
by simp

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
a second.

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?

- Brian