On 25/01/2019 20:29, Bertram Felgenhauer wrote: > > - While most heap images are about 40% smaller with x86_64_32, this is > not always the case; some heap images ended up being even larger in > this experiment. Could there be a problem with the sharing pass on > x86_64_32?
There was indeed something odd with sharing: David Matthews has changed that in polyml-1b2dcf8f5202 (see Isabelle/bb0a354f6b46). > Hardware: > i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD > > Common build flags: > ISABELLE_BUILD_OPTIONS="threads=12 parallel_proofs=2" > > Configurations: > polyml 5.7.1 x86_64 ML_OPTIONS="--maxheap 24G -H 500 --gcthreads > 6" > polyml-a444f281ccec x86_64 ML_OPTIONS="--maxheap 24G -H 500 --gcthreads > 6" For this hardware I recommend threads=6. Moreover note that --gcthreads is automatically provided, if ML_OPTIONS does not say anything else. > 623083120 IsaFoR_2 (1.00) > 623291272 IsaFoR_2 (1.00) > 367497971 IsaFoR_2 (0.59) > 884213127 IsaFoR_2 (1.42) ? I have briefly tried IsaFoR_2 and now get 624867156 (1.00), which is better but still slightly odd. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev