[isabelle-dev] Poly/ML x86_64_32 available for testing (polyml-test-a444f281ccec)

[Makarius]

On 23/01/2019 23:44, Makarius wrote:
> Isabelle/20bc1d26c932 now provides an updated polyml-test-a444f281ccec
> (active by default).
> 
> It performs slightly better than the previous test version -- I have
> also removed old workarounds for integer arithmetic in
> Isabelle/4591221824f6.

One more performance result in this respect:

Isabelle/4591221824f6 + AFP/2eacf2ed7d5d

x86_64_32-linux --minheap 1500 threads=8

Finished Flyspeck-Tame (3:37:32 elapsed time, 5:32:38 cpu time, factor 1.53)

This is a about two times better than what we were used to. It is a
combination of high-end software (current Poly/ML) with high-end
hardware (Intel Xeon Gold 6148 CPU @ 2.40GHz, 20 CPU cores, 64 GB
memory, SSD).


	Makarius