Re: [isabelle] Isabelle2021-RC5: support for Apple Silicon
- To: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- Subject: Re: [isabelle] Isabelle2021-RC5: support for Apple Silicon
- From: Makarius <makarius at sketis.net>
- Date: Sat, 13 Feb 2021 13:49:20 +0100
- Authentication-results: mx2f26; spf=pass (sender IP is 62.216.204.123) smtp.mailfrom=makarius at sketis.net smtp.helo=[192.168.178.32]
- Autocrypt: addr=makarius at sketis.net; prefer-encrypt=mutual; keydata= mQINBFcrF+4BEADMcXMnu3XHg6bRsGe3tajAHqvm89+ecn/Y0WhjI2FplhkZs1LwM+ZA9eXh hiBrC/yX0FJ+qjzVIfm66CX4nzVG1f8qwaervMpvpA+gbhtQiXc0t+LDcqV+5cdtpKplPHSu oW+KzJKyCdkDB5fYMOzuaXQwYi12YAEQH2r6K7Q7Np+k82Xli1pWe+Tha/BH0pKJ5Q01aPep ASrNW9F+moX7C0fxWl65LiXGmF0UJep6fqKruhy8oNF4p6I2oZhktvaR/x6tkL2PkT3r+xUS 6g5i3BOjfwhoGY57nsioeK+8VFvdRH5DK4CbrTgDl7ddcrEeENrfpDiPLs/afVbe/T9oDXmJ OJAO4WMpfZNiFhx9SSVTHohw29Fyzn0N1UQGjPqAY1jg32DAxlnMQ0co/KabEFAcoQsW1/6U ZGiNxYVIyEKGrnSY4WuLuNC8CmU1RaYSdTk1y9tYdxufM9lH9ynzJwac6FdalOOxMR2G9JG8 L9/dk3ytlP6DVwkPBSCpJaTkTyMp1wSkF1oK/BDu5xKUQh0zvvLCuZ16hiKRBBSjpVExXRZC u+NC1Y4wqm1HOH7HBwgZ1Hv9S/EPmI9iwgcW0SpDJqPf2Cm7oFMZsZ5Dbs6/nOQoe4Zegy45 ymqDRlIekP7zj+vOoR80XAYfmAH5DElJHldcjmgLBMdpvvqGZwARAQABtB5NYWthcml1cyA8 bWFrYXJpdXNAc2tldGlzLm5ldD6JAj0EEwEIACcFAlcrF+4CGyMFCQlmAYAFCwkIBwIGFQgJ CgsCBBYCAwECHgECF4AACgkQ89KUEoG/TbiVrw/9FjEBgh2CB7Qof7Y4k0yc7j+x/A0Wmkc0 iwP5jaKJuxRv1JJT8CFqm392+/cdh3EkRUk/UWD+hpNndYJwxZltrEpKVqFAWoVOg3ZJ4cuI MYhlp4tk/T0KSl/gKT16dc6uJ7M/FzW0zv50vjFtAdianEDuqLXHKaGDUwWoOTDly0gdZ7aH /eNby6ONHUSJMdTNOErh2N+uESM4aZqUuuL/dTb6xiVzCpV5saT8EMakoazUd7QhoBaHvqfs BL7DEmvcTtA79GF3ufHrF/UndIcx8aMznZ2PGNjmy5seDCoKX0EYHdLam8vgo/TuU4dRw5Zn 6E/ouyNOliXT1Mn+SomeBSXTR5MXRq4TQ9MKVGiP0Yl+7GJQU0JFtDC1ZZEOyjIiwGWOhbUR pYujVm8C1iQ7NcEn2BqOAmRML6IR6+En4RLbgCNsBNXlmTPRJOaI+iV6DZzg3x9zcaDGhoYt jkBTEFpb0F3jU9yuaEU5401NV34fUxg8tqXs0R9CKinO7kQ8N+RDjyyY8k2KZiDYBJ6r+OK0 d7TaTj7F9tmpAu2pmQ8lxOKjDZIwlbGTsC4lxISmcPzBGTKXja5nakcWYx/lZ4vje0WZ12HN amnD1weakFixRYit0d+Kz7cuj684NSbhwC0oN2t9R06Nfq8UPEWRKEitCly0OtRgio8zVZ/L eAC5Ag0EVysX7gEQAKs5NVOvYkE/r8KLsJ8/L/9eulpJDOFilZ9fyuqii7t1UpHZLb58QghW JM+IB2GSGsB+pOi6Je7hmwxcVdXYbGlYZ4Btqqw48/XptfbNZ8alCk6AqoVFP4MbYxij/Qqv f/Yw6GR0p1RIC/W4GF/JgDDwDFEiMT6Pv6dpM8acdNFCERDZdoOJiC+XJRwy5lZ2g5FOJkT9 rVI9EnA7mBXLLjPOMUp2/eZxN6gKOZzI3ej9vixg3adWR2yfKPgacHP/ujnVfITOl0OyLE5f zIHq85dEV4zW6Mpx7+Um0tdkwlUVMaW2nQ1bcwejgVAuD/MLSF/lSs3N5D1ctw5QUemYh7/e 2dC12UJuFDFxNPzcltQTlkBCVWV1D0SjScDHdlF6HhzpZOlt52/rwTn5GHtY4nwAL4IJ+Yvl WX8YKmyILH4Ai8c/N2IVRERQ2qorWFlsQnqrXV+hXf8aUwjc/pq4K9rsWxvle3TpeZfoBefU /s1PEX0SepZFAqAXHlQ9DZPsdPDo9EFK695G5w4nf03EhE9TV1MKGUuc1XJ6f1ZLaxu0TwTA 6qYtKIyBcU0Yn61S2Kh7Dgb5LdLV8nfl71+n/xIt2IWH5UJ9YuwEgGEP0c6ImnAUZ+nRodFI 0RwtCWlRkSJWtQln1vcphrz8PjWZH6e/nWnceXR/Al5P0WexQgtvABEBAAGJAiUEGAEIAA8F AlcrF+4CGwwFCQlmAYAACgkQ89KUEoG/Tbh7VQ/9Fc4bdwJYc3jH/LiuXv6uMg50Cv6lg2NT bL9DClWGNiYzejfM2A4c5K+GRUXhyD7S9U203MOv3z7uTbtyQL8XVolNnQlRIkB00f8nJ2sw HMXx/hemjXBvtlneq+vrMORJexldXUMFq19ZZrvj0zZL+pUnGFqt+IWTEE5GpL7wu20Demaj jYyGyKcDZyJOWZcl4e45Yn3hl0EI2xVmVh7ZinVsb3+nqgcltFy4Jt+drezwV2EiLGJHfGsT jEQb3C9VpneU4Jo+hHtfqLK4Q8+WlIOzSfyvwbabxrhyqg7i11fu8yckNW3dCURPYigV07HK 4dN0zhj53M0Q3eTwegJRPJb8XoLDcSdbsaU2HIShlGDKmzS9KL4JzLikQ9dXROC4cae3jRKH aexFi4B55Ab6FxIfXj09wUCO6Nm0owDfIBDMgiywvi2Rb2etCjBgRbSj71S2nntd9ZitoYvE yKirLkWmJRbp3ln8cHi8Uc/jr1cDPVRWuLUN0uceMj5+AR+NZVakcNUHWJCinMMjacho0SyP QmocdU8pzzupreaVWruqaSzqcpWBPwrE5OxEtJ+OyIBjKmRJ5eptjh4rKgNaVnKjhqbvr+Yz pUAgPp38jjf4HJghUGIfWArKNelKJEJOYk94DAbmT67LgqEdZ0yaA2BCHmreN727WIzV9vkX NMc=
- In-reply-to: <c3614ccb-a505-1735-9367-c4f25f3882b6@sketis.net>
- References: <710bf85d-0628-a7dd-75e6-9709488313a2@sketis.net> <c3614ccb-a505-1735-9367-c4f25f3882b6@sketis.net>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0
On 08/02/2021 23:09, Makarius wrote:
> On 08/02/2021 22:42, Makarius wrote:
>
>> Presumably the last release candidate is
>> https://isabelle.sketis.net/website-Isabelle2021-RC5
>
> 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.
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.
Makarius
Building Pure ...
Finished Pure (0:00:12 elapsed time, 0:00:12 cpu time, factor 0.97)
Building HOL ...
Finished HOL (0:02:53 elapsed time, 0:07:52 cpu time, factor 2.72)
Building Flyspeck-Tame ...
Finished Flyspeck-Tame (0:01:11 elapsed time, 0:03:32 cpu time, factor 2.98)
Running Flyspeck-Tame-Computation ...
Finished Flyspeck-Tame-Computation (2:38:30 elapsed time, 3:58:26 cpu time, factor 1.50)
Building AWN ...
Finished AWN (0:00:45 elapsed time, 0:02:00 cpu time, factor 2.68)
Running AODV ...
Finished AODV (1:14:08 elapsed time, 4:06:45 cpu time, factor 3.33)
Building Word_Lib ...
Finished Word_Lib (0:00:45 elapsed time, 0:02:23 cpu time, factor 3.11)
Building IP_Addresses ...
Finished IP_Addresses (0:02:20 elapsed time, 0:06:56 cpu time, factor 2.96)
Building Simple_Firewall ...
Finished Simple_Firewall (0:00:25 elapsed time, 0:01:15 cpu time, factor 3.03)
Building Routing ...
Finished Routing (0:00:14 elapsed time, 0:00:27 cpu time, factor 1.93)
Building Iptables_Semantics ...
Finished Iptables_Semantics (0:01:44 elapsed time, 0:06:05 cpu time, factor 3.51)
Building Iptables_Semantics_Examples ...
Finished Iptables_Semantics_Examples (0:03:34 elapsed time, 0:13:22 cpu time, factor 3.75)
Running Iptables_Semantics_Examples_Big ...
Finished Iptables_Semantics_Examples_Big (0:56:32 elapsed time, 3:33:52 cpu time, factor 3.78)
Building HOL-Library ...
Finished HOL-Library (0:02:04 elapsed time, 0:06:51 cpu time, factor 3.31)
Building Category3 ...
Finished Category3 (0:04:03 elapsed time, 0:12:07 cpu time, factor 2.99)
Building MonoidalCategory ...
Finished MonoidalCategory (0:03:33 elapsed time, 0:07:41 cpu time, factor 2.17)
Running Bicategory ...
Finished Bicategory (0:37:42 elapsed time, 1:46:45 cpu time, factor 2.83)
Running JinjaThreads ...
Finished JinjaThreads (0:39:49 elapsed time, 2:21:02 cpu time, factor 3.54)
Building ConcurrentIMP ...
Finished ConcurrentIMP (0:00:24 elapsed time, 0:00:53 cpu time, factor 2.21)
Running ConcurrentGC ...
Finished ConcurrentGC (0:13:35 elapsed time, 0:51:12 cpu time, factor 3.77)
6:45:26 elapsed time, 17:49:48 cpu time, factor 2.64
Building Pure ...
Finished Pure (0:00:14 elapsed time, 0:00:13 cpu time, factor 0.97)
Building HOL ...
Finished HOL (0:02:45 elapsed time, 0:07:22 cpu time, factor 2.67)
Building Flyspeck-Tame ...
Finished Flyspeck-Tame (0:01:02 elapsed time, 0:03:04 cpu time, factor 2.96)
Running Flyspeck-Tame-Computation ...
Finished Flyspeck-Tame-Computation (2:36:44 elapsed time, 3:56:57 cpu time, factor 1.51)
Building Word_Lib ...
Finished Word_Lib (0:00:41 elapsed time, 0:02:07 cpu time, factor 3.06)
Building IP_Addresses ...
Finished IP_Addresses (0:02:39 elapsed time, 0:06:43 cpu time, factor 2.52)
Building Simple_Firewall ...
Finished Simple_Firewall (0:00:23 elapsed time, 0:01:03 cpu time, factor 2.70)
Building Routing ...
Finished Routing (0:00:13 elapsed time, 0:00:25 cpu time, factor 1.90)
Building Iptables_Semantics ...
Finished Iptables_Semantics (0:01:39 elapsed time, 0:05:00 cpu time, factor 3.03)
Building Iptables_Semantics_Examples ...
Finished Iptables_Semantics_Examples (0:03:02 elapsed time, 0:11:21 cpu time, factor 3.73)
Running Iptables_Semantics_Examples_Big ...
Finished Iptables_Semantics_Examples_Big (1:04:55 elapsed time, 3:46:52 cpu time, factor 3.49)
Building AWN ...
Finished AWN (0:00:39 elapsed time, 0:01:44 cpu time, factor 2.67)
Running AODV ...
Finished AODV (0:58:25 elapsed time, 3:16:21 cpu time, factor 3.36)
Building HOL-Library ...
Finished HOL-Library (0:01:53 elapsed time, 0:05:52 cpu time, factor 3.10)
Building Category3 ...
Finished Category3 (0:03:34 elapsed time, 0:10:30 cpu time, factor 2.94)
Building MonoidalCategory ...
Finished MonoidalCategory (0:03:07 elapsed time, 0:06:47 cpu time, factor 2.18)
Running Bicategory ...
Finished Bicategory (0:34:21 elapsed time, 1:37:06 cpu time, factor 2.83)
Running JinjaThreads ...
Finished JinjaThreads (0:41:08 elapsed time, 2:13:40 cpu time, factor 3.25)
Building ConcurrentIMP ...
Finished ConcurrentIMP (0:00:22 elapsed time, 0:00:49 cpu time, factor 2.18)
Running ConcurrentGC ...
Finished ConcurrentGC (0:12:27 elapsed time, 0:46:32 cpu time, factor 3.74)
6:31:09 elapsed time, 16:40:37 cpu time, factor 2.56
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.