Mathlib dependencies (eg Aesop)

Stream: mathlib4

[Artie Khovanov]

Jannis kindly pushed out a quick bugfix to a problem I was having with Aesop. I'd like to test out the new behaviour in a project I have downstream of Mathlib (and eventually use it in a Mathlib PR). What is the process for Mathlib dependencies being updated, and how can I see when it has happened? I'm happy to wait for whatever internal process but I don't know what exactly I'm waiting for.

[Ruben Van de Velde]

If it's landed in aesop, mathlib should get it in due course through a PR like #32647

[Artie Khovanov]

Got it, thanks. Do you know how regularly the bot runs?

[Chris Henson]

It looks like this workflow is scheduled for every hour?

[Bryan Gin-ge Chen]

The PR is at #32878 and it was opened 9 hours ago, however it looks like its build was taking longer than an hour so the scheduled workflow pushed new updates to it and CI was getting canceled repeatedly. I guess these updates corresponded to actual new commits to aesop, so assuming Jannis is done for now, the build should finish this time :fingers_crossed:

[Artie Khovanov]

Yeah looks like the last time the aesop dependency was updated in mathlib is when Kim manually(?) bumped the toolchain

[Artie Khovanov]

Bryan Gin-ge Chen said:

The PR is at #32878 and it was opened 9 hours ago, however it looks like its build was taking longer than an hour so the scheduled workflow pushed new updates to it and CI was getting canceled repeatedly. I guess these updates corresponded to actual new commits to aesop, so assuming Jannis is done for now, the build should finish this time :fingers_crossed:

Oh right, I see! Interesting to get a glimpse of how the sausage is made, as it were. Thanks everyone.

My understanding is that dependencies get updated pretty much instantly, in principle, but the dependency needs to stay the same for long enough that a build can finish.

[Bryan Gin-ge Chen]

Yeah, though if the build times stay long we may want to reduce the frequency of the workflow so we can at least get some of the incoming changes tested against mathlib. By the way, here are the threads where the build results should be reported; hopefully we'll see some results there in an hour or so:

• #nightly-testing > Mathlib `lake update` failure
• #nightly-testing > Mathlib `lake update` success

[Artie Khovanov]

oh wow ✔ [7746/7749] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (3084s)

[Bryan Gin-ge Chen]

I commented on the PR and added a blocking label to it since we shouldn't merge this until this slowdown is addressed (the bot will keep putting the auto-merge-after-CI label on it). cc @Jannis Limperg who I pinged on the PR too.

[Artie Khovanov]

Oh is this not normal? /gen

[Bryan Gin-ge Chen]

The same file took 23 seconds to build on a recent build of master: https://github.com/leanprover-community/mathlib4/actions/runs/20208676021/job/58011152402 (which is still long, but not 3000 seconds long)

[Jannis Limperg]

I'm taking a look at the performance regression. (I wonder how it's even possible for a file to take this long and not time out. ^^)

[Jannis Limperg]

There's something profoundly weird going on here. I've bisected the regression down to Aesop commit 76b54a2. When I lake build Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/Basic.lean with this Aesop version, it does indeed take super long (and maybe doesn't finish at all; I was too impatient to let it run). However, when I lake env lean Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/Basic.lean, after building the dependencies, it finishes in reasonable time, but reports sorry warnings on two other declarations that appear before the declaration that times out. @Mac Malone @Sebastian Ullrich any quick guesses what could be going on? What could be relevant differences between these two modes of operation?

[Kim Morrison]

https://github.com/leanprover-community/mathlib4-nightly-testing/pull/144 is also timing out. I don't see any particular evidence it is due to aesop, except that there's this thread about aesop causing time outs!

[Kim Morrison]

Can we just revert the changes to aesop and deploy them once tested? I'd prefer not to have to manually prevent aesop updates in nightly-testing/master in the meantime.

[Kim Morrison]

Kim Morrison said:

https://github.com/leanprover-community/mathlib4-nightly-testing/pull/144 is also timing out. I don't see any particular evidence it is due to aesop, except that there's this thread about aesop causing time outs!

Sorry, false alarm, restarting CI fixed this.

[Sebastian Ullrich]

Jannis Limperg said:

There's something profoundly weird going on here. I've bisected the regression down to Aesop commit 76b54a2. When I lake build Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/Basic.lean with this Aesop version, it does indeed take super long (and maybe doesn't finish at all; I was too impatient to let it run). However, when I lake env lean Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/Basic.lean, after building the dependencies, it finishes in reasonable time, but reports sorry warnings on two other declarations that appear before the declaration that times out. Mac Malone Sebastian Ullrich any quick guesses what could be going on? What could be relevant differences between these two modes of operation?

From a quick options bisection, looks like it's -Dbackward.proofsInPublic=true. So in other words, it appears that new restrictions introduced by the module system would make the file work here (probably by delaying some by blocks until mvars are assigned), except that because of incompatibilities of existing Mathlib code with these new restrictions, the restrictions are temporarily disabled and so we run the file with the semantics before the module system in this specific respect. So adding set_option backward.proofsInPublic false seems like a valid workaround to me as we do want this to be the Mathlib-global default eventually.

[Johan Commelin]

Note that #32934 just got merged, which sets proofsInPublic to false globally.

[Jeremy Tan]

#32945 begins the process of removing them

[Artie Khovanov]

#32878 now builds quickly!

[Jeremy Tan]

I found that to_additive is not correctly exporting hidden declarations. I tried removing the backward.proofsInPublic in GroupTheory.OreLocalization.Basic and got the following downstream errors:

error: Mathlib/GroupTheory/MonoidLocalization/Basic.lean:197:2: @[to_additive] failed. The translated value is not type correct. For help, see the docstring of `to_additive`, section `Troubleshooting`. Failed to add declaration
AddLocalization.r_iff_oreEqv_r:
Unknown constant `AddOreLocalization.oreEqv._proof_2`
error: Mathlib/GroupTheory/MonoidLocalization/Basic.lean:225:2: @[to_additive] failed. The translated value is not type correct. For help, see the docstring of `to_additive`, section `Troubleshooting`. Failed to add declaration
AddLocalization.mk_eq_mk_iff:
Unknown constant `AddLocalization.r_iff_oreEqv_r`
error: Mathlib/GroupTheory/MonoidLocalization/Basic.lean:234:2: @[to_additive] failed. The translated value is not type correct. For help, see the docstring of `to_additive`, section `Troubleshooting`. Failed to add declaration
AddLocalization.rec:
Unknown constant `AddLocalization.mk_eq_mk_iff`
error: Mathlib/GroupTheory/MonoidLocalization/Basic.lean:271:2: @[to_additive] failed. The translated value is not type correct. For help, see the docstring of `to_additive`, section `Troubleshooting`. Failed to add declaration
AddLocalization.ndrec_mk:
Unknown constant `AddLocalization.mk_eq_mk_iff`
error: Mathlib/GroupTheory/MonoidLocalization/Basic.lean:284:2: Type mismatch
  rec ?m.20 ⋯ x
has type
  ?m.18 x
but is expected to have type
  p

[Michael Rothgang]

CC @Jovan Gerbscheid @Floris van Doorn on the above to_additive find

[Jovan Gerbscheid]

Hmm, I think the issue may be that currently, the approach for translating auxiliary proofs is to unfold them, then do the whole translation, and then to refold them. But I think this is a bad approach for proofs generated by proofsInPublic, and instead we should not unfold them, but translate them directly.

One anoying issue with that though is that the dont_translate := ... option doesn't get passed along.

[Jovan Gerbscheid]

Or it might just be a matter of exporting declarations that aren't being exported.

[Jovan Gerbscheid]

I've had a closer look, and it turns out that removing the proofsInPublic option causesOreLocalization.oreEqv._proof_1 to instead be called OreLocalization.oreEqv._proof_2.

But the additive version generated by to_additive is still ._proof_1.

So far, to_additive was relying on always one of these two things happening:

• The names just happen to have the same postfix (e.g. _proof_1), so it works out.
• The auxiliary theorem is never used again, so it's not a problem that we don't know how to translate it.

[Floris van Doorn]

This looks like the same issue as #metaprogramming / tactics > to_additive and module system. It can be fixed by using import all on some modules.

[Floris van Doorn]

Jovan Gerbscheid said:

Hmm, I think the issue may be that currently, the approach for translating auxiliary proofs is to unfold them, then do the whole translation, and then to refold them. But I think this is a bad approach for proofs generated by proofsInPublic, and instead we should not unfold them, but translate them directly.

One anoying issue with that though is that the dont_translate := ... option doesn't get passed along.

I don't know what proofsInPublic is, but the reason to unfold aux-decls is to get enough context to apply the to_additive-heuristics. If we don't unfold them, it can be very hard to decide what to additivize on an aux-decl.

[Jovan Gerbscheid]

Ah right if you import all, then the aux theorem can be unfolded.

[Jovan Gerbscheid]

Is there a way to access a theorem body even if it has not explicitly been imported via import all?

[Sebastian Ullrich]

Is there no way we could additivize the aux decl in the module it was declared in?

[Jovan Gerbscheid]

If I recall correctly, that is what we did up to about a year ago, and then @Kyle Miller changed it so that the proofs are unfolded, which was necessary in one of the lean version bumps?

[Kyle Miller]

What I'm remembering is that there was an improvement to the way proof terms are abstracted from definitions that unfortunately changed their types in such a way that they no longer were meaningful to to_additive — and that previously they were only accidentally meaningful. The fix Floris and I made was to unfold these proofs, since that way in context it was clear how to additivize. Then it would be sure to abstractNestedProofs for defs to put things back into a similar form.

I don't recall to_additive needing the _proof_1 postfixes needing to be the same, unless what you're saying @Jovan Gerbscheid is that this is one of the conditions that happens to make the current code work when using the new module system.

Why is it that additivization is happening across modules?

If it's necessary, could there be a flag to make the abstracted proofs (and simp aux lemmas) necessary for a definition be exported?

[Jovan Gerbscheid]

Yeah I take that back about the _proof_1 postfixes having needed to match. But indeed now with the mulodule system this does happen to make the current code work when the postfixes match.