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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
