[isabelle-dev] Poly/ML x86_64_32 available for testing

[Makarius]

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