Hi Lukas, Am 24.02.2012 09:09, schrieb Lukas Bulwahn: > On 02/18/2012 10:18 AM, Florian Haftmann wrote: >>> How much relative time do the quickcheck examples in HOL-ex take? >>> According to my feeling time could be high to separate these into a >>> separate session, to facilitate maintenance. >>> > I separated the Quickcheck-Examples from HOL-ex into an own session (cf. > http://isabelle.in.tum.de/repos/isabelle/rev/f462e49eaf11)
thanks a lot. > The latest performance numbers do not show that the run time reduced, so > either there is really another bottleneck or my own change has not had > any effect on the measurements yet? > (cf. http://isabelle.in.tum.de/devel/stats/at-poly/HOL-ex.png) Now it had. > If Library-Codegenerator-Test works, you only know that you get source > code that compiles correctly. > With the Quickcheck-Examples session, you know that the source code also > runs correctly. On the other hand, Library-Codegenerator-Test is more pervasive. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
