lake option

Stream: lean4

[Scott Morrison]

Kevin Buzzard said:

Why can't we have a erm lake? option which just says "yes please, compile all the lean files in this project, because that's obviously what we want, like most projects"

Can we have a think about ways to reduce the pain of contributors having to maintain Mathlib.lean? This is an annoying pain point.

I'd be happy for options that either worked without any Mathlib.lean at all, or options that just automatically updated it with a lake build (although perhaps we can't even assume that PR authors are running this before committing).

:ping_pong: @Mac Malone for thoughts?

[Arthur Paulino]

Isn't there a PR that implements the update for that file with a Lake script?

As far as I remember, keeping a Mathlib.lean file is not a necessity from the perspective of the Lean 4 toolchain: it's there for mathlib's own maintenance reasons (CI stuff?)

So moving towards that direction would probably require distilling the all reasons why it exists and then evaluate an alternative route for each of them

[Adam Topaz]

Have we considered using globs := #[.andSubmodules …] as a lake option with an empty ’Mathlib.lean` file? @Alex J. Best taught be this trick.

[Arthur Paulino]

I do remember someone mentioning this a while ago. And in my memory, one of the reasons why Mathlib.lean is needed is due to how the linters run, which I don't understand (needs confirmation!)

Another reason is the current implementation of Cache, which infers all the files that need to have oleans cached (and downloaded) by traversing imports, starting from Mathlib.lean

[Mac Malone]

Scott Morrison said:

I'd be happy for options that either worked without any Mathlib.lean at all, or options that just automatically updated it with a lake build (although perhaps we can't even assume that PR authors are running this before committing).

Arthur Paulino said:

Isn't there a PR that implements the update for that file with a Lake script?

Yep, mathlib4#5593. @Scott Morrison was concerned about the script increasing configuration elaboration time, but that should no longer be a concern with lean4#2480.

[Scott Morrison]

If someone were interested, they could rebase #5593 onto #6910 (which is the PR that brings lean4#2480 to mathlib), and then check the elaboration time issue again.

[Arthur Paulino]

cc @Anand Rao Tadipatri
(I hope I ping'd the right person)

[Anand Rao Tadipatri]

Thanks for the ping. I've been busy with travel lately, but I'd be glad to benchmark the elaboration time and add an option to build Mathlib.Tactic over the weekend.