Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] running Isabelle on a Mac


view this post on Zulip Email Gateway (Aug 22 2022 at 20:01):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’m looking for advice regarding a suitable model of Apple Mac for running Isabelle.

I’ve got a 2013 Mac Pro, and its processor is a 3.5 GHz 6-Core Intel Xeon E5. Recent benchmarks suggest that the recently updated 27 inch iMac delivers much better performance. But I’ve been advised that Xeon chips are particularly good for multithreaded tasks, compared with the i9 chips used in the iMac. Does anybody have any experience of the latter?

http://browser.geekbench.com/mac-benchmarks

Larry Paulson

view this post on Zulip Email Gateway (Aug 22 2022 at 20:01):

From: Tobias Nipkow <nipkow@in.tum.de>
I would definitely advise against my less than a year old MacBook Pro where the
Core i9 overheated and it was slower than my previous MacBook Pro. See the
thread on this list last year. Even when the i9 did not overheat I was
underwhelmed by the performance increase for Isabelle.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 20:02):

From: Makarius <makarius@sketis.net>
My high-end machines are usually on Linux, but I routinely keep an eye
on Apple hardware because that is an officially supported Isabelle platform.

Some month ago, I went to one of these globally standardized Apple
stores to play with the new iMac Pro (Intel Xeon) (see also
https://www.apple.com/imac-pro). I did this in the presence of an Apple
guy beside me, who was was quite impressed by the amount of cores that
were used by our fine application (just Isabelle HOL + HOL-Analysis, no
tests of AFP). Overall performance looked pretty good in this test
drive, but I don't have concrete numbers.

Technical side-remark: Apple presumably has a standardized setup of test
machines. You can do whatever you want as long as the OS configuration
lets you so. The staff can reset it later to return to a clean state, so
they are normally not worried about arbitrary testing by customers.

One thing you cannot do in the test configuration is to download an .app
bundle and run that as an application. But of course, you could just
open a Terminal window an run Isabelle2019.app/Isabelle/bin/isabelle on
the command-line (unless Apple has nailed down the OS even further in
the meantime).

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 20:02):

From: Lawrence Paulson <lp15@cam.ac.uk>
Many thanks to all for your comments!

The key phrase seems to be “thermal throttling” and one sees online various references to it:

https://www.youtube.com/watch?v=BXIaSXU99-k
https://www.cultofmac.com/564741/macbook-pro-thermal-throttling-consumer-reports/

Larry


Last updated: Nov 21 2024 at 12:39 UTC