[isabelle-dev] Quickcheck Examples

[Lukas Bulwahn]

Thanks a lot for your help.

A large part of Quickcheck's run time is spent in the code generator 
calls, and the evaluation, which does mostly memory allocations and 
deallocations.
I am surprised that this issue suddenly occurs now that it is its own 
session. Maybe the many parallel invocations of Quickcheck now pressure 
the ML compiler much more than as it was just a part of HOL-ex.


Lukas

On 02/27/2012 12:22 PM, Makarius wrote:
> There are further problems with HOL-Quickcheck_Examples.  In recent 
> repository versions it does not terminate so well -- I've stopped 
> trying after approx. 1h CPU time.  (Aside: judicious use of Par_List 
> operations could improve quickcheck tools significantly.)
>
> The removal of Find_Unused_Assms_Examples in b07ae33cc459 does not 
> help either.  In fact it is a bad idea to leave untested things in the 
> repository, they will start to rot and to smell rather quickly.
>
> So in 879f5c76ffb6 I've now moved the whole problem session to the 
> "full" target of the IsaMakefile.  This is only run by some isolated 
> isatest sessions, probably not mira.
>
> This gives the opportunity to isolate all these issues, without 
> degrading productivity of everybody else.  (The makeall all turnaround 
> time is critical to the ever ongoing maintanence process; it used to 
> be 10min a few years ago, then 20min, now it is approaching 30min again.)
>
>
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>