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/[email protected]/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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
