shake

Stream: mathlib4

[Kim Morrison]

Now that Mathlib is on v4.28.0-rc1 and the new shake is available as lake shake, it's time to update Mathlib CI so it runs lake shake again. I think the current preferred settings are lake shake --add-public --keep-implied --keep-prefix and --fix is you want it to apply the changes.

Currently this suggests quite a few changes, so we'll have to make another PR before enabling this in CI.

[Kim Morrison]

Does anyone know the current state of automatically adding commits to a PR? I would love to not have to run shake myself, and to have CI run it, try rebuilding, and if that worked just apply the changes automatically.

[Kim Morrison]

#34511

[Kim Morrison]

(@Johan Commelin, I used the x <command line> format for the commit message. Is your machinery ready to handle this?)

[Kim Morrison]

@Sebastian Ullrich, something I don't see how to do currently is to only run shake on a single file. I'd like to be able to do this, so it minimizes the imports of just that one file (plus adding imports as required downstream, of course).

I think this would be quite useful when looking at the rebuild critical path e.g. https://speed.lean-lang.org/mathlib4-out/be6dc76a4049aab3ce7ae14bfd2a19720c8f43d2/

[Kim Morrison]

(I only just learnt how to find the rebuild critical path today:

• go to https://radar.lean-lang.org
• select "mathlib4" in the top right (or jump direct to https://radar.lean-lang.org/repos/mathlib4)
• select a recent commit (most recent at the top)
• click "Lakeprof report"

[Yaël Dillies]

#mathlib4 > The long pole in mathlib @ 💬

[Sebastian Ullrich]

Kim Morrison said:

Sebastian Ullrich, something I don't see how to do currently is to only run shake on a single file. I'd like to be able to do this, so it minimizes the imports of just that one file (plus adding imports as required downstream, of course).

Can you say more, is it that you want to run this specific file under different flags than the rest?

[Kim Morrison]

I don't want any suggestions for anything upstream of it, but I want to convert public import to import just in that file.

[Sebastian Ullrich]

Making sure that the base commit has already been shaken is likely the easiest option to avoid unrelated changes, no? Then I think you can just do import changes yourself in the file (which gives you more control on e.g. removing only a subset of public imports) and rerun shake afterwards. As it will use the oleans from the working base commit, it should understand that it needs to add imports to unbreak downstream files, even if the package is not actually buildable before doing so. I'll see if I can test this on Yaël's example

[Snir Broshi]

Kim Morrison said:

Does anyone know the current state of automatically adding commits to a PR? I would love to not have to run shake myself, and to have CI run it, try rebuilding, and if that worked just apply the changes automatically.

Mathlib uses pre-commit whose config is in .pre-commit-config.yaml.
Currently it only removes trailing whitespace and then commits automatically, e.g. this commit in #34353.

It seems pretty easy to add hooks from the current repo, just need to add an entry in the config that says to run lake shake --fix ....

(I'm not sure if there are some other ways Mathlib commits automatically. It can be done without pre-commit of course, but it's a nice existing framework that is externally maintained)

[Sebastian Ullrich]

Sebastian Ullrich said:

I'll see if I can test this on Yaël's example

Hmm that was a bit anticlimactic as it turned out there was nothing to fix downstream. But at least Shake seemed to be fine with this workflow. I've put both steps in #34523 though they could also be separated.

[Bryan Gin-ge Chen]

I would be happy to review PRs adding such functionality to our pre-commit setup! Some other commands that might be worth running automatically are lake exe lint-style --fix and ./scripts/lint-bib.sh && rm docs/references.bib.old (from the old bot fix style command which sadly doesn't seem to work at the moment.)

[Snir Broshi]

and lake exe mk_all? (probably requires disabling the existing lake exe mk_all --check that fails the build, unless it comes after pre-commit)

[Kim Morrison]

Sebastian Ullrich said:

Making sure that the base commit has already been shaken is likely the easiest option to avoid unrelated changes, no? Then I think you can just do import changes yourself in the file (which gives you more control on e.g. removing only a subset of public imports) and rerun shake afterwards. As it will use the oleans from the working base commit, it should understand that it needs to add imports to unbreak downstream files, even if the package is not actually buildable before doing so. I'll see if I can test this on Yaël's example

I think we're still talking past each other here.

@Sebastian Ullrich, your commit https://github.com/leanprover-community/mathlib4/pull/34523/commits/efcc944fcb422f46c75540d0eeac8ffff134d809 then broke the build, because we need to add public import below.

I want to be able to run lake shake <...options...> --only Mathlib/Analysis/Normed/Lp/SmoothApprox.lean, which will have the effect of working out which public imports in SmoothApprox can be converted into imports, and make all necessary adjustments downstream.

Currently I don't think shake can do this, and if we want to reduce public import to import where possible in a single file, it has to be done by hand.

[Sebastian Ullrich]

Yes, I had some issues with Lake and thought it built. I see now that I would have to make some changes to shake to support my approach as well. I'm happy to support something like --only but can you think of similar use cases we may want to support with a more general interface? E.g. for core we might want to shake anything but Init with --keep-public, which cannot be split into two separate runs

[Sebastian Ullrich]

A third interesting idea triggered by a comment by @Paul Reichert: if we want to e.g. minimize Lp.SmoothApprox more thoroughly, we likely want it be kept minimized that way in the future as well, no? That would suggest an in-source annotation like -- shake: no-add-public, which would not require any new cmdline interface

[Kim Morrison]

I've encountered a weird situation on the shake PR. #34511

At commit c997929cf0568c908e2de8476739b89ce8240ae9 (the current head of that PR branch), lake build Mathlib.Control.Traversable.Equiv produces an error, but opening the file in VSCode it looks fine.

Would someone be able to try reproducing this for me? It is potentially a module system bug.

[Kevin Buzzard]

I can confirm that I get error: Mathlib/Control/Traversable/Equiv.lean:138:29: Unknown identifier `functor_norm` on command line and it builds fine in VS Code.

[Kevin Buzzard]

Hovering over functor_norm in VS Code I get the surprising message

A simp lemma specification is:

• optional ↑ or ↓ to specify use before or after entering the subterm
• optional ← to use the lemma backward
• thm for the theorem to rewrite with

[Kim Morrison]

Okay, can I bump this one up to some combination of @Sebastian Ullrich, @Mac Malone and @Marc Huisinga? Divergences between lake build and VS Code triggered by running shake seems tricky.

[Mac Malone]

@Kim Morrison Within the module system, the server loads more data about its imports than lake build does. Namely, it loads server metadata from olean.server and compiled code from .ir (e.g., for #eval to work). If elaboration relies on this additional data, a build can fail where the interactive session does not. For instance, shake may have removed a meta import in the transitive import graph that some Mathlib meta code (e.g., for prodoucing functor_norm) needed but Shake thought was unnecessary.

[Mac Malone]

Sadly, I am not sufficiently familiar with the breadth of Mathlib meta code to likely be able to debug this.

[Kevin Buzzard]

FWIW adding import Mathlib.Tactic.Attr.Register (the file where docs#Parser.Attr.functor_norm is defined) (or adding public import Mathlib.Tactic.Attr.Register) to Mathlib/Control/Traversable/Equiv.lean makes this file build on command line.

[Sebastian Ullrich]

Okay, this took a short while to analyze in full depth. The issue indeed is that functor_norm simply isn't imported anymore, so the cmdline behavior is correct; lean#12375 will ensure shake does not discard such imports. The divergence between server and cmdline here is a separate issue, which ultimately stems from simpsets being registered via initialize. This part will require some more thinking.