Turns Out the MacBook Pro is the Best Laptop for Lean4

Stream: general

[张守信(Shouxin Zhang)]

I recently got a new Mechrevo Kylin 16 Ultra, a laptop from a Chinese manufacturer, configured with 64GB of RAM, a 2TB SSD, an R9 9955HX3D CPU, and a 5090 GPU.

I spent some time setting up the Windows Subsystem for Linux (WSL) with Ubuntu and then installed the WSL extension in VSCode. This was to ensure the CPU performance wouldn't be significantly impacted by the Windows OS, allowing for a fair comparison against the M4 Pro chip in my macOS system under a Linux environment.

Unfortunately, when I created a test.lean file and added the line import Mathlib, the time it took for the tactic state to load was about double that of my M4 Pro. To be fair, both laptops were running on battery. (An unplugged M4 Pro should probably be compared to a desktop-class 9950X3D when it's plugged in.)

Furthermore, since my new Windows laptop is a gaming notebook, its battery life is far worse than my MacBook Pro's. The Mac can easily last me a full day of normal use—I'd say at least 7 hours without issue. This one only gets about 3 hours.

From every angle, I believe the MacBook is the golden tool for working with Lean. The reasons are stated above. (But is there really a Windows laptop with better performance than a Mac? I watched a review video on gaming laptop CPUs, and the 9955HX3D is currently the top non-Apple chip. Yet, it seems when it comes to single-core performance, the Mac is still far ahead.)

[Joscha Mennicken]

Doesn't WSL 2 run in some sort of VM? I'd expect that to add some CPU performance overhead, but to have better FS performance than on plain Windows. But I've never used it myself.

[Max Nowak 🐉]

It is possible to set up Lean to run on windows without WSL. I wonder what performance you'll get then.

[Jz Pan]

Max Nowak 🐉 said:

It is possible to set up Lean to run on windows without WSL. I wonder what performance you'll get then.

It will be worse.

[Wang Jingting]

Have you tried dual booting a Linux system instead of using WSL? I'm also curious about the difference between these choices.

[张守信(Shouxin Zhang)]

Wang Jingting said:

Have you tried dual booting a Linux system instead of using WSL? I'm also curious about the difference between these choices.

I'll try to make the comparison after my functional analysis exam on June 17th. (To be honest, as a newbie, I think installing a dual-boot system would be a headache for me ： ╮(╯▽╰)╭)

[张守信(Shouxin Zhang)]

Joscha Mennicken said:

Doesn't WSL 2 run in some sort of VM? I'd expect that to add some CPU performance overhead, but to have better FS performance than on plain Windows. But I've never used it myself.

That sounds very reasonable. I will let you know how it performs running on a pure Linux system versus in a virtual machine after I've had a chance to test it.

[Chris Birkbeck]

Wang Jingting said:

Have you tried dual booting a Linux system instead of using WSL? I'm also curious about the difference between these choices.

I have done exactly this. I've not compared it to WSL, but I can say Ubuntu is significantly faster than native Windows at least.

[Kevin Buzzard]

I have switched to a MacBook Pro from an older Ubuntu machine and it's great, except that I've noticed that lake build in mathlib finishes essentially instantly on linux whereas you can see the mac very quickly counting to 6000. I was quite surprised by this.

[Chase Norman]

Wouldn’t that be internet speed?

[Henrik Böving]

No that would be the limiting factor for the initial lake exe cache get, lake build with a fetched cache doesn't talk to the internet

[Wang Jingting]

Chris Birkbeck said:

Wang Jingting said:

Have you tried dual booting a Linux system instead of using WSL? I'm also curious about the difference between these choices.

I have done exactly this. I've not compared it to WSL, but I can say Ubuntu is significantly faster than native Windows at least.

Yeah, actually that's how I setup my computer (on my computer, compiling in Linux is about 5 times faster than Windows), but I've never tried to use WSL, so I'm sort of curious about how that would perform.

[Philippe Duchon]

张守信(Shouxin Zhang) said:

Wang Jingting said:

Have you tried dual booting a Linux system instead of using WSL? I'm also curious about the difference between these choices.

I'll try to make the comparison after my functional analysis exam on June 17th. (To be honest, as a newbie, I think installing a dual-boot system would be a headache for me ： ╮(╯▽╰)╭)

The idea that installing a dual-boot system is more scary/difficult than working with Lean is a bit alien to me. At least, starting from a blank state, asking your favorite search engine for a tutorial, reading it for five minutes, then trying to follow it more or less blindly, you are way more likely to end up with a successul install than a successful proof that addition of the naturals is commutative.

But of course, we all have our personal preferences :slight_smile:

[张守信(Shouxin Zhang)]

Based on my latest test, my 9955HX3D on Ubuntu 24 compiles import Mathlib about 1 second faster than my unplugged Mac M4 Pro.

It's quite amazing; Lean files compile significantly faster on a native Linux system than on WSL.

I haven't yet tested the performance of the classic tactics rw?, apply?, and simp/simp_all. I'll do that after breakfast.

[张守信(Shouxin Zhang)]

When I plugged in my Mac, I found the apply? tactic seems to run faster on the M4 PRO than on my 9955HX3D. However, the difference is small, staying within 0.5s. This holds true for various scenarios: when apply? finds a direct solution, suggests potentially useful theorems, or fails.