mathlib cache works for lean_lib but not for lean_exe?

Stream: mathlib4

[David Richter]

Hi, I have a question about the mathlib cache.

When I do
$ lake new testproject math $ cd testproject $ printf "import Mathlib" > Testproject.lean $ lake build
it seems to use the cache.

But when I append another lean_exe target to the end of the file (for example via
$ printf "[[lean_exe]]\nname = \"main\"\nroot = \"Testproject\"" >> lakefile.toml)
and then try to build that lean_exe target:
$ lake build main

Then it continues running from 7xxx/13xxx, for example:
⡿ [7197/13952] Running Mathlib.Logic.Nontrivial.Defs:c.o...

So it seems to me that the cache only works for lean_lib targets, but not for building lean_exe targets?
But maybe I'm just confused.

(Versions:
$ elan --version elan 4.1.2 (58e8d545e 2025-05-26) $ lake --version Lake version 5.0.0-src+7c3ca70 (Lean version 4.22.0-rc3))

[Eric Wieser]

The cache only contains olean files not .o files

[Eric Wieser]

The latter are a lot more platform dependent

[Eric Wieser]

It's very unlikely you actually need to import mathlib at compile time in your executable though

[David Richter]

Kinda makes sense. Is there a way to avoid compiling the mathlib, when I import mathlib in an executable target, but only use something from mathlib in a proof? For example importing mathlib to prove termination of a function.

[Eric Wieser]

Have you already used #min_imports to at least only import the bits of mathlib you actually used?

[Eric Wieser]

Maybe @Sebastian Ullrich can comment on whether this is something that later iterations of the module system can hope to help with; having "proof-only" depencies which are excluded from compilation.

[Sebastian Ullrich]

Hmm, that could be an interesting additional phase, a noncomputable import if you will. But it would be great to have clear data on its impact first, e.g. measured time overhead for significant projects

[Eric Wieser]

My fear is that such projects will never produce such data, and will instead say "I guess we can't depend on mathlib" and then rebuild the theory they need from scratch

[Eric Wieser]

But I guess it makes a big difference whether @David Richter needs FLT to prove termination or whether they need something lightweight from Mathlib.Data

[Eric Wieser]

Could lean_exe do some dependency analysis to skip modules whose IR isn't actually needed? Or does the presence of initializers make this unsound?

[Sebastian Ullrich]

That, and it would mean native compilation would have to wait for elaboration of all modules to finish first

[Eric Wieser]

Sebastian Ullrich said:

could be an interesting additional phase, a noncomputable import if you will

I guess you need some error message work here, so that whenin C.lean you import B which noncomputable import As, you get an error telling you to import A if you want to compile a x.

[David Richter]

I got a project from someone else and was trying to figure out why the cache was not working. I suppose the person waited for everything to compile once, some (long) time ago, forgot about it, and only when sharing the development the problem became apparent again.

A warning that building mathlib in an exectuable target cannot use the cache would be useful, for the reason of platform-specific compilation. This may have pointed me in the correct direction. I'm not sure which tool would be responsible for this warning though. Lake build?

I suppose it would be convenient to be able to noncomputable import mathlib stuff, because currently is surprising that building (even the same file) for either a library target or a executable target makes such a big difference in compile time. I suppose this could increase the amount of people that use mathlib, but not develop it? Currently one would rather rewrite the proof trying to not depend on mathlib in the executable. I haven't thought about this from the perspective of writing large projects, I'm more in the mindspace of having a simple project with a few files, and being surprised that switching between an library target and an executable target makes such a big difference in compile time.

[Eric Wieser]

Currently one would rather rewrite the proof trying to not depend on mathlib in the executable.

I want to be very clear that "not depending on mathlib (the project)" is a very different goal than "not using import Mathlib"

[Eric Wieser]

Can you run #min_imports in your file and replace import Mathlib with what it suggests?

[David Richter]

Sorry, this might not be very interesting. I figured out, it did depended on nothing... :)

I imagine the person who wrote the code happened to import 'Mathlib.Tactic', as a general way to write proofs everywhere, but then eventually simplified the code to not use it?