Recommend me a PC under 2000 €

Stream: general

[Martin Dvořák]

I would like to get a PC for Lean 4, to be as fast as possible.
The budget is 2000 € (i.e., approximately 2000 $).
I expect it to be a "tower" PC.
Any recommendations?

[Christian K]

I think that you can go all out on a CPU with a 2000€ budget. The flagship AMD CPU is the ryzen 9950X (with a massive 32 threads!), it costs about 650€ - 700€. I think it even has built-in graphics, so you wouldn't even need an external GPU. The best (consumer) intel CPU is in a similar price and performance range (I don't know which one would be better for lean).

[Martin Dvořák]

Yeah, AMD 9950X3D is on my radar.

[Ruben Van de Velde]

And probably throw as much as you can at RAM

[Martin Dvořák]

I guess I won't need more than 32 GM RAM, so should I aim for 32 GB but as fast RAM as possible?

[Christian K]

You could also take a look at the AMD Threadripper CPUs, although I think at some point, single core performance is more important for lean than just adding more cores

[Christian K]

Martin Dvořák said:

I guess I won't need more than 32 GM RAM, so should I aim for 32 GB but as fast RAM as possible?

This makes sense, I think using two 16 GB sticks is a bit faster than one 32 GB

[Ruben Van de Velde]

I don't know anything about speed differences for RAM, but 32G of RAM sounds like a good plan

[Martin Dvořák]

Yeah, gone are the days when 640 kB was enough for everybody.

[Nick Ward]

Is there a general consensus on what makes a good machine if your goal is "compile mathlib as fast and painlessly as possible"? I would assume it's just a big SSD and as much RAM as you can buy.

[Eric Taucher]

Can anyone comment if Lean 4 is typically bound to a single processor core/thread/etc? I know that with Prolog unless I specifically write the code for multiple threads one core is carrying all the load and the others are practically idle working on non-Prolog tasks.

If Lean 4 uses just one core then I would look for a CPU that has at least a few cores that can run extremely fast for a long time and not idle down for heat.

[Eric Taucher]

Also consider the configuration. With Windows many of my tasks are often causing the antivirus checker to kick in which then slows things down. I don't know which OS you plan to pick but do keep that in mind.

[Edward van de Meent]

i suspect it is using multiple threads... for me, a common message when building is building Mathlib.Foo.Bar (+ 11 more)

[Christian K]

Yes, I think for mathlib, more threads are generally better, but when working in a single file in vscode, lean probably uses only one thread.

[Edward van de Meent]

or thereabouts. So either lake is lying, or building is done multithreaded

[Christian K]

But when you build your own projects (according to my experience), the amount of threads that can be used depends on how flat the import structure is.

[Eric Taucher]

As for memory I would even suggest going to 64GB, I can't count how many times I think I buy enough then a few years latter it is never enough. I currently have 16 GB on my machine and regret not going for 32GB.

[Ruben Van de Velde]

lake certainly builds files in parallel, and I believe there's been work recently to do concurrent work within one file as well

[Eric Taucher]

If you are getting a tower and don't have an Uninterruptible Power Supply UPS, then consider tossing that into the budget.

Obviously laptops use the battery for that purpose but I remember the days before laptops and power going out. :frown:

[Kim Morrison]

Single file parallelism will improve significantly over the next few months. Certainly for building Mathlib, many cores is great. Downstream projects tend to have more linear import structures, so currently there's less parallelism available, but improving.

[Martin Dvořák]

Eric Taucher said:

As for memory I would even suggest going to 64GB, I can't count how many times I think I buy enough then a few years latter it is never enough. I currently have 16 GB on my machine and regret not going for 32GB.

Thanks for the tip! I nevertheless feel like 32 GB is almost too much. Can you give me one scenario where more than 32 GB would be useful?

[Arthur Paulino]

Memory is cheap. You can extend later

[Arthur Paulino]

Also, memory gets cheaper with time. There's a chance it will be even cheaper when you want/need to extend it

So I would say get your 32GBs of RAM, then spend more on CPU. And the rest on peripherals for ergonomics, like a good monitor, a good keyboard and even a proper chair (gaming chairs are terrible in my experience). Though chairs are obnoxiously expensive assets... you might want to leave that for the next budget

[Christian Merten]

Martin Dvořák said:

Eric Taucher said:

As for memory I would even suggest going to 64GB, I can't count how many times I think I buy enough then a few years latter it is never enough. I currently have 16 GB on my machine and regret not going for 32GB.

Thanks for the tip! I nevertheless feel like 32 GB is almost too much. Can you give me one scenario where more than 32 GB would be useful?

I have 32 GB and I regularly whish I had more, Firefox consumes a lot of memory, it can easily reach 10-15 GB. If you add one or two lean processes to that, you reach the limit quite fast.

[Martin Dvořák]

Does the speed of my SSD play an important role for Lean?

[Eric Taucher]

Martin Dvořák said:

Thanks for the tip! I nevertheless feel like 32 GB is almost too much. Can you give me one scenario where more than 32 GB would be useful?

On Windows to run a Linux OS typically Windows Subsystem for Linux (WSL) is used and that allocates a block of memory, e.g. 8GB, so if you want to run two or more such Linux instance on the same PC then more memory is better. While I have started Linux on WSL with 8GB, 16GB is nicer. So if you get 32GB and then start a Linux on WSL allocating 16GB to that instance, the WIndows OS is now limited to 16GB.

Since you plan to get a tower, if you do get 32GB check to make sure that at least 2 memory slots are left empty to allow you to upgrade latter.

[Marc Huisinga]

Kim Morrison said:

Single file parallelism will improve significantly over the next few months. Certainly for building Mathlib, many cores is great. Downstream projects tend to have more linear import structures, so currently there's less parallelism available, but improving.

It's also worth adding that parallelism already plays a significant role when using Lean interactively.

• Task cancellation is (necessarily) cooperative in Lean. So when you add a character to a document, whatever long-running tactic is currently running must periodically check that it should stop. This isn't always guaranteed for every tactic that people write, so we can't immediately terminate the previous elaboration run immediately. Instead of waiting for the previous elaboration run to complete, which would significantly increase the latency in the language server, we immediately launch another elaboration run in parallel.
• There is a separate process for every single file that is open, so interaction with multiple files at once is parallel.
• When the language server calls Lake to build the dependencies of a file, Lake is also run in a separate process.
• Language server requests are processed in parallel, e.g. semantic highlighting, auto-completion, etc.
• Several of the language server I/O operations are run in parallel.
• When launching the language server, the .ilean files are loaded in parallel so that it doesn't block the rest of the language server from functioning.

[Eric Taucher]

Martin Dvořák said:

Does the speed of my SSD play an important role for Lean?

For me personally having used spinning disk hard drives for decades, an SSD is so much faster that the differences in speed between one SSD and another is not something I focus on since SSD became the norm.

I don't know how much faster a RAM drive would be over an SSD, but it is something to consider if you have the memory to spare.

[Kevin Buzzard]

Martin Dvořák said:

Eric Taucher said:

As for memory I would even suggest going to 64GB, I can't count how many times I think I buy enough then a few years latter it is never enough. I currently have 16 GB on my machine and regret not going for 32GB.

Thanks for the tip! I nevertheless feel like 32 GB is almost too much. Can you give me one scenario where more than 32 GB would be useful?

In 2020 4 gig was hopeless but 8 gigs was OK for running Lean. Today 8 gigs is pretty bad, 16 gigs is usually fine but Lean still occasionally takes my laptop down if I start messing with stuff at the beginnings of mathlib or if I'm live streaming and hacking. 32 gigs is always fine. But in 5 years' time 16 gigs will probably be a disaster, and maybe even 32 gigs might not always be fine. Are you planning on throwing the machine away in 2 years or do you want it to be a bit more future-proof? It's not just about what works today.

[Arthur Paulino]

You don't necessarily need to throw your machine away if you need more RAM
https://www.ecosia.org/search?method=index&q=buy+ram

[Edward van de Meent]

i hear you can download that nowadays? :upside_down:

[Matej Penciak]

One comment about the "Buy 32 now, extend to 64 later" strategy: If you choose to go with the 9950x (or its predecessor the 7950x), then it's documented that they don't behave great with 4 sticks of RAM (on the connectivity part of: https://www.amd.com/en/products/processors/desktops/ryzen/9000-series/amd-ryzen-9-9950x.html, or any number of forum threads if you google 9950x memory controllers).

I'm not sure about the tradeoff of memory size and memory speed for Lean compilation, but 2x32gb is roughly the same price as 4x16gb, more stable, and faster so I'd say there's no reason not to do it.

[Eric Taucher]

Matej Penciak said:

then it's documented that they don't behave great with 4 sticks of RAM

Thanks. Will be keeping that in mind for my next computer.

Found this video by Gamers Nexus from 4 years ago. So yes, a point to pay attention to and so forget what I noted about keeping 2 slots open. New advise, do the research from scratch about the memory options as what use to be a constant is not. Learned something new today.

[Daniel Weber]

Kevin Buzzard said:

In 2020 4 gig was hopeless but 8 gigs was OK for running Lean. Today 8 gigs is pretty bad, 16 gigs is usually fine but Lean still occasionally takes my laptop down if I start messing with stuff at the beginnings of mathlib or if I'm live streaming and hacking. 32 gigs is always fine. But in 5 years' time 16 gigs will probably be a disaster, and maybe even 32 gigs might not always be fine. Are you planning on throwing the machine away in 2 years or do you want it to be a bit more future-proof? It's not just about what works today.

I'd argue that we should strongly endeavor for this to not be the case—why are you expecting this? Is it merely from Mathlib growing?

[Kevin Buzzard]

Because I remember when my computer had 12k of memory in total and no disc, and this was fine? (edit for @Eric Taucher : it was an Acorn Atom)

[Chris Wong]

The other monorepo (Google's) gave up on local builds a long time ago, and hosts everything on the cloud instead. Perhaps Gitpod is the future :thinking:

[Yaël Dillies]

Gitpod is dead in two months :sad: (or rather we won't be able to use it anymore)

[Eric Taucher]

Kevin Buzzard said:

12k of memory

I can't figure out which computer commonly had 12K. I was thinking maybe an Altair 8080 but that came with 256 bytes of RAM. Or perhaps a computer job run on an IBM mainframe in the late 70's with JCL, but even those used about 32K.

[Vlad Tsyrklevich]

Chris Wong said:

The other monorepo (Google's) gave up on local builds a long time ago, and hosts everything on the cloud instead. Perhaps Gitpod is the future :thinking:

'everything hosted in the cloud' is not really how it works. You essentially have a cached NFS-like mounted directory for google3, so it's just a local directory like any other and building/testing locally works just like normal. Of course, you wouldn't want to needlessly build the entire repo, just what you're working on.

Also, there are many monorepo projects. For example, LLVM is open source, much larger than mathlib, and works just fine as a monorepo.

[Ruben Van de Velde]

Once mathlib gets to the size of all of google's code, we can reconsider :)

[Patrick Stevens]

Arthur Paulino said:

And the rest on peripherals for ergonomics, like a good monitor, a good keyboard and even a proper chair (gaming chairs are terrible in my experience). Though chairs are obnoxiously expensive assets... you might want to leave that for the next budget

New chairs are extremely expensive, but second-hand chairs are merely expensive; in London you can get an Aeron for a few hundred GBP on eBay or whatever.

[Eric Taucher]

Eric Taucher said:

I don't know how much faster a RAM drive would be over an SSD, but it is something to consider if you have the memory to spare.

Just learned of Ramfs, OS specific alternative, but would not be surprised if the idea was reimplemented on other OSes.

Ramfs is a very simple FileSystem that exports Linux's disk caching mechanisms (the page cache and dentry cache) as a dynamically resizable ram-based filesystem.

Discovered while reading

Cutting Down Rust Compile Times From 30 to 2 Minutes With One Thousand Crates

[Eric Wieser]

Ruben Van de Velde said:

Once mathlib gets to the size of all of google's code, we can reconsider :)

This is a poor threshold, since thanks to alphaproof Google's monorepo includes mathlib!