Felipe Escallón (Sep 30 2025 at 15:25): Felipe Escallón (Sep 30 2025 at 15:25):I am looking into buying a Macbook which I would use for Isabelle temporarily. I was considering buying the M4 Macbook Air with 24 GB of RAM, but the Pro with the same chip and 16 GB costs around the same. I am worried that the thermal throttling will affect the performance of the Air too much, but I don't know if the Pro has too little RAM. Which one would be best?
Jonathan Julian Huerta y Munive (Oct 01 2025 at 11:52):The Isabelle website guidelines (hardware requirements) lists the main factors to consider: number of cores and memory. Personally, I observed that I want a higher number of cores to process a large stack of theories quickly. But for several consecutives calls to sledgehammer, my computer's memory becomes the bottleneck. Based on this, it depends on whether you are going to deal with a large library or you are going to work in automation.
Brody Little (Oct 02 2025 at 22:19):I’m not an expert on Isabelle by any means, nor have I worked on a larger project, but memory usage was routinely the bottleneck for my M1 Air with 16GB when sledgehammering away.
Mathias Fleury (Oct 03 2025 at 06:48):Even if Apple is better at memory usage than Windows, 16GB is the minimum recommended for laptops since at least 2015.I would nowadays say that 16GB is not enough for "professional" usage (back in 2015, IDE were not just chrome rebranded…)
Felipe Escallón (Oct 03 2025 at 07:36):Since getting 24GB seems to be worth it, my only concern would be cooling. I was able to briefly test successive sledgehammer calls on a 13” Air with 16GB, and it did get hot but not enough to throttle as far as I could tell. Could that be an issue when working for several hours at a time?
Mathias Fleury (Oct 03 2025 at 07:47):Let's see if a MBA user comes by and answers. Otherwise, ask on the mailing list
Mathias Fleury (Oct 03 2025 at 07:48):although it probably depends how often you are really calling sledgehammer.
Felipe Escallón (Oct 03 2025 at 07:59):I would say I use it frequently. I work on formalizations in projects like my bachelor’s thesis (I don’t know if that counts as a large project, but it’s the largest one I will work on in the near future)
Last updated: Oct 08 2025 at 20:22 UTC