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