precompileModules downstream of mathlib

Stream: lean4

[James Gallicchio]

It seems completely infeasible to have precompileModules := true downstream of mathlib. A lake build with prebuilt oleans present takes at least 25 minutes on my 12 core machine, and reloading file dependencies takes a minute or two (most of that time consumed by ld, from what I can tell). Which is unfortunate, because I want to write lazy proofs that just call slow automation tactics from mathlib.

Is there any way to specify a subset of modules to precompile? Or any other way to make it feasible to use this feature downstream of mathlib?

EDIT: clarified that lake build takes a while even with the prebuilt oleans

[Sebastian Ullrich]

"Downstream of mathlib" is not very precise, what size of dependency closure are we talking about here?

[James Gallicchio]

I think roughly half of mathlib? (is there a quick way to check?) I import Mathlib.Tactic somewhere which inflates the closure quite a bit.

[Kim Morrison]

import Mathlib.Tactic.Common might work better?

[James Gallicchio]

That appears to only cut out a couple hundred files. Let me figure out exactly which tactics I need.

[James Gallicchio]

Ok, I only import linarith, ring, and fincases.

[James Gallicchio]

(With dependencies, that gives 1400 ish modules)

[Kim Morrison]

Unfortunately the linarith -> ring -> norm_num chain of tactics picks up an absurd number of side dependencies...

[James Gallicchio]

And reducing the import closure is really only a bandaid on a feature that doesn't scale well...

[Yaël Dillies]

Note #9411 should help with that

[Yaël Dillies]

It doesn't really reduce the number of dependencies itself, but it makes it much easier to do so. And that's not just a bandaid. I need to reduce those imports for a mathematical reason: I need the map from ℚ≥0 to any DivisionSemiring.