[isabelle-dev] Quickcheck Examples

Makarius makarius at sketis.net
Mon Feb 27 12:22:35 CET 2012


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



More information about the isabelle-dev mailing list