Email Gateway (Mar 24 2022 at 10:15): Email Gateway (Mar 24 2022 at 10:15):From: Lawrence Paulson <lp15@cam.ac.uk>
Lots of us are Mac users and will be wondering whether the latest products (notably the Mac Studio) are worth it. Poly/ML now has native Apple support, but hard benchmarks would be best, compared against the latest Intel offerings.
The other big M1 win is battery life, only relevant to laptops.
Larry
Email Gateway (Mar 24 2022 at 10:33):From: Fabian Huch <huch@in.tum.de>
We do have hard benchmark results [1].
The M1 Pro/M1 Max (which are the same CPU-wise) are a lot faster than
older Intel generations, and are the best option on laptops (even if you
extrapolate for the fastest Intel/AMD laptop CPUs), but can not compete
against the 12th gen Intel cores on desktop: M1 Pro with native arm
backend takes 2:17, i7-12700K only 1:47.
Intels i9-12900KS should be the fastest desktop CPU currently available.
The M1 Ultra is just two M1 Max glued together, and Isabelle won't
profit at all from the additional cores (at least for single sessions
which perform typical symbolic operations like HOL-Analysis).
Fabian
[1]:
https://docs.google.com/spreadsheets/d/12GhEwSNSopowDBq5gSem3u39fliiIcoTIZHMnX4RE3A
Email Gateway (Mar 24 2022 at 18:54):From: Makarius <makarius@sketis.net>
Note that any changes of underlying libraries requires to rebuild other
sessions: multiple independent CPUs can help here a lot, but just 2 CPUs with
8 cores each is not so much. Better are 20 CPUs with 8 cores each, or maybe a
larger cluster.
This important model of Isabelle development with profound changes at the
bottom (e.g. Pure, HOL, HOL-Analysis) has seen some decline in recent years.
As a consequence, the ambitions for proper reforms have been diminished.
My current plan is to revive it with the help of distributed parallel builds,
instead of doing it on a single hot (and expensive) machine.
The classic target is < 10min for all sessions of the Isabelle distribution,
and < 45min for all of AFP (excluding only "very_slow").
Makarius
Email Gateway (Mar 24 2022 at 18:57):From: Makarius <makarius@sketis.net>
Mac Studio looks like an expensive version of the Mac Mini M1, or a cheap
version of Mac Pro.
Not bad as a very fancy desktop machine, but quite some money spent for parts
that have no meaning to Isabelle: GPUs and Neural Engine.
The 1-CPU version with 64GB RAM + 1 TB SSD costs 2900,- EUR.
The 2-CPU version with 128GB RAM + 1 TB SSD costs 5500,- EUR.
Makarius
Last updated: Jul 15 2022 at 23:21 UTC