Building lean/mathlib: Technology, Timings, References?

Stream: general

[Fabian Huch]

Are there any good references regarding the Lean build system (i.e., how the object files work, how long a full Lean/Mathlib build takes, what hardware is being used, etc.), or can somebody tell me about that? I can see the system in action on github, but other than that I just found a few references that multi-threading exists.

[Kim Morrison]

• make -C build/release -j32 in the lean4 repo takes <2 minutes (on a 16 core M2 Ultra)
• lake build takes about 20 minutes in the mathlib4 repo (it's been a while since I actually timed this). Mathlib CI runs on a combination of Github CI machines, and machines privately hosted by the Hoskinson centre.

[Kim Morrison]

There's no a lot written down about our build infrastructure outside of the .github/workflows directories in the lean4/Std/Mathlib repos.

[Fabian Huch]

Thanks for the info! Is this with precompiled olean files, or completely without?

[Fabian Huch]

So running the mathlib makefile took 28 minutes on my fastest workstation (24 core i9-12900K), and it appeared to use all cores. Does this seem reasonable?

[Mario Carneiro]

mathlib doesn't have a makefile, and I'm not sure what you mean by running it

[Mario Carneiro]

if you mean lake build then yes I would expect it to take about 20-30 minutes using 100% of a fast machine

[Mario Carneiro]

That will use precompiled things only if they happen to be lying around after a previous build or because you ran lake exe cache get. If you delete .lake then it will definitely not be using those caches. (However lean + lake itself is always downloaded pre-built by elan.)

[Mario Carneiro]

Most users don't use this workflow because building mathlib is too expensive. Instead, you run lake exe cache get and it will download built oleans from the cloud machines

[Fabian Huch]

Mario Carneiro said:

mathlib doesn't have a makefile, and I'm not sure what you mean by running it

I ran make, there is a GNUmakefile.

[Fabian Huch]

(Running on bbf2206 in mathlib4, to clarify things)

[Mario Carneiro]

so there is... I don't think it is used much

[Fabian Huch]

Though some of he tests in the end failed.

[Fabian Huch]

I see.

[Mario Carneiro]

looks like it is being used for orchestrating building the tests, which can't be run through lake ATM

[Mario Carneiro]

not sure what happened to the tests, I would expect them all to pass on master since they are run in CI. What error did you get?

[Mario Carneiro]

there is a note in the CI though:

bash -o pipefail -c "
# Tests use parts of ProofWidgets not imported by Mathlib.
# Ensure everything has been built.
lake build ProofWidgets
make -k -j 8 test"

[Mario Carneiro]

most likely if you just run make test without building ProofWidgets you will get an error about missing oleans or something

[Fabian Huch]

Yes, that was the error. I see.

[Mario Carneiro]

(this would have been handled automatically by lake if it understood how to build test files)

[Fabian Huch]

One more question: What are these tests? Are they relevant for the formalizations?

[Mario Carneiro]

many of them are testing the tactics, which are programs like any other and can have bugs in them

[Fabian Huch]

Thanks for all the info!

[Mario Carneiro]

(almost all of them in fact, most tests are named after the tactic under test)