[isabelle-dev] Towards the next release
makarius at sketis.net
Thu Apr 19 13:04:59 CEST 2012
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
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
More information about the isabelle-dev