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