Laptops suitable for Lean

Stream: general

[傅辰佶]

Any recommendations for laptops that are suitable for lean? Say, is MacBook Air (8-core, 8GB shared memory, 256GB storage) good enough?

[Patrick Massot]

This is not enough RAM for a nice use.

[傅辰佶]

How about 16GB?

[Timo Carlin-Burns]

I think processor performance makes a difference too. It's pretty painful for me to use Lean on my laptop from 2017 with an Intel 7200U 3.1Ghz CPU.

[Richard Copley]

(If I understand correctly, the shared memory in a Mac is fast VRAM which is available to the GPU but can also be used by the CPU. It is in addition to ordinary DRAM.)

[Matthew Ballard]

I used a M1 MacBook air with those specs and the memory was limiting. But the processor was more than enough

[傅辰佶]

You mean 16GB memory is not enough?

[Julian Berman]

I use a MacBook Air absolute base model (8GB) and honestly find it pretty fine. But maybe the secret is "don't try anything more powerful". Especially if you use GitPod though you can do all your Lean development SSHed / on the web too.

[傅辰佶]

I see. Sounds good!

[Kevin Buzzard]

I use a Linux laptop with 16G ram and it works fine for lean, it's about three years old

[Michael Stoll]

Mine is a bit older, but similar (CPU is "Intel(R) Core(TM) i7-8565U CPU @ 1.80GHz"), and does quite well. (I'll be getting a new one soon, though.)

[Shreyas Srinivas]

Apart from what everyone else said, do get a laptop with a lot of storage, especially if it is a Mac, since they don't seem to allow expanding the storage. Lean quickly fills up your storage if you work on many based mathlib projects (and the tooling currently works most smoothly for mathlib dependent projects and mathlib).

[Eric Rodriguez]

that can be dealt with mostly with cache+toolchain pruning

[Kim Morrison]

Echoing @Julian Berman, I do a lot of my work on a quite ancient Mac laptop, but via ssh remote session to a beefy desktop machine. Except for an annoying delay with VSCode reconnecting the session after the laptop sleeps, I find this a completely fine experience.

[Rebecca Bellovin]

For some reason, I've had much worse experiences trying to run VSCode on Dell XPSes than on Lenovo Thinkpads (both with 16G memory, running Ubuntu); adding another 16G of swap to the XPSes helped a lot

[Jon Eugster]

Eric Rodriguez said:

that can be dealt with mostly with cache+toolchain pruning

While that's true to some extend, just the amount of mathlib copies living in various .lake/packages folder can sum up quite a bit... Currently that's 4GB per project depending on mathlib.

For the NNG I had an approach of automatically pruning some unused mathlib .olean files in CI after building, which gets that down to 2GB, but it still adds up on the server.

[Antoine Chambert-Loir]

I need to have my office buy me a new laptop. I had a 2015 MacBook Pro. The new one could be a recent model with M2 chip and 16GB of “combined memory“. (This is already expensive enough.) Would that be reasonable for a comfortable use of Lean?

[Antoine Chambert-Loir]

https://www.apple.com/shop/buy-mac/macbook-pro/14-inch-space-gray-apple-m3-chip-with-8-core-cpu-and-10-core-gpu-8gb-memory-1tb

[Kim Morrison]

I think so. Lean is not such a memory hog as it used to be, and I think many people find 16gb is fine. The M2 likes Lean. :-)

[Oliver Nash]

IMHO money spent on RAM is never wasted and is the single best way to extend the useful lifetime of a computer, especially for devices (like MacBooks) which cannot have more memory added later.

[Shreyas Srinivas]

I would recommend going for 32 GB if you plan to keep this machine for a while.

[Kevin Buzzard]

I sometimes run out of memory (i.e. swapping gets serious) on a 16GB machine during a "normal working session" (I have a browser open with many tabs, Discord and Zulip and Teams and Slack open, a zoom call open and I'm editing mathlib). I never have such problems with my 32GB machine.