Re: [isabelle-dev] Quickcheck Examples
On Mon, 27 Feb 2012, Lukas Bulwahn wrote: 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. In principle the codegen infrastructure and all should work in parallel, but there might be additional oddities in the quickcheck scenario. You can reproduce the presumed non-termination on macbroy2 with regular settings like this: ISABELLE_USEDIR_OPTIONS=-i false -d false -M 4 -q 2 ML_PLATFORM=x86_64-darwin ML_HOME=/home/polyml/polyml-5.4.1/x86_64-darwin ML_SYSTEM=polyml-5.4.1 ML_OPTIONS=-H 1000 --gcthreads 4 The process is running with approx. 100-200% most of the time, which is neither sequential nor fully parallel. Probably you merely benefit from theory parallelism, not from more fine-grained Par_List things that could be used in your own code. One potential source of problems is the pseudo-random generator, with its global state. There have been funny effects in the past that might have come back in one form or the other, even though random generators have been changed several times. Anyway, how long does the session run on "your laptop"? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
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
