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

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

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

2019-01-23 Thread Makarius 
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.


It is important to check that obsolete entries in
$ISASELLE_HOME_USER/etc/settings are cleaned up, such that this greatest
and latest version gets used.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev