Adapting Mathlib to `v4.29.0-rc1`

Stream: mathlib4

[Kim Morrison]

Please read the announcement about v4.29.0-rc1.

[Kim Morrison]

A few things to start the ball rolling:

• Everyone will notice merge conflicts resulting from the additions of set_option backward.isDefEq.respectTransparency false in many places in Mathlib. Please help out newcomers dealing with this!
• If you're working on a new file, is it completely okay to add set_option backward.isDefEq.respectTransparency false at the top of the file, and not worry about this process further.
• If you're working on existing files, our preference is that you try to localize set_option to individual declarations where possible. This will help us triage, identify problems, and track improvements.
• Nearly always, these set_options are required "at the point of use", but there are occasional places in Mathlib where a set_option is needed on a declaration that otherwise compiles, but is needed to prevent errors downstream. If possible, we'd ask that when adding these you leave a comment on the same line like -- needed in X.Y.Z

[Robin Arnez]

Just to make sure, is #35500 (disable backward.isDefEq.respectTransparency globally) interfering with any plans?

[Kim Morrison]

More generally:

• We are very aware this is disruptive. We do not believe that all of these set_options represent problems in Mathlib, although many do! We are working harder on further fixes to Lean, and there will be more release candidates soon which should alleviate the need for these.
• It is super helpful if contributors can provide an #mwe showing a problem that looks like it needs to be fixed in Lean. We will analyze these and try to fix asap. Community members are already hard at work on this at #general > backward.isDefEq.respectTransparency @ 💬
• We are really determined to reach a good conclusion to these problems; we are fixing a longstanding problem in Lean's typeclass inference, and once we sort out the wrinkles, this will bring better performance and predictability to Lean.

[Snir Broshi]

Thank you!
Could you explain a bit what the changes do specifically, perhaps with MWEs that the 2 big changes break and are considered intentional rather than bugs? (i.e. what "wrong" behavior did Mathlib rely on)

[Snir Broshi]

Does lean#12179 mean that some defeq checks automatically upgrade defs to abbrevs? Or automatically added @[expose] or @[reducible]?
Edit: docs#Lean.Meta.TransparencyMode contains some relevant info

[Kim Morrison]

Previously, isDefEq was unfolding semireducible arguments when checking equalities of implicit arguments (i.e. treating anything sitting in an implicit position as if it were reducible).

[Kim Morrison]

We think that lean#12564 should resolve many of the problems experienced in Mathlib so far. We're testing it now.

[Kim Morrison]

I have to pause now, but if anyone would like to contribute fixes on the lean-pr-testing-12564 branch, that would be super helpful.

[Kim Morrison]

Also, some good news:

Henrik Böving said:

I was just looking at the mathlib instructions count:
image.png

Thanks to v4.28 and v4.29 we managed to push instruction count back to where it was 3 months ago despite mathlib adding around 150k lines in the mean time :tada: !

λ git diff --stat ef549b7b128a834178a5f25fbcdf75c3aa32deb7
 8160 files changed, 325220 insertions(+), 142632 deletions(-)