Email Gateway (Feb 08 2021 at 22:09): Email Gateway (Feb 08 2021 at 22:09):From: Makarius <makarius@sketis.net>
The announcement now says:
* Support for macOS Big Sur on Intel and Apple Silicon (ARM).
For RC5 the main change is "Improved support for Apple Silicon (ARM): external
processes are managed by Isabelle/Scala instead of Apple's Rosetta (which does
not support multithreaded process fork)."
Thus sledgehammer works properly, and as far as I can see everything else as well.
I also managed to run complete Isabelle + AFP twice: it takes approx. 12h for
one run. Detailed timings are included for the following setup:
Hardware: Macmini9,1, Apple M1 CPU with 4 cores * 2 (hyperthreading), 16GB RAM
macOS Big Sur 11.2
Isabelle/da0ee7fbc068 (approx. Isabelle2021-RC5)
AFP/07ea995a6665 from afp-2021 repository
etc/settings:
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ML_PLATFORM="x86_64_32-darwin"
ML_OPTIONS="--minheap 1500 --maxheap=10g"
isabelle build -o threads=4 -d '$AFP' -a -X very_slow
For comparison, here are timings for Isabelle on the last generation of Intel
Mac Mini (Macmini8,1, 6-Core Intel Core i7, 64 GB RAM):
https://isabelle.sketis.net/devel/build_status/macOS_11.1_Big_Sur_4_threads/index.html
Overall the Apple Silicon machine is pretty impressive: slightly faster than
the Intel one. Note that 16 GB is presently the upper bound for that new
generation of Mac Minis, while the older generation supported 64 GB.
Makarius
nohup.out
Email Gateway (Feb 13 2021 at 12:57):From: Makarius <makarius@sketis.net>
Here are side-by-side measurements of the last two generations of Mac Minis.
Overall setup:
Isabelle2021-RC5 (approximately, with minor/irrelevant variations in the
changeset ids)
AFP/9a6ed530ce81 (afp-2021 branch)
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ML_PLATFORM="x86_64_32-darwin"
ML_OPTIONS="--minheap 1500 --maxheap 10g"
isabelle build -o threads=4 -d '$AFP' -f -g slow
Machines:
(1) Intel: Macmini8,1, i7 CPU with 6/12 cores, 64 GB RAM, SSD storage, macOS
11.2
(2) Apple Silicon: Macmini9,1, M1 CPU with 4/8 cores, 16 GB RAM, SSD
storage, macOS 11.2.1
The counting of CPU cores has become more difficult than before: Intel has its
traditional notion of hyperthreading, but Apple M1 has a different notion of
big vs. little cores. Poly/ML reports 6 cores on (1) and 8 cores on (2).
For the measurements, I have enforced 4 worker threads in Isabelle/ML and
restricted the heap size such that the Macmini9,1 still feels comfortable: it
has only 16 GB (at maximum), while the older Intel Mac Mini has 64 GB (at
maximum).
The results for AFP "slow" are included in the attachment. The new Apple
Silicon machine is slightly faster, even with the runtime translation of
Poly/ML x86_64 code to ARM64 via Rosetta 2.
Some notable results:
intel.log:Finished HOL (0:02:53 elapsed time, 0:07:52 cpu time, factor 2.72)
apple.log:Finished HOL (0:02:45 elapsed time, 0:07:22 cpu time, factor 2.67)
intel.log:Finished AODV (1:14:08 elapsed time, 4:06:45 cpu time, factor 3.33)
apple.log:Finished AODV (0:58:25 elapsed time, 3:16:21 cpu time, factor 3.36)
intel.log:Finished Flyspeck-Tame-Computation (2:38:30 elapsed time, 3:58:26
cpu time, factor 1.50)
apple.log:Finished Flyspeck-Tame-Computation (2:36:44 elapsed time, 3:56:57
cpu time, factor 1.51)
intel.log:Finished ConcurrentGC (0:13:35 elapsed time, 0:51:12 cpu time,
factor 3.77)
apple.log:Finished ConcurrentGC (0:12:27 elapsed time, 0:46:32 cpu time,
factor 3.74)
In conclusion, I am pleased to declare Apple Silicon M1 (and macOS 11 Big Sur)
as fully supported by the Isabelle2021 release (which is to be published
towards the end of next week).
Side-remark: This rather quick adoption of quite different new hardware has
been possible thanks to a generous donation of a Macmini9,1.
Last updated: Jan 04 2025 at 20:18 UTC