On Thu, 19 Apr 2012, Gerwin Klein wrote:
Btw, it's easy to reproduce: just make a theory file based on HOL
(Main.thy) that defines a record with 600 fields. Run it in
Isabelle-2009-1 and the current version for comparison.
We also have a semi-active src/HOL/Record_Benchmark for quite some time --
it goes back to formerly passive theories by Norbert Schirmer. This is
run by isatest via the special "full" target, which is meant to measure
things that don't need to be tested otherwise. Here are some recent
statistics
http://isabelle.in.tum.de/devel/stats/mac-poly64-M4/HOL-Record_Benchmark.png
Formally, one can imagine the record package to provide a few boolean
options "record_codegen", "record_quickcheck" etc. to control certain
features in an agnostic way.
One needs to make sure that such feature variants are routinely tested.
One should also try hard to understand the actual issues that are worked
around here.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
