Expected Lean 4 build time?

Stream: lean4

[Mac]

I just timed how long it takes for my computer to build Lean 4 from scratch (in a Windows 10 MSYS2 environment) using time make and got the following result:

real    117m21.664s
user    1m34.093s
sys     6m36.292s

Is this comparable to others' build times? Or is there perhaps a bottleneck I may be missing that resulted in my times? I am curious if these times seem reasonable or not.

[Gabriel Ebner]

Six minutes of cpu time sounds about right. The real time is crazy though--did you put your computer to sleep while it was building?

[Mac]

nope, I ran the build in the background while doing other things on my computer (though not particularly CPU intensive things -- just watching YouTube videos and coding)

[Sebastian Ullrich]

Definitely not expected, even the GitHub Actions Windows runner is way faster

[Mac]

okay, I will explore more into the bottlenecks may be -- I did try this in a different location from my normal build setup, so I will try build again there and seeing if I get more reasonable times.

[Mac]

also, what, for reference, would be consider reasonable from scratch build times for Lean 4? (without running make in parallel with -jN)

[Daniel Fabian]

@Mac, would it be possible for you to try and build with WSL (ideally Wsl2) too? It would at least help us confirm that it has something to do with MSYS

[Sebastian Ullrich]

The Actions runner takes something like 15min with and 30min without ccache cache, which is on two cores

[Sebastian Ullrich]

Btw, I would be very suspicious of those 1m34s user time. Perhaps msys2 is not measuring the right thing there.

[Gabriel Ebner]

I just built current Lean 4 with plain make, and it took 26.86 mins (on linux, no caches). So 1.5 hours seems awfully long, even for a single-threaded build on windows.

[Johan Commelin]

But Gabriel, your machine also builds mathlib 5 faster than my server...

[Johan Commelin]

I don't trust any numbers coming from you to be representative of normal build times :joy: You clearly have some quantum computer under your desk or something. :stuck_out_tongue_wink:

[Gabriel Ebner]

The single-threaded performance should be comparable though. (A build with all cores is of course much faster and only takes 3 minutes, 37 seconds.)

[Johan Commelin]

/me is still cautious :laughing:

[Mac]

fyi, I am also currently building on a hard disk rather than an SSD so that may also be a factor.

[Sebastian Ullrich]

Upgrade straight to a RAM disk then :laughing:

[Mac]

note that I do have an SSD in this computer, I am just (for some reason) not building on it XD

[Daniel Fabian]

Disk IO can be a drastic contribution to build times. We usually use NVMe drives for that reason and it helps a lot. Also, WSL1 was severely slower with disk IO than WSL2. I'm not sure if MSYS has similar struggles, but it may be worth double-checking.

[Julian Berman]

Here (M1 ARM, not-very-powerful MB Air, make -j4): 111.61 real 281.10 user 33.49 sys (where the units are seconds).

[Gabriel Ebner]

This is surprisingly fast, is this with ccache or a debug build?

[Julian Berman]

I have ccache installed, but didn't do anything particularly to tell it to use it -- does it normally announce it used it in the output?

[Julian Berman]

anecdotally this build time I just got "feels" like what I normally get when pulling and rebuilding, it's typically fast enough that I just go do some small thing and come back and it's done.

[Gabriel Ebner]

I think it uses ccache by default, yes.

[Julian Berman]

Aha, got it.

[Sebastian Ullrich]

In fact Lean only prints out something if it can't enable ccache, since usually it's a no-brainer to use it

[Sebastian Ullrich]

Like, the CI has a 98% cache hit rate :)

[Gabriel Ebner]

There's also a massive difference with compilers and build options. With gcc and RelWithDebInfo it's 220s, with gcc and Release it's 185s, and with clang and Release it's 167s. Interestingly, the cpu time is actually higher with the clang build.

[Mac]

So I tested it out in my usual setup and got:

real    74m34.808s
user    1m31.529s
sys     6m23.311s

My next test will be on WSL(2) (still on HDD) and the test after that will be on the SSD. I probably won't do that until 8-10 hours from now as I intend to head off to sleep soon.

[Mac]

I will probably try installing ccache (if I don't already have it) and try after those two tests.

[Sebastian Ullrich]

Just make sure to build on the Linux partition with WSL2, since accessing the Windows one is even slower than WSL1 afaik

[Mac]

oh, in that case, I probably should do a MSYS2 SSD test first as I think the WSL2 partition is on my SSD as well.

[Julian Berman]

With export CCACHE_DISABLE=1, I get: 358.54 real 1299.16 user 51.34 sys

[Sebastian Ullrich]

Ah, that actually sounds more realistic than my guessed CI numbers. For a single module and in release mode, C compilation time absolutely dominates Lean compilation time, but it is also much more parallelizable (average stdlib .olean parallelism is something like ~3?)

[Gabriel Ebner]

There are several C file that take almost a minute to compile on my machine, they really reduce the parallelism.

[Sebastian Ullrich]

Yeah, I want to take a look at them soon since I'm not planning to upgrade my hardware again anytime soon...

[Sebastian Ullrich]

Elab.Do is the worst offender since it transitively depends on basically everything but the server

[Mac]

The MSYS2 SSD build got the following times:

real    79m1.068s
user    1m33.734s
sys     6m51.160s

As such, SSD vs HDD doesn't really seem to have a significant effect on the build time (at least in my setup).

[Daniel Fabian]

wow, I sure am interested in the WSL2 test then :D

[Mac]

also, by the way, I did have ccache installed (in MSYS2)

[Mac]

On a slightly unrelated note, the link for Linux (Ubuntu) in the Building Lean documentation is broken. The actual file has the version number in its name, but the link doesn't.

[Mac]

also, interestingly enough, the lastest cmake on Ubuntu (18.04) apt is 3.10.2 which is too old for Lean.

[Daniel Fabian]

i mean... on ubuntu, nix be thy friend ;-)

[Mac]

I am not sure I want to go through the process of learning nix just to do some build time tests XD

[Sebastian Ullrich]

We try to support the latest Ubuntu LTS, which is 20.04

[Mac]

ah, makes sense

[Mac]

I'm curious: are any of the other times people gave tests on MSYS2 Windows or are these all comparisons to a Linux OS build times? I wonder if this may be a "not optimized for MSYS2" problem.

[Andrew Ashworth]

if build time is an issue

[Andrew Ashworth]

i would try Clang first

[Andrew Ashworth]

or maybe not first, but "in addition to"

[Sebastian Ullrich]

Mac said:

I'm curious: are any of the other times people gave tests on MSYS2 Windows or are these all comparisons to a Linux OS build times? I wonder if this may be a "not optimized for MSYS2" problem.

The CI uses MSYS2, take a look for yourself

[Mac]

I finished running a test on WSL2 Ubuntu (LTS 20.04) and got the following times:

real    46m8.091s
user    44m46.209s
sys     1m17.504s

[Mac]

So, yes, WSL2 build times appear to be much faster than MSYS2.

[Mac]

However, unless WSL2 can cross-compile Lean for regular Window/MSYS2, I am not sure how much this helps (as the currently built executable, I believe, can only be run within WSL2).

[Mac]

Also note, for reference, that my WSL2 is using GCC 9 whereas my MSYS2 is using GCC 10.

[Mac]

Sebastian Ullrich said:

The CI uses MSYS2, take a look for yourself

On this point, is the GitHub CI for Lean 4 really comparable to a regular machine? I didn't really expect that.

[Mac]

Actually, looking at the Windows CI build times. They are generally on the order of 15m for make -j4 so if we naively single-thread that by multiplying the time by 4, it would come to around an 1hr/60m build time. This is worse than my WSL2 build time and better than my MSYS2 build time (thus further indicating that WSL2 build times are, in fact, likely significantly faster than MSYS2 build times). It is also better than my MSYS2 by about ~15-20m which, while significant, is not that big of a difference (i.e. my times are about 30% worse). I certainly would still like to improve my times, but this at least suggests that my times are not that insanely off base.

[Wojciech Nawrocki]

@Mac MinGW emulates some Unix system calls in userland in a way that's not very efficient -- see here. On the other hand, WSL1 used to call directly into the NT kernel and WSL2 is just a VM running natively.

[Daniel Fabian]

Well that's only half the story, though

[Daniel Fabian]

Because nix shortens build times to 5 min or usually

[Daniel Fabian]

So wsl2 would still help a lot before we replicate something clever in lake

[Mac]

In fact, the update stage0 times on the CI can take on the order of 30m with make -j4 which could be about 120m single-threaded. So, in fact, my from-scratch build times on MSYS2 may, in fact, be much faster than the CI.

[Mac]

The only reason that normal CI builds take 10-15 minutes (with make -j4) may be due to some form of caching (ex. ccache?)

[Mac]

One thing I differently learned form this though is that I should be passing -jN to make at all times. I do have 6 dual-thread cores on my machine so -j10 would probably significantly decrease build times. :grinning:

[Daniel Fabian]

I thought the rule of thumb was n virtual cores + 1

[Mac]

Maybe it is? I don't have enough experience/knowledge in that area to know. I also would like to be be doing other things while being so (I did n-2) to avoid maximally taxing my machine. But that may be unnecessary.

[Mac]

With make -j10 (on a 6 physical/12 logical core machine) using MSYS2 I got:

real    10m24.999s
user    1m58.663s
sys     8m29.935s

[Daniel Fabian]

That feels better than 1 hour?

[Mac]

Yeah 10min is better than an 1hr 20m. XD