Computer for Lean

Stream: general

[Yury G. Kudryashov]

I'm going to buy a new desktop computer because my current laptop needs 2.5h to compile Mathlib and my very old desktop is even slower. I have a problem: I know ~nothing about hardware. What numbers should I look at? Do you have specific recommendations?
P.S.: I would prefer to continue using Linux as an OS.

[Frederick Pu]

Yury G. Kudryashov said:

I'm going to buy a new desktop computer because my current laptop needs 2.5h to compile Mathlib and my very old desktop is even slower. I have a problem: I know ~nothing about hardware. What numbers should I look at? Do you have specific recommendations?
P.S.: I would prefer to continue using Linux as an OS.

Ram is probably the most important thing since most of type checking involves caching a bunch of trees. But I'm not an expert

[Yury G. Kudryashov]

Both laptop and desktop have 16G RAM but laptop is 2x faster in building Mathlib.

[Yury G. Kudryashov]

My laptop has 2x more cores but each core is 2.5x slower (in GHz)

[Mario Carneiro]

more cores and more RAM are the main numbers of interest (well, cores * clock speed but clock speed has been mostly stable for the past many years)

[Yury G. Kudryashov]

Where do I see "clock speed"?

[Kyle Miller]

I'd say for RAM, 16 GB minimum, but it's great having 32 GB so you can have multiple mathlibs and other projects open at once for experimentation. (64 GB is very nice to have)

For CPU, get as many cores as you can afford, since this has the largest impact on mathlib compilation time as it's mostly parallelizable. I'm not sure how much GHz matters, since probably a lot of Lean compilation of memory-bound, but it doesn't hurt having more GHz if you can.

For a hard drive, I think they're pretty much standard now, but a solid state drive I think has lower latency. I don't know much about this measurement.

[Mario Carneiro]

clock speed is the thing next to "GHz"

[Kyle Miller]

(More RAM also means more mathlib can be in cache rather than just on the hard drive.)

[Mario Carneiro]

hard disk volume is of course also important for your 17 chunky mathlib-based projects and the 30 chunky versions of lean they somehow manage to depend on

[Yury G. Kudryashov]

I have 8x"11th Gen Intel(R) Core(TM) i7-1160G7 @ 1.20GHz" on my laptop, 4x"Intel(R) Core(TM) i5-3570 CPU @ 3.40 GHz" on my desktop. Desktop is 2x slower than laptop in building Mathlib.

[Yury G. Kudryashov]

Mario Carneiro said:

hard disk volume is of course also important for your 17 chunky mathlib-based projects and the 30 chunky versions of lean they somehow manage to depend on

I mostly work on branches of Mathlib (but this may change in a month).

[Mario Carneiro]

well, I'm saying that you should watch the size of the .elan and .cache/mathlib directories

[Mario Carneiro]

as well as myproj/.lake but this is bounded by the number of projects you have that depend on mathlib so if you only work on mathlib that doesn't grow without bound like the other two

[Dan Velleman]

Mario, can you say more about how to manage the .elan and .cache/mathlib directories? I know I can use elan toolchain uninstall to get rid of toolchains I'm not using anymore. My cache/mathlib directory has a long list of .ltar files, using 1.28 GB on my disk. Do I need all that stuff? Can I delete any of it, and if so how should I do it?

[Ruben Van de Velde]

Don't delete the cache files at the moment, since we're having trouble with the server they come from

[Yury G. Kudryashov]

Once we have our cache back (not yet!), you can delete ~/.cache/mathlib and lake exe cache update will re-download whatever it needs.

[Yury G. Kudryashov]

See also https://github.com/JLimperg/elan-cleanup

[Kevin Buzzard]

These directories are just full of versions of lean and mathlib which you happened to use on your computer at least once. You can periodically delete them and lake will just continue to download the leans and mathlibs which you use in future

[Antoine Chambert-Loir]

Together, my .elan and .cache/mathlib directories take up 18GB and 22GB…
How can I know which stuff isn't of any use anymore?

[Yury G. Kudryashov]

For ~/.elan, I use elan-cleanup from time to time (after updating itself to use the same toolchain as mathlib does)

[Yury G. Kudryashov]

For ~/.cache/mathlib, normally you can delete all files and let lake exe cache get download whatever is needed. However, right now the cache doesn't work, so I would not clear that folder before the cache is up again.