[isabelle-dev] Towards the next release

[Makarius]

On Thu, 19 Apr 2012, Gerwin Klein wrote:

>> What happens in b) is much more ambitious, and if this is really a 
>> bottleneck, an option like »record_quickcheck« could do the job.
>>
>> But I think before to settle here it is important to have more detailed 
>> benchmarks about records which separates figures for a) and b). 
>> Commenting out ensure_random_record and ensure_exhaustive_record in 
>> function add_code coulde make a good start.
>
> My feeling is that the problem already occurs in a), but you are right, 
> this needs to be confirmed. I'll measure and see how things go.
>
> 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.
>
>
>> Also note that most of the quickcheck addons are by Lukas, not me ;-)
>
> Sorry, I had just assumed that anything that looks like code generator 
> is in your domain ;-)

There further unclarities with quickcheck still pending.  See the open 
thread from almost 2 months ago: 
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02254.html

Moving HOL-Quickcheck_Examples to the "full" target was just an immediate 
reaction to make things not fully untested, so that the problem can be 
sorted out without a real-time pressure.

Now we do have a real time pressure, because the point zero of 
Isabelle2012 is in less than 2 weeks.


 	Makarius