Minimum computer strength

Stream: general

[Huỳnh Trần Khanh]

What is the minimum computer strength needed to use Lean and Mathlib? I've been using https://live.lean-lang.org because every time I try to run Lean on my laptop it freezes.

[Jeremy Tan]

I use a Lenovo ThinkPad Gen 2 (E14) and it works perfectly fine with Lean/mathlib

[Yury G. Kudryashov]

Lenovo ThinkPad X1 Nano Gen1 is slow but I wrote a lot of Mathlib code on it.

[Jz Pan]

A laptop bought at 2017 running Win10 with quad-code i5 2.5GHz CPU and 8GB RAM suffices, although importing whole mathlib will take 2 minutes.

[Kevin Buzzard]

8GB RAM is the bare minimum nowadays, you'd be better off with 16, and even then I've seen Lean take down my 16G laptop when I have docs open (which are also a real memory hog I think?) which is one reason I'm upgrading my laptop so I can get more RAM. But I'm a heavy user and am compiling my own projects a lot.

[Michael Rothgang]

If you're on linux, "Lean takes down my laptop" can be fixed at the lake level: by default, uses all your cores to build things - this can freeze your computer at seemingly random times if lake decides to do something with your VS Code which is open in the background. You can tell lake to be more nimble, though.

[Michael Rothgang]

(Perhaps this should be changed in lake... that's a topic for a different thread.)

[Sebastian Ullrich]

@Michael Rothgang Could you please open such a topic? I would of course be very interested in hearing more about that issue, i.e. hardware, htop screenshot, ideally a samply profile... If you do mean a freeze over multiple seconds, that almost certainly is thrashing of memory. Which limiting the number of concurrent build processes does indirectly help with.

[Sebastian Ullrich]

(also the solution is in no way limited to Linux)

[Michael Rothgang]

@Sebastian Ullrich Sure, I'll try to open such a topic soon. Just to clarify

• htop is the same/very close to my (Debian) Linux's "system tray", right?
• if I need to wait for "my computer freezes in the background", I might take a while to encounter this. But I can try to trigger this via "open lots of files".

[Sebastian Ullrich]

I don't know your system tray

[Yury G. Kudryashov]

https://htop.dev/ should be available in debian.