Katherine Kosaian (Aug 10 2024 at 13:48): Katherine Kosaian (Aug 10 2024 at 13:48):I am looking to purchase a new computer and want to ensure that I will be able to smoothly run Isabelle/HOL and achieve good performance (working with Isabelle on my current laptop, a 2019 Macbook Pro with 8 GB RAM has caused me some frustration over the years).
Generally, I like Macs, and so I am wondering: Is Isabelle stable with the new M3 chips? Does anyone have experience (positive or negative) with using Isabelle on a new Mac?
Also, are there any specs that I should pay special attention to (memory/RAM/etc)?
Jan van Brügge (Aug 10 2024 at 22:16):I can't say anything about M3, but I would not go for less than 32GB of RAM. Isabelle can really eat a lot of memory
Wenda Li (Aug 12 2024 at 09:11):I am happily running Isabelle on my M1 Macboo Pro with 32Gb RAM. To me, the more RAM the better -- I would even trade some CPU cores for RAM when needed.
Fabian Huch (Aug 12 2024 at 09:24):From what I hear Isabelle works very well with the M3 chips -- but I would go for 32GB. @Kevin Kappelmann @Lukas Stevens
Jan van Brügge (Aug 12 2024 at 10:18):The fact that Apple still sells Laptops with 8GB non-upgradable RAM is honestly baffling. I guess they want people to buy a new one soon
Craig Alan Feinstein (Aug 13 2024 at 00:41):Here is a simple question - suppose I have two 2x2 matrices, one with rows (1 2) (3 4) and the other with rows (1 3) (2 4) (which happens to be the transpose of the first). How do I efficiently prove in Isabelle that the product is (5 11) (11 25)?
Wenda Li (Aug 13 2024 at 02:43):Craig Alan Feinstein said:
Here is a simple question - suppose I have two 2x2 matrices, one with rows (1 2) (3 4) and the other with rows (1 3) (2 4) (which happens to be the transpose of the first). How do I efficiently prove in Isabelle that the product is (5 11) (11 25)?
@Craig Alan Feinstein wrong thread? :-)
Craig Alan Feinstein (Aug 13 2024 at 02:48):@wendali yes I’m sorry it should be in the matrix multiplication thread.
Katherine Kosaian (Aug 13 2024 at 18:09):Thank you all for the recommendations!! I will try to prioritize RAM.
Jonathan Julian Huerta y Munive (Aug 14 2024 at 10:09):@Katherine Kosaian and cores. From the Isabelle website:
Asta Halkjær From (Aug 14 2024 at 10:49):It doesn't speak to interactive use, but for "how long does it take to build HOL-Analysis", it seems extra cores and RAM have diminishing returns. https://arxiv.org/abs/2209.13894
Last updated: Dec 21 2024 at 12:33 UTC