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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
