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
