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 _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
