[isabelle-dev] Analysis not building

[Bertram Felgenhauer]

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)