Mathlib as a PC benchmark

Stream: general

[Martin Dvořák]

I measured the time to build Mathlib as of 2025-03-28 on my two computers. Both were measured with maximum performance settings, no power saving. The results were, as I expected (or perhaps more than I expected), tremendous. You can post yours.

[Martin Dvořák]

CPU: Intel Core i5-8250U
RAM: DDR4, 16 GB, 2400 MHz
SSD: Samsung MZVLB512HBJQ-000L7

6.5 hours

[Martin Dvořák]

CPU: AMD Ryzen 9 9950X
RAM: DDR5, 32 GB, 6000 MHz
SSD: Samsung 990 PRO 1 TB

15 minutes

[Kevin Buzzard]

Can you make it clear exactly what this benchmark is? Do you also compile batteries or get cache? What exactly are you typing to do this?

[Martin Dvořák]

First I made sure that all the before-compilations things were finished by running lake build and waiting until it started crunching individual files. Then:

lake clean
lake build

Afaik it recompiled all dependencies.

[Kevin Buzzard]

So lake exe cache get (meaning that lake build is immediate) and then lake clean and lake build would also work?

[Yury G. Kudryashov]

Do we understand which parameters have the most effect on the compiler time?

[Yury G. Kudryashov]

Also, do you remember how much the faster computer cost?

[Yury G. Kudryashov]

I'm thinking about upgrading my desktop to something that can compile mathlib in less than half an hour.

[Wang Jingting]

My friends and I have also done some research on how to find a laptop better at compiling mathlib (because we're both upgrading our laptops). In general, we found that on the same laptop, it takes 4~5 times more time to compile under Windows comparing to compiling under Linux. And Ryzen 9 7940HX/7945HX outperforms intel i9-14900HX on this.

[Wang Jingting]

It is observed that in the process, the RAM it occupies is almost always less than 8~16GB (somewhere between that, but I forgot the exact number).

[Wang Jingting]

By the way, if we're hoping that mathlib will expand to 10~100 times its current size, how would we expect things to be done at that time? Are we facing the choice between downloading >= 50GB of cache and hours of compilation? (Or are we expecting that Moore's law will give us better computers?)

[Wang Jingting]

Wang Jingting said:

My friends and I have also done some research on how to find a laptop better at compiling mathlib (because we're both upgrading our laptops). In general, we found that on the same laptop, it takes 4~5 times more time to compile under Windows comparing to compiling under Linux. And Ryzen 9 7940HX/7945HX outperforms intel i9-14900HX on this.

On i9-14900HX/64GB RAM, it took about 138 minutes under Windows and about 25 minutes under Linux. On R9-7940HX/64GB RAM, it took ~2 hours under Windows and 20 minutes under Linux.

[Yury G. Kudryashov]

I guess, my Intel i5 is too old. I'll search for something newer tomorrow.

[Yury G. Kudryashov]

Wang Jingting said:

By the way, if we're hoping that mathlib will expand to 10~100 times its current size, how would we expect things to be done at that time? Are we facing the choice between downloading >= 50GB of cache and hours of compilation? (Or are we expecting that Moore's law will give us better computers?)

There are several ways we can deal with that, and they are being discussed by the maintainers. E.g.,

• integrate lake with lake exe cache (or another cache solution) so that you don't download cache for the files you don't import;
• provide "partial" oleans that lack some information not required for basic operations;
• migrate from a single repository to many (similar to what KDE libraries did during KDE3->4 migration), so that you can choose what repositories do you depend on;
• hope for more effective Lean / Lean meta code / hardware.

Note: this is not a summary of some specific discussion, but a random list of possibilities that came to my mind (though some of these options were discussed on Zulip before). And none of this is an "official" plan from the maintainers team.

[Niels Voss]

In the case that we would get partial .oleans, would that basically mean that proofs would be erased from the .olean files? Would this have the potential to break other proofs?

[Yury G. Kudryashov]

See #lean4 > Lean 4 needs to be optimised by at least 10x. Ideas? @ 💬

[Kim Morrison]

Yury G. Kudryashov said:

• integrate lake with lake exe cache (or another cache solution) so that you don't download cache for the files you don't import;

Mac Malone is working on this this quarter.

[Yury G. Kudryashov]

I guess, I included this because I saw a discussion about it somewhere on Zulip.

[Chris Birkbeck]

Wang Jingting said:

On i9-14900HX/64GB RAM, it took about 138 minutes under Windows and about 25 minutes under Linux. On R9-7940HX/64GB RAM, it took ~2 hours under Windows and 20 minutes under Linux.

I've also noticed Linux being much faster than windows to build (with the same hardware), is there a reason these such a big gap? or is it just "windows bad, linux good"?

[Sébastien Gouëzel]

On Windows, have you deativated the integrated antivirus on the directory containing mathlib? I think this makes a big difference.

[Chris Birkbeck]

I had not, let me try and see if this helps.

[Henrik Böving]

Sébastien Gouëzel said:

On Windows, have you deativated the integrated antivirus on the directory containing mathlib? I think this makes a big difference.

It definitely does, whenever we debug windows issues on our windows machines we can see large amounts of CPU percentage being wasted by anti virus software.

Chris Birkbeck said:

Wang Jingting said:

On i9-14900HX/64GB RAM, it took about 138 minutes under Windows and about 25 minutes under Linux. On R9-7940HX/64GB RAM, it took ~2 hours under Windows and 20 minutes under Linux.

I've also noticed Linux being much faster than windows to build (with the same hardware), is there a reason these such a big gap? or is it just "windows bad, linux good"?

The windows build process is tweaked compared to the Linux one for technical reasons surrounding symbol limits in shared objects and has to do inherently more work than the linux or macos one.

[Chris Birkbeck]

So I turned windows defender off but it doesn't seem hugely faster (its still running, but on Linux it would be basically done by now). One thing I notice is that even though all the cores show as if they are being used, the % utilisation stays in the 30-70% range, but on Linux once it starts building it stays at 100% until it finishes.

[Matej Penciak]

Chris Birkbeck said:

So I turned windows defender off but it doesn't seem hugely faster (its still running, but on Linux it would be basically done by now). One thing I notice is that even though all the cores show as if they are being used, the % utilisation stays in the 30-70% range, but on Linux once it starts building it stays at 100% until it finishes.

I just wanted to back up that this was also my experience trying to use Lean in Windows. Same hardware, windows defender on/off... The build process is definitely slower. I'll add that running with WSL2 inside of Windows has almost equivalent performance to a Linux dual boot.

[Yury G. Kudryashov]

If someone here understands what should I care about when choosing a desktop for Lean and can help me choose a specific desktop (I use Linux), then I'll be very grateful.

P.S.: I don't want to pay for this to avoid dealing with taxes, but I'm ready to donate $50 to a charity we'll agree on.

[Kevin Buzzard]

I just asked the analogous question about laptops recently (on mobile so can't face searching). One thing that came up was that GPUs probably aren't much help if your goal is "compile lean code fast" but they might be a lot of help if your goal is "run AIs locally to help you writing lean code". So what exactly are your goals? (Mine was the former so I didn't pay extra for GPUs)

[Ruben Van de Velde]

#general > new (mac) laptop for Lean

[Chris Birkbeck]

My understanding is that you want a CPU with lots of cores (like a Ryzen 9950X or the newer 9950x3D if money is not a factor) and maybe something 32GB of RAM? (although RAM seems less important now than it was before).

[Ruben Van de Velde]

(I have 32GB of RAM and wish I had more, though it's mostly my web browser eating it all up)

[Kevin Buzzard]

One thing I'm really loving with 48GB and two monitors is that I can have FLT and mathlib open at the same time, and eg make PRs to mathlib whilst noting what I've PRed in FLT very easily. The only time I've heard my fan come on was when I ran into the #count_heartbeats issue which I posted about in #lean4 over the weekend

[Yury G. Kudryashov]

My main issue is that I look at some configurations that differ 2x in price, and I can't see the difference. So, if someone is willing to hop on a quick call and help me order a specific desktop, I'll be very grateful.

[Chris Birkbeck]

Kevin Buzzard said:

One thing I'm really loving with 48GB and two monitors is that I can have FLT and mathlib open at the same time, and eg make PRs to mathlib whilst noting what I've PRed in FLT very easily. The only time I've heard my fan come on was when I ran into the #count_heartbeats issue which I posted about in #lean4 over the weekend

Oh interesting, but was it really the RAM stopping you from doing that before? I find that surprising, then again I know nothing really about this, just what I've overheard from others.

[Kevin Buzzard]

No idea. It's just something I wouldn't have dreamed of trying before

[Yury G. Kudryashov]

OK, a specific question. Is there something wrong with this configuration? https://www.dell.com/en-us/shop/desktop-computers/dell-tower-plus-desktop/spd/dell-ebt2250-desktop/useebt2250ucto08?view=configurations&configurationid=39f771ba-3fab-4eba-ac9b-dc7b3665a2bf#features_section
I don't plan to run AI inference on this computer.

[Sebastian Ullrich]

The only thing that is a bit weird to me is that they don't give the model names of the memory and SSD. If you had the names, searching for any quick reviews on them would not be a bad idea.

[Martin Dvořák]

Martin Dvořák said:

CPU: Intel Core i5-8250U
RAM: DDR4, 16 GB, 2400 MHz
SSD: Samsung MZVLB512HBJQ-000L7

6.5 hours

This PC has Windows. I didn't know it made a difference.

[Martin Dvořák]

Martin Dvořák said:

CPU: AMD Ryzen 9 9950X
RAM: DDR5, 32 GB, 6000 MHz
SSD: Samsung 990 PRO 1 TB

15 minutes

This PC has Linux.

[Sébastien Gouëzel]

I'd take the 1TB SSD just to be on the safe side.

[张守信(Shouxin Zhang)]

It looks like—putting Mac devices aside—the remaining contenders for mobile-laptop CPUs are the R9-9955HX, R9-9955HX 3D, U9-275HX, and U9-285HX. Do we have any measurements (on Windows 11 or Linux) for how long these CPUs take to compile Mathlib4, along with some hands-on impressions of everyday single-file work—e.g., running simp, inferInstance, rw?, apply, and similar tactics?

I’ll probably end up buying Lenovo’s R9000P with the R9-9955HX. Still, Intel’s U9 line looks very tempting thanks to its strong single-core performance (would that make working on a single file faster?). With my limited budget, choosing the right laptop for Lean 4 is giving me a real headache.

Are there any powerful online servers we could use instead? I don’t know much about server-grade CPUs, but in my mind their performance should far exceed that of a personal laptop. Is that just wishful thinking?

[Michael Rothgang]

Re: server performance vs. local computers
When working on mathlib, you can use a similar phenomenon by using mathlib's cache. If you push your current branch of mathlib, CI servers try to build it. After the build has completed, you can download the olean files (for every file which built successfully). Thus, when I modify a lower-level file A in mathlib and want to see what effect it had on a "higher-level" file B (which depends on A, but through many other dependencies), a useful strategy can be (1) edit file A and push changes, (2) wait a bit, (3) download the cache for file (B). That way, I only have to build A and B on my computer.

[Michael Rothgang]

At the moment, this cache is specific to mathlib --- but my understanding is that the Lean FRO is working on extending this to other projects. (I'm not sure who'd run the servers for that --- if it's "bring your own, but we support it" or some general service provided to e.g. any project on reservoir.)

[Frederick Pu]

I'm currently on an amd ryzen 7 and 16 GB of ram.

[Frederick Pu]

more cores will help with building with lake but I think lean server on any single file will only run on one core. So you'll want more threads per core for fast real time type checking

[Henrik Böving]

In file parallelism is becoming a thing in the very recent Lean development work so even individual files should assumed to be multi core.

[Frederick Pu]

but isn't lean itself a single process program. Meaning that any lean process can only do multithreading not core level parrallelism?

[Alex Meiburg]

Your wording makes me think you might be a bit confused? Number of cores you can use == number of threads. So "multithreading" and "multi-core" are the same thing. Being a single process is irrelevant: lots of massively parallel programs are only a single process.

(There is some subtlety about logical vs physical core, hyperthreading, inter-core memory contention... but this is the main idea.)

[Henrik Böving]

Frederick Pu said:

but isn't lean itself a single process program. Meaning that any lean process can only do multithreading not core level parrallelism?

Quick Operating Systems crash course: A process is a thing in the OS world that has its own virtual address space (i.e. the memory it addresses is separated from the memory that other processes can address) and resources (open files, network connections etc.). A single process can have multiple threads associated with it that all share these resources but can be scheduled concurrently and in particular also in parallel if you have a multi core machine. So no, being a single process does not at all prevent you from doing something multicore and in fact most multicore applications out there are single process multiple thread ones.