Re: [isabelle-dev] Analysis not building
Florian Haftmann wrote: > > HOL-Analysis can’t be built (reproducibly) with the latest version > > (76f2d492627e). It simply dies, no error message. > > I cannot reproduce this. Neither can I; using polyml-b68438d33c69 I can build HOL-Analysis with Isabelle-24bbc4e30e5b and manual init-component for Poly/ML and both HOL-Analysis and IsaFoR with Isabelle-2018 and the same manual init-component. Maybe this is somehow specific to OS/X, which I believe Larry uses? That said, polyml-1b2dcf8f5202 seems to work just as well, for me. In other news, the problem with the sharing pass appears to be resolved and the IsaFoR images with x86_64_32 are now all about 60% the size of the x86_64 ones. Nice! Cheers, Bertram Numbers: ML_PLATFORM="x86_64_32-linux" ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6" ISABELLE_BUILD_OPTIONS="threads=10 parallel_proofs=2" polyml-test-1b2dcf8f5202 polyml-test-b68438d33c69 Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14) Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14) Finished HOL (0:02:23 elapsed time, 0:08:49 cpu time, factor 3.68) Finished HOL (0:02:26 elapsed time, 0:08:58 cpu time, factor 3.69) Finished HOL-Lib (0:05:12 elapsed time, 0:32:06 cpu time, factor 6.17) Finished HOL-Lib (0:04:58 elapsed time, 0:31:08 cpu time, factor 6.25) Finished HOL-AFP (0:05:40 elapsed time, 0:32:52 cpu time, factor 5.79) Finished HOL-AFP (0:05:38 elapsed time, 0:32:51 cpu time, factor 5.82) Finished IsaFoR_1 (0:05:10 elapsed time, 0:27:31 cpu time, factor 5.32) Finished IsaFoR_1 (0:05:11 elapsed time, 0:27:39 cpu time, factor 5.33) Finished IsaFoR_2 (0:05:26 elapsed time, 0:25:37 cpu time, factor 4.71) Finished IsaFoR_2 (0:05:27 elapsed time, 0:25:37 cpu time, factor 4.69) Finished IsaFoR_3 (0:06:38 elapsed time, 0:39:22 cpu time, factor 5.92) Finished IsaFoR_3 (0:06:36 elapsed time, 0:39:24 cpu time, factor 5.96) Finished IsaFoR_4 (0:08:26 elapsed time, 0:26:28 cpu time, factor 3.14) Finished IsaFoR_4 (0:08:37 elapsed time, 0:26:55 cpu time, factor 3.12) Finished Code (0:08:03 elapsed time, 0:08:11 cpu time, factor 1.02) Finished Code (0:08:02 elapsed time, 0:08:11 cpu time, factor 1.02) 19271289 Pure (0.69 x 28081037 (x86_64 heap image size)) 19269857 Pure (0.69) 250024211 HOL (0.61 x 410972244) 250129275 HOL (0.61) 307851090 HOL-Lib (0.59 x 525949867) 307921910 HOL-Lib (0.59) 537798522 HOL-AFP (0.59 x 913422879) 537694918 HOL-AFP (0.59) 428162386 IsaFoR_1 (0.59 x 724672759) 427425094 IsaFoR_1 (0.59) 367783763 IsaFoR_2 (0.59 x 623083120) 367626511 IsaFoR_2 (0.59) 419599023 IsaFoR_3 (0.59 x 712211696) 419246195 IsaFoR_3 (0.59) 284804855 IsaFoR_4 (0.59 x 480209352) 284701607 IsaFoR_4 (0.59) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
On 02/02/2019 15:37, Lawrence Paulson wrote: > This worked — thanks! > >> On 2 Feb 2019, at 13:56, Makarius wrote: >> >> Can you try the following in your $ISABELLE_HOME_USER/etc/settings? >> >> init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202" OK. With Isabelle/76f2d492627e this is the default, and it is better to remove the init_component from local etc/settings again, to participate in further updates of the default. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
This worked — thanks! Larry > On 2 Feb 2019, at 13:56, Makarius wrote: > > Can you try the following in your $ISABELLE_HOME_USER/etc/settings? > > init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202" > > Apparently, the last two updates on polyml-test were not as monotonic as > I was hoping, despite clear improvements by David Matthews. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
On 02/02/2019 14:56, Makarius wrote: > On 02/02/2019 14:39, Lawrence Paulson wrote: >> It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle >> jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”. >> >> The reason I fetched in the first place was that I was getting crashes in my >> interactive sessions. > > Can you try the following in your $ISABELLE_HOME_USER/etc/settings? > > init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202" > > Apparently, the last two updates on polyml-test were not as monotonic as > I was hoping, despite clear improvements by David Matthews. > > After a standard test, I will probably make the above version the > default again. I've done that now in Isabelle/dde776d1defa, after successful "isabelle build -a". Thus we are at least back to the status-quo from some days ago, where nobody noticed everyday crashes. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
On 02/02/2019 14:39, Lawrence Paulson wrote: > It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle > jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”. > > The reason I fetched in the first place was that I was getting crashes in my > interactive sessions. Can you try the following in your $ISABELLE_HOME_USER/etc/settings? init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202" Apparently, the last two updates on polyml-test were not as monotonic as I was hoping, despite clear improvements by David Matthews. After a standard test, I will probably make the above version the default again. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”. The reason I fetched in the first place was that I was getting crashes in my interactive sessions. Larry > On 2 Feb 2019, at 13:26, Florian Haftmann > wrote: > >> HOL-Analysis can’t be built (reproducibly) with the latest version >> (76f2d492627e). It simply dies, no error message. > > I cannot reproduce this. > > ML_PLATFORM="x86_64_32-linux" > ML_SYSTEM="polyml-5.7.1" > ML_OPTIONS="--maxheap 9G" > > Have you tried a fresh build or delete the corresponding log / saved > state manually? > > Cheers, > Florian > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
> HOL-Analysis can’t be built (reproducibly) with the latest version > (76f2d492627e). It simply dies, no error message. I cannot reproduce this. ML_PLATFORM="x86_64_32-linux" ML_SYSTEM="polyml-5.7.1" ML_OPTIONS="--maxheap 9G" Have you tried a fresh build or delete the corresponding log / saved state manually? Cheers, Florian 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] Analysis not building
HOL-Analysis can’t be built (reproducibly) with the latest version (76f2d492627e). It simply dies, no error message. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
