Status of precompilation

Stream: lean4

[Scott Morrison]

Something I would love a summary of (@Henrik Böving, if you're in the mood, your last one was great! :-) is where we are at in terms of running the compiled versions of mathlib tactics, in other mathlib proofs. I know something is preventing us from doing this, but I don't understand what.

[Henrik Böving]

I dont know the specifics of that but the idea actually originates from the talk where I stole the picture from: http://leanprover.github.io/talks/WITS2022.pdf I was under the impression that even though it is difficult Sebastian can do it though?

[Jannis Limperg]

Scott Morrison said:

Something I would love a summary of (Henrik Böving, if you're in the mood, your last one was great! :-) is where we are at in terms of running the compiled versions of mathlib tactics, in other mathlib proofs. I know something is preventing us from doing this, but I don't understand what.

I think (but don't quote me on this) that this is a Lake issue. Lake currently knows how to pre-compile a whole package, so Std and Aesop are pre-compiled. But it does not know how to pre-compile individual files. And mathlib tactics can't easily be split into their own package since they depend on a lot of definitions and lemmas.

[Sebastian Ullrich]

It is actually the other way around - lake knows how to precompile individual modules (thus the option name) but not whole packages https://github.com/leanprover/lake/issues/136

[Sebastian Ullrich]

It appears that for current mathlib4 the overhead from the current precompilation scheme is larger than the speedup from avoiding interpretation. This is not too surprising to me as by the numbers I got the last time, "only" around 10% of the mathlib4 build is spent in the interpreter, so the margin for introducing additional overhead is not high.

[Sebastian Ullrich]

But this is for the one-size-fits-all solution of precompiling every computable definition in mathlib4; a more selective scheme should be able to get closer to saving those 10%

[Scott Morrison]

Is it possible, though, that expensive search tactics (e.g. library_search, propose, and rewrites are the ones that could benefit most from compilation? And these will never show up in your statistics because their uses are solely during exploration, and are not committed to the repo.

[Scott Morrison]

On the other hand, ring and linarith are slow tactics that do make it into the repo.

[Sebastian Ullrich]

Yes, good point. Unfortunately without the doomed PR linked in my second link, it's hard to measure the potential impact accurately.

[Sebastian Ullrich]

Well, it would not be hard to experiment with it though - set precompileModules := true in the lakefile, then use one of these tactics in a file importing the tactic. You can copy Lake's lean cmdline and remove the --load-dynlib arguments to compare the performance without having to change the lakefile again.

[Sebastian Ullrich]

Sebastian Ullrich said:

But this is for the one-size-fits-all solution of precompiling every computable definition in mathlib4; a more selective scheme should be able to get closer to saving those 10%

Good news: if I hard-code precompilation only for Aesop.*, Mathlib.Tactic.*, and Mathlib.Mathport.Rename, a full rebuild is 2% wall clock and 3.5% task clock faster than without precompilation

[Sebastian Ullrich]

It precompiled 453 modules into 35MB of shared libraries; that seems like an amount we could put in the cache even per platform, but also I should probably be more selective for Mathlib.Tactic in order to exclude tactics that are not performance-critical but come with a ton of dependencies.

[Notification Bot]

14 messages were moved here from #lean4 > What is the kernel, really?—and other fundamental questions by Sebastian Ullrich.

[Sebastian Ullrich]

What is still completely unclear at this point:

• What is the impact on other platforms?
• How much specifically is the linking and compilation overhead, and how much interpretation is left?
• What should be the proper Lake API for this? precompileModuleGlobs? /cc @Mac

[Jannis Limperg]

I'm a bit surprised that this doesn't have a bigger impact (though 2% is nothing to scoff at). Any theories? I guess many tactics spend most of their time in core routines, which are pre-compiled anyway?

[Sebastian Ullrich]

Again, 10% is the limit. I'm sure much of that is lost by the newly introduced overhead, but I intend to have the speedcenter give us more detailed figures there.

[Henrik Böving]

What speedup do we usually experienced with something purely compiled vs something purely interpreted? Do we have numbers on that?

[Sebastian Ullrich]

20x is definitely possible AFAIR

[Henrik Böving]

:O

[Scott Morrison]

Sebastian Ullrich said:

I should probably be more selective for Mathlib.Tactic in order to exclude tactics that are not performance-critical but come with a ton of dependencies.

If you push somewhere the setup that precompiles only Mathlib.Tactic.*, I'm happy to do the curation down to a smaller subset.

[Scott Morrison]

@Jannis Limperg, a conclusion from today's porting meeting is the precompilation of tactics is not compatible with our current olean caching strategy, and so if we bump the dependency on aesop, as in the PR https://github.com/leanprover-community/mathlib4/pull/3236 (which we won't merge!), then lake exe cache get is not going to work anymore.

[Scott Morrison]

Could you turn off tactic precompilation again, so we can continue tracking aesop while this is addressed?

[Jannis Limperg]

Precompilation is now disabled again. @Sebastian Ullrich I've also removed the trace messages that Aesop would print when profiler is enabled.

Btw, the destructProducts transparency change is coming next week since I'm on holiday this week.

[Mac Malone]

Sebastian Ullrich said:

• What should be the proper Lake API for this? precompileModuleGlobs? /cc Mac

Sorry, I just realized I missed the email notification for this mention during the flurry of discussion about the Lake subtree. The way I was thinking this would be done is something like so:

lean_lib Mathlib.Tactic where
   precompileModules := true
   -- any other options

lean_lib Mathlib where
   --- normal mathlib configuration

However, I have tested that this works. I think Lean (and Lake) may not currently permit two libraries to have the same prefix. If so, Mathlib.Tactic would likely have to be named MathlibTatic for now.

[Sebastian Ullrich]

Sebastian Ullrich said:

Again, 10% is the limit. I'm sure much of that is lost by the newly introduced overhead, but I intend to have the speedcenter give us more detailed figures there.

!4#3575. This is for Mathlib.Mathport.Rename only for now, which is a perfect first test case as it has no dependencies that have to be precompiled first but is perhaps the most-interpreted code in mathlib4.

[Sebastian Ullrich]

ToAdditive in contrast has a dependency closure of size 72, benchmarking now

[Sebastian Ullrich]

By the way, @Gabriel Ebner's new Lake progress display is the simplest way I'm aware of for computing the closure size of a module

$ lake clean && lake build Mathlib.Tactic.LibrarySearch
[0/13] Building Std.Lean.Expr
[0/17] Building Std.Tactic.OpenPrivate
[0/13] Building Std.Util.ExtendedBinder
[0/13] Building Std.Tactic.TryThis
[0/19] Building Std.Data.Option.Init.Lemmas
[0/20] Building Std.Tactic.HaveI
[0/28] Building Std.Lean.TagAttribute
[0/28] Building Std.Tactic.Unreachable
[0/32] Building Std.Tactic.SeqFocus
[0/34] Building Std.Tactic.ByCases
[0/38] Building Std.Lean.Parser
[0/38] Building Std.Tactic.GuardExpr
[0/169] Building Std.Lean.Meta.Basic
...
[168/169] Building Mathlib.Tactic.LibrarySearch

That's not small!

[Mario Carneiro]

is that a progress bar? because it seems to be going the wrong direction

[Mario Carneiro]

ideally std should be precompiled though, does it really need to be counted here?

[Sebastian Ullrich]

Mario Carneiro said:

is that a progress bar? because it seems to be going the wrong direction

Bad cropping on my part, it seems to go the right direction after hitting 169

[Mario Carneiro]

is that the number of files that have been discovered so far or something?

[Sebastian Ullrich]

Mario Carneiro said:

ideally std should be precompiled though, does it really need to be counted here?

That's a good question, it depends on whether loading the shared libs is negligible. But I'm assuming that generic meta programs like to_additive will not change all that often either, at least going forward.

[Mario Carneiro]

So the way I should read this is that Mathlib.Tactic.LibrarySearch depends on 169 other files

[Sebastian Ullrich]

I believe so

[Mario Carneiro]

because if I kept reading the output the number stops growing after [.../169]

[Sebastian Ullrich]

It does hit 168/169 in the end

[Mauricio Collares]

The progress bar is [completed/discovered], which is counter intuitive for parallel compilation

[Matthew Ballard]

:octopus: for a progress bar!

[Sebastian Ullrich]

Mario Carneiro said:

ideally std should be precompiled though, does it really need to be counted here?

Note that if we actually want to cache the shared libraries for all platforms, that effectively requires cross-compilation on CI

[Sebastian Ullrich]

The platform caching support is certainly the largest unsolved issue with this entire approach. Using precompilation only on some platforms is probably untenable, it would demote those other platforms to a second class with wildly differing performance profiles from the first class. Caching precompilation only on some or on no platforms is only acceptable if recompilation is fast enough, ideally a fraction of the time it takes to acquire the cache; as the PR is already at 85s native compilation, this does not appear feasible either without finding a sweet spot of optimization options. Cross-compilation finally should be achievable thanks to LLVM being a native cross-compiler and our toolchain being standalone, but I'm not sure yet how the actual caching would work.