building mathlib on ubuntu v mac

Stream: general

[Kevin Buzzard]

I have a new mac laptop with an M4 Pro and 48 GB of memory. I also have an old but fast desktop running Ubuntu 24.04. I haven't updated mathlib for a while on either machine. So on both machines I did the following
(I'm on master in both, but behind):

cd Mathlib
git pull
rm -rf .lake
lake exe cache get!
time lake build
time lake build
time lake build

Obviously getting cache takes time because I removed .lake so I need to download everything; I only did this in an attempt to make sure I had a level playing field. But I don't care how long getting cache takes -- I care how long building takes. Here are the results.

Ubuntu:

buzzard@brutus:~/Mathlib$ time lake build
Build completed successfully (7239 jobs).

real    0m2.911s
user    0m3.183s
sys 0m0.559s
buzzard@brutus:~/Mathlib$ time lake build
Build completed successfully (7239 jobs).

real    0m1.939s
user    0m2.046s
sys 0m0.522s
buzzard@brutus:~/Mathlib$ time lake build
Build completed successfully (7239 jobs).

real    0m1.549s
user    0m1.765s
sys 0m0.460s
buzzard@brutus:~/Mathlib$

In practice it takes under 2 seconds to complete lake build on the Ubuntu machine.

Here are the resuts for the expensive mac which I bought specifically to do Lean quickly:

buzzard@IC-HWDXTW69VR Mathlib % time lake build
Build completed successfully (7239 jobs).
lake build  2.05s user 2.82s system 36% cpu 13.487 total
buzzard@IC-HWDXTW69VR Mathlib % time lake build
Build completed successfully (7239 jobs).
lake build  3.50s user 7.46s system 23% cpu 46.271 total
buzzard@IC-HWDXTW69VR Mathlib % time lake build
Build completed successfully (7239 jobs).
lake build  3.79s user 8.14s system 22% cpu 52.483 total
buzzard@IC-HWDXTW69VR Mathlib %

So in practice it takes well over 30 seconds to compile mathlib on the mac, even though we've just compiled it. Sometimes there can be a very long pause before anything happens, and then a very long wait on ⣯ [0/0] Running job computation (+ 0 more) and then a slowish count to 7000.

I then wrote this message and then went back to the mac and did time lake build again.

buzzard@IC-HWDXTW69VR Mathlib % time lake build
Build completed successfully (7239 jobs).
lake build  1.92s user 2.45s system 138% cpu 3.156 total
buzzard@IC-HWDXTW69VR Mathlib % time lake build
Build completed successfully (7239 jobs).
lake build  1.92s user 2.52s system 138% cpu 3.205 total
buzzard@IC-HWDXTW69VR Mathlib %

Now it's compiling in 3 seconds.

I then realised that I wanted to include the line which the mac stopped on in this message so I typed time lake build and after a second I hit ctrl-C so I could copy ⣯ [0/0] Running job computation into this message.

I then compiled again and we're back to 51 seconds.

buzzard@IC-HWDXTW69VR Mathlib % time lake build
⣯ [0/0] Running job computation (+ 0 more)^C
lake build  0.25s user 0.50s system 64% cpu 1.153 total
buzzard@IC-HWDXTW69VR Mathlib % time lake build
Build completed successfully (7239 jobs).
lake build  3.67s user 7.61s system 22% cpu 51.250 total
buzzard@IC-HWDXTW69VR Mathlib %

What is going on and how do I make it stop?

[Kevin Buzzard]

Huh, I waited for 15 minutes and then tried again.

buzzard@IC-HWDXTW69VR Mathlib % time lake build
Build completed successfully (7239 jobs).
lake build  3.46s user 7.10s system 20% cpu 51.025 total
buzzard@IC-HWDXTW69VR Mathlib % time lake build
Build completed successfully (7239 jobs).
lake build  1.92s user 2.44s system 133% cpu 3.257 total
buzzard@IC-HWDXTW69VR Mathlib %

After the pause, again I'm on nearly a minute compiling mathlib the first time, and then 3 seconds the second time. Note that I didn't do anything with mathlib in the interim. Note also that even when it's not misbehaving I am consistently under 2 seconds in Ubuntu and consistently over 3 seconds on the mac (but this is not something I'm particularly fussed about, it's the 51 second runs which annoy me).

[Chris Birkbeck]

Does your Mac have any antivirus software? ( I was having some slowdowns then realised the other day that mine had stupid windows defender since it's managed by my uni).

[Sebastian Ullrich]

It feels like macOS may be overeager at discarding the file system cache? Linux is usually happy to use any unused RAM for such purposes

[Kevin Buzzard]

Chris Birkbeck said:

Does your Mac have any antivirus software? ( I was having some slowdowns then realised the other day that mine had stupid windows defender since it's managed by my uni).

I don't know, I personally didn't put any antivirus software on it but this is a work laptop and it went through someone else before it got to me.

[Shreyas Srinivas]

If you are in the UK I am guessing they still push Sophos onto uni machines

[Matthew Ballard]

Performance of this is comparable natively on my Mac and in the Ubuntu VM sitting on it.

[Filippo A. E. Nuccio]

How much RAM do you have on the Ubuntu machine?

[Kevin Buzzard]

I want to come back to this. Yesterday I checked out the same commit of mathlib on my 5 year old desktop and my new mac. I ran lake exe cache get and then lake build on the command line, left everything to complete, and then I left both command line windows open for 24 hours.

I then came back to the windows and typed lake build again.

Here's the output on the ubuntu machine:

ubuntu.gif

1) Immediately goes to "running job computation"
2) two seconds later, starts counting to 7442 very quickly
3) gets there about 4 seconds later
4) one last second on "Running mathlib/Mathlib.default"

Total time around 7 seconds.

[now give me a second while I switch machines]

[Kevin Buzzard]

Here's what happens if I do exactly the same thing on the mac.

slow_on_mac.gif

1) Literally nothing happens (no output, no info) for around ten seconds (note that the Ubuntu machine finishes the entire job in under ten seconds)
2) "Running job computation" for maybe 20+ seconds.
3) Counts to 7442 over a period of about ten seconds.

Total time 46 seconds.

Is there something wrong with my set-up or are all mac users in this hell?

[Kevin Buzzard]

Specs: the Ubuntu machine is a 5 year old standard desktop with 32 gigs of ram; the mac is an M4 pro with 48 gigs of ram.

[Kevin Buzzard]

Matthew Ballard said:

Performance of this is comparable natively on my Mac and in the Ubuntu VM sitting on it.

So you're saying that this is something I just have to live with? I am now really regretting following the "just buy an expensive mac" suggestion when I asked for a fast laptop for Lean. I know that mac users all love their machines and I want to love my machine but it is such a step down from Ubuntu in practice when I'm working on FLT. I will do another experiment involving VS Code and post again in about 12 hours because I think there's another instance when I am seeing huge performance degradation on my laptop v desktop.

[Kevin Buzzard]

FWIW this was on mathlib commit b8aaf14a892866ba8333faac94f658b9dc557afa

[Kevin Buzzard]

I spend a surprisingly large amount of time doing Lean with poor or no internet; the more internet I have, the more people are asking me to do things. However I am very much open to running some VM; I had naturally assumed that any attempt to emulate another OS would obviously come with a performance hit but maybe I am out of date here?

[Chris Birkbeck]

I just ran this on my mac (which is slightly older than yours) and got lake build 8.97s user 2.65s system 418% cpu 2.774 total

[Matthew Ballard]

Kevin Buzzard said:

Is there something wrong with my set-up or are all mac users in this hell?

I am not in that hell. Where did my_venv come from?

[Chris Birkbeck]

Yes the venv is what I am wondering about as well

[Matthew Ballard]

Until Apple brings its M series virtualization to the iPad :prayer_beads:, I’m rocking a 5 year old M series MacBook Pro to compare

[Shreyas Srinivas]

Kevin it is possible that your employer updated your software including the antivirus which also probably reset the firewall settings

[Shreyas Srinivas]

Also I think that venv comes from trying to run blueprint

[Shreyas Srinivas]

I’d suggest deactivating it anyway before a test.

[Kevin Buzzard]

Yes the my_venv is so I can use lean blueprint. @Chris Birkbeck what happens if you wait an hour and then try again?

[Chris Birkbeck]

Lets find out.

[Kevin Buzzard]

For me the second lake build is fast if it's just after the first one, but slow if I leave it a while

[Chris Birkbeck]

Well, as a check I just tried this on some repos I've not touched in a few days, and its still takes around the same time. The one I ran above was for just basic mathlib, so I'll try that one later and see.

[Shreyas Srinivas]

Kevin Buzzard said:

For me the second lake build is fast if it's just after the first one, but slow if I leave it a while

were you working without cache the first time?

[Shreyas Srinivas]

As in, fetching cache?

[Kevin Buzzard]

ohnonono, I started by fetching cache. I am always running lake build on a project with all oleans present and correct. It's not my_venv (thank goodness, because I don't want to go without leanproject).

I do have some Imperial-related crapware running, I will try and figure out how to remove it. I am very mac-ignorant, I think I'll do this and then come back here, but I need to worry about the 2 talks I'm giving today first so it'll have to be the weekend.

[Chris Birkbeck]

So about an hour later : Build completed successfully (7454 jobs). lake build 7.21s user 6.47s system 341% cpu 4.007 total maybe a tiny bit slower but might just be more things open. Definitely not like what you see.

[Michael Stoll]

I noticed that there was a factor-10 difference in the unpacking step, too.

[Kevin Buzzard]

So thanks to everyone who helped. After discussion with Chris Birkbeck both here and at LLL yesterday I decided that it was the crapware on the machine that was probably the problem, and given that I don't use it for anything other than Lean and everything is backed up, I decided today to just factory reset the machine and not install the crapware (in fact I was quite surprised that I'd chosen to install any crapware the first time I set it up).

However it turned out to be not as easy as that. Imperial did buy this mac for me, and after the factory reset I got a popup saying "Remote Management: This Mac is owned by Imperial College London, remote management is required" (which is fair enough) and then I got a popup telling me that Microsoft 365, Microsoft Defender, Company Portal and Jamf Connect were going to be installed. I think Jamf connect is just doing some password management thing, and I can confirm that after just reinstalling VS Code, git and lean, I still have the same problem: "lake build" on mathlib is 10 seconds of no output, 20 seconds of "[0/0] Running job computation (+ 0 more)" and then back to normality, with a further immediate "lake build" being completely normal (just a few seconds) and then a third "lake build" five minutes later being back to being ridiculously slow.

I suspect that uninstalling WindowsMicrosoft Defender is not going to be possible so I might now have to take this up with Imperial IT.

[Chris Birkbeck]

FYI if you have admin rights you can uninstall windows defender but it's not straightforward...

[Yaël Dillies]

I assume it's not Windows Defender since you're on a mac

[Chris Birkbeck]

Well my uni did install windows defender on my Mac!

[Kevin Buzzard]

Indeed it is called "Microsoft Defender".

[Chris Birkbeck]

Oh lol sure maybe is was "Microsoft" defender. What I noticed was that something called wdavdaemon was using up lots of my CPU which annoyed me and it turned out to be this.

[Shreyas Srinivas]

You can’t get rid of that managed software thing without Imperial’s IT people supporting you.

[Shreyas Srinivas]

They’d basically have to agree to not have any oversight over the laptop which most orgs in the English speaking world won’t permit

[Sébastien Gouëzel]

Can you open Microsoft Defender and tell it not to scan your project directory? On windows, this makes a huge difference.

[Michael Rothgang]

I'm also reminded of this gotcha on mac (related to code signing): https://nnethercote.github.io/2025/09/04/faster-rust-builds-on-mac.html

[Michael Rothgang]

Perhaps that's not relevant here/ perhaps it only becomes relevant if you need to compile the cache executable...

[Michael Rothgang]

(Another very random Mac performance fact: are you charging your mac from the left?)

[Michael Rothgang]

I realise that these might not be related to the issue you're reporting, Kevin --- but they might be useful to know regardless.

[Michael Rothgang]

@Mac Malone Do you think detecting if Gatekeeper (more precisely, XProtect) is enabled on mac and warning about this could be a useful thing for lake to do? Does lake create new executables (for lake exe cache, lake test, etc.) often enough for this to be worth it? See e.g. this post for some detail what I'm talking about.

(Disclaimer: I am not a mac user, so all my knowledge about this issue is from the above post.)

[Sebastian Ullrich]

Let's not worry about issues without evidence of affecting users for now

[Kevin Buzzard]

Sébastien Gouëzel said:

Can you open Microsoft Defender and tell it not to scan your project directory? On windows, this makes a huge difference.

Oh my goodness me, that is the solution.

In fact it was not quite the solution: I told Windows Defender to not scan my lean project directory and the problem still persisted. So then I told it to not scan anything in my home directory and this seems to have completely solved the problem. For literally months I have opened FLT on my laptop, started a file with import Mathlib, pasted some code and then waited for between 30 seconds and a minute for anything to happen. Today things are very different! Thank you so much @Sébastien Gouëzel , I owe you a nice bottle of wine.

I know it might sound ridiculous but I literally did not even know I was running Microsoft Defender until I factory reset the machine and this time watched more carefully to see what Imperial were doing to my machine. In normal use the top right hand of my screen had a bunch of icons on them but I had never even looked at them, they were just there from day 1, I have never even used this operating system before, and I just regarded them as "stuff which macs have and which I don't need to understand". It was only when it dawned on me that it was the crapware which was the problem that I started to figure out exactly what I was stuck with.

Thank you to everyone who helped; this has literally made a very large difference to my working life. I had even got into the habit of opening VS Code and then going to check emails or Zulip because I knew that it would be unresponsive for about a minute.

[Sébastien Gouëzel]

I'm really glad it made a difference for you. It also made a huge difference for me (on Windows) when I found the setting.

The next question is: is it possible to detect if Windows Defender is active on the Lean directory (or whatever is relevant when starting mathlib) and issue a warning about this if so? I'm sure this would be helpful to many more people than just the two of us.

[Kenny Lau]

what is the setting on windows?

[Sébastien Gouëzel]

Go in windows defender, protection against viruses and threats (or something like that, I am translating from French), Parameters of protection against viruses and threats, manage parameters. There is an "Exclusions" item for folders which shouldn't be scanned. I have added the various Lean project folders and the mathlib cache there.

[Kenny Lau]

ah I did exactly that and observed no change (see #general > slowdown on initial use ), do I need to restart my computer?

[Sebastian Ullrich]

You should also add .elan fwiw

[Sébastien Gouëzel]

Normally, the slowdown is only on the initial launch (because then the files are fresh in cache). Do you have a slowdown on each launch?

[Kenny Lau]

every time i click restart file, basically

[Sébastien Gouëzel]

Weird. I don't know what is going on then.

[Sebastian Ullrich]

To be more explicit: start by excluding your entire home directory, like Kevin did, to ensure all relevant folders are covered

[Kenny Lau]

is there a way to see which folders Lean uses?

[Kenny Lau]

do I need to exclude vscode as well?

[Patrick Massot]

Kevin Buzzard said:

Thank you so much Sébastien Gouëzel , I owe you a nice bottle of wine.

Oh, that’s a nice way to pay for productivity boosts! How many bottles do I get if I install Linux on your Mac next time I see you?

[Ching-Tsun Chou]

I just saw this thread. Here's a datapoint from my M1 MacBook Air:

ctchou-macair:~/play/mathlib4 $ time lake build
Build completed successfully (7473 jobs).
lake build 5.27s user 2.65s system 160% cpu 4.947 total
ctchou-macair:~/play/mathlib4 $ time lake build
Build completed successfully (7473 jobs).
lake build 5.25s user 2.46s system 168% cpu 4.573 total
ctchou-macair:~/play/mathlib4 $ time lake build
Build completed successfully (7473 jobs).
lake build 5.21s user 2.44s system 165% cpu 4.635 total

[Shreyas Srinivas]

Btw @Kevin: I noticed that in the output of time command in your gif for the Mac, the real time (as in what you observe on a clock while waiting for lake to finish) is much larger than the cumulative cpu time spent in both user and system (I.e. kernel mode). Typically the real time that you would observe is less than this cpu time because the cpu time is spread out across multiple cores. So what you observe could be a sign that

1. you have some crapware running or
2. You have a bad network connection or
3. Your antivirus or firewall is blocking something.

[Kevin Buzzard]

Shreyas the problem is solved: it was Microsoft Defender (which I cannot remove as when they bought the mac for me, Imperial reported its serial number to Apple who now force me to install and run software on Imperial's list). I stopped it scanning the relevant directories and now have consistently fast builds.