On 24/01/2022 22:33, Makarius wrote:
In Isabelle/68ffcf5cc94b we now have Poly/ML with updated ARM64
code-generator, see also the announcement by David Matthews on 16-Jan-2022
(http://lists.inf.ed.ac.uk/pipermail/polyml/2022-January/002489.html):
So far it looks pretty good, but we don't have systematic test and
measurements so far.
Here are some measurements on macOS Big Sur for Isabelle/7483347efb4c, with
the following build parameters:
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ISABELLE_BUILD_OPTIONS="threads=4"
ML_OPTIONS="--minheap 1500 --maxheap=10g"
* MacMini8,1 Intel x86_64_32-darwin:
Finished HOL (0:03:08 elapsed time, 0:09:11 cpu time, factor 2.93)
Finished HOL-Library (0:02:49 elapsed time, 0:09:04 cpu time, factor 3.21)
Finished HOL-Analysis (0:05:25 elapsed time, 0:19:00 cpu time, factor 3.50)
Finished HOL-Proofs (0:05:41 elapsed time, 0:10:09 cpu time, factor 1.79)
Finished HOL-Decision_Procs (0:03:21 elapsed time, 0:11:21 cpu time, factor
3.39)
Finished HOL-Data_Structures (0:04:02 elapsed time, 0:14:37 cpu time, factor
3.62)
Finished HOL-Nominal-Examples (0:03:14 elapsed time, 0:11:54 cpu time, factor
3.68)
Finished HOL-ex (0:03:11 elapsed time, 0:11:08 cpu time, factor 3.49)
* MacMini9,1 Apple M1 x86_64_32-darwin (Rosetta 2):
Finished HOL (0:02:47 elapsed time, 0:07:59 cpu time, factor 2.87)
Finished HOL-Library (0:02:24 elapsed time, 0:07:39 cpu time, factor 3.18)
Finished HOL-Analysis (0:05:16 elapsed time, 0:17:12 cpu time, factor 3.27)
Finished HOL-Proofs (0:05:37 elapsed time, 0:09:47 cpu time, factor 1.74)
Finished HOL-Decision_Procs (0:03:50 elapsed time, 0:11:17 cpu time, factor
2.95)
Finished HOL-Data_Structures (0:03:22 elapsed time, 0:12:16 cpu time, factor
3.63)
Finished HOL-Nominal-Examples (0:02:59 elapsed time, 0:10:18 cpu time, factor
3.45)
Finished HOL-ex (0:02:43 elapsed time, 0:09:29 cpu time, factor 3.49)
* MacMini9,1 Apple M1 arm64_32-darwin:
Finished HOL (0:02:18 elapsed time, 0:06:40 cpu time, factor 2.88)
Finished HOL-Library (0:02:04 elapsed time, 0:06:40 cpu time, factor 3.21)
Finished HOL-Analysis (0:04:43 elapsed time, 0:15:24 cpu time, factor 3.26)
Finished HOL-Proofs (0:04:09 elapsed time, 0:07:25 cpu time, factor 1.79)
Finished HOL-Decision_Procs (0:03:01 elapsed time, 0:09:08 cpu time, factor
3.03)
Finished HOL-Data_Structures (0:02:52 elapsed time, 0:10:30 cpu time, factor
3.66)
Finished HOL-Nominal-Examples (0:02:30 elapsed time, 0:08:58 cpu time, factor
3.58)
Finished HOL-ex (0:02:28 elapsed time, 0:08:32 cpu time, factor 3.45)
Remark on the hardware: MacMini8,1 has 6 cores, MacMini9,1 has 8 cores (4
small, 4 big). The build option threads=4 unifies this to some extent, for
better comparison.
Conclusion: the new Apple hardware, Rosetta 2, and the new Poly/ML ARM64
code-generator are all excellent.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
