[isabelle-dev] Poly/ML x86_64_32 available for testing
makarius at sketis.net
Sun Jan 27 21:26:14 CET 2019
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
There was indeed something odd with sharing: David Matthews has changed
that in polyml-1b2dcf8f5202 (see Isabelle/bb0a354f6b46).
> i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD
> Common build flags:
> ISABELLE_BUILD_OPTIONS="threads=12 parallel_proofs=2"
> 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.
More information about the isabelle-dev