[isabelle-dev] Towards the next release

[Makarius]

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