Re: [isabelle-dev] Quickcheck Examples
On Fri, 20 Apr 2012, Lukas Bulwahn wrote: On 02/27/2012 02:31 PM, Makarius wrote: 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"? I have not noticed that non-termination on my laptop when checking my changesets. Also with the setting mentioned above, I could not reproduce the non-terminating behaviour on macbroy2 with changesets baf90cb2a606. I will continue testing Quickcheck-Examples to see if it only occurs infrequently. My observation on 27-Feb-2012 was still very crude, I've updated that in a private mail on 16-Mar-2012. In particular, "nontermination" means "termination after 1-2 hours", and it is independent of parallelism: http://isabelle.in.tum.de/devel/stats/at-poly/HOL-Quickcheck_Examples.png http://isabelle.in.tum.de/devel/stats/mac-poly-M4/HOL-Quickcheck_Examples.png The isatest settings are in Admin/isatest/settings/. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
On 04/20/2012 02:12 PM, Lukas Bulwahn wrote: On 02/27/2012 02:31 PM, Makarius wrote: 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"? I have not noticed that non-termination on my laptop when checking my changesets. Also with the setting mentioned above, I could not reproduce the non-terminating behaviour on macbroy2 with changesets baf90cb2a606. I was mistaken--I was checking with f5eaa7fa8d72. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
On 02/27/2012 02:31 PM, Makarius wrote: 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"? I have not noticed that non-termination on my laptop when checking my changesets. Also with the setting mentioned above, I could not reproduce the non-terminating behaviour on macbroy2 with changesets baf90cb2a606. I will continue testing Quickcheck-Examples to see if it only occurs infrequently. Can you other system configurations by running the isatest with the "full" target? Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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
Re: [isabelle-dev] Quickcheck Examples
On Fri, 24 Feb 2012, Lukas Bulwahn wrote: Maybe we could also get performance measurements for the new session? See now 1258eab48270. I have also updated the IsaMakefile itself in 2190af0ef263. All this redundancy in the session management is well-known and waiting to be eliminated for many years. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
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
Re: [isabelle-dev] Quickcheck Examples
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) 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) Maybe we could also get performance measurements for the new session? I hope it facilitates maintenance nevertheless. Although if Quickcheck fails (or does not terminate) after some changes, this usually indicates that there is some flaw in the code generation setup. 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. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
> I guess there are no voices at all. If you have strong feelings for yet > another session, I can go ahead and split the theories. I would appreciate that, thanks a lot. Btw. recently I was able to delete a remarkable amount of dead code from quickcheck_narrowing (unfortunately it is not in the main branch, but in Brian's numerals fork). Maybe you would like to inspect all those quickcheck modules for such things. 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
Re: [isabelle-dev] Quickcheck Examples
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. Are there any voices pro or contra? IMHO the overhead when figuring out (frequently occurring) non-termination problems in HOL-ex is not tolerable at the moment, so a fat cure would be reasonable. I guess there are no voices at all. If you have strong feelings for yet another session, I can go ahead and split the theories. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
> 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. Are there any voices pro or contra? IMHO the overhead when figuring out (frequently occurring) non-termination problems in HOL-ex is not tolerable at the moment, so a fat cure would be reasonable. 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
[isabelle-dev] Quickcheck Examples
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. Florian -- Home: http://www.in.tum.de/~haftmann 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
