Assistance on lean-pr-testing-12564

Stream: mathlib4

[Kim Morrison]

We have a candidate fix for v4.29.0-rc1, in particular the #mwe from #general > backward.isDefEq.respectTransparency @ 💬 , in lean#12564.

[Kim Morrison]

However this itself causes further breakages in Mathlib, although relatively quite few. Could I ask for assistance on this, so we can efficiently get through this and deploy lean#12564 in an rc2?

[Kim Morrison]

The problems break up into two classes: broken proofs, which so far I have just sorried on the branch, and missing instances. Some instances I have already added.

If you add more instances, please put #adaptation_note /-- Needed after leanprover/lean4#12564 -/ before them, so we can review/reduce duplication at some point.

[Kim Morrison]

So far the instances I've had to add seem like reasonable things, and supplying them has just been a matter of inferInstanceAs <| ...some slight unfolding of the goal .... There are some other instances which now fail, but I haven't investigated how Mathlib master supplies them, e.g. [Algebra R S] : Module (MvPolynomial X R) (MvPolynomial X S).

[Kim Morrison]

For both the instances / broken proofs, ideally contributors can just push fixes to the branch (maybe say so here!). Even extremely hacky proofs are welcome, we can just merge with an #adaptation_note and clean up post rc2. The gloves are off, here. :-)

[Kim Morrison]

Even more useful is if you can identify something that is broken but shouldn't be, and then please tell us about it here, and we can coordinate making a Mathlib free #mwe to send back to lean#12564.

[Kim Morrison]

Here are the current files where assistance would be appreciated. (I am cheekily pinging the "Authors:" of each of the files. That's why you put your name there, right? :-)

Files with declaration uses sorry (warnings only)

File	First sorry	Authors
Algebra/BigOperators/Field.lean	L35	@Bhavik Mehta, @Daniel Weber
Algebra/Category/Grp/FilteredColimits.lean	L74	@Justus Springer
Algebra/Category/ModuleCat/Differentials/Presheaf.lean	L78	@Joël Riou
Analysis/RCLike/TangentCone.lean	L24	@Sébastien Gouëzel
Analysis/Real/Hyperreal.lean	L200	@Abhimanyu Pallavi Sudhir
Geometry/RingedSpace/OpenImmersion.lean	L989	@Andrew Yang
LinearAlgebra/CliffordAlgebra/Grading.lean	L46	@Eric Wieser
LinearAlgebra/Matrix/Charpoly/Coeff.lean	L147	@Aaron Anderson, @Jalex Stark
LinearAlgebra/Matrix/Determinant/Basic.lean	L285	@Kenny Lau, @Chris Hughes, @Anne Baanen
LinearAlgebra/Matrix/SpecialLinearGroup.lean	L349	@Anne Baanen, Wen Yang
LinearAlgebra/SymplecticGroup.lean	L61	@Matej Penciak, @Moritz Doll, Fabien Clery
NumberTheory/Padics/MahlerBasis.lean	L282	Giulio Caflisch, @David Loeffler
RingTheory/Algebraic/Integral.lean	L653	@Johan Commelin
RingTheory/Extension/Generators.lean	L244	@Andrew Yang
RingTheory/MvPolynomial/Groebner.lean	L236	@Antoine Chambert-Loir
RingTheory/MvPolynomial/MonomialOrder.lean	L996	@Antoine Chambert-Loir
Topology/Algebra/Module/Equiv.lean	L1001	@Jan-David Salchow, @Sébastien Gouëzel, @Jean Lo, @Yury G. Kudryashov, @Frédéric Dupuis

Files with errors (first error per file)

File	First error	Error type	Authors
Algebra/Category/ModuleCat/Differentials/Presheaf.lean	L60	failed to synthesize: HSMul ↑(R.obj X) ↑(M.obj X) ?m	@Joël Riou
Analysis/Normed/Algebra/UnitizationL1.lean	L108	failed to synthesize: Module R (Unitization 𝕜 A)	@Jireh Loreaux
Analysis/Real/Hyperreal.lean	L147	overloaded, errors (application type mismatch)	@Abhimanyu Pallavi Sudhir
LinearAlgebra/CliffordAlgebra/Grading.lean	L33	failed to synthesize: HPow (Submodule R (CliffordAlgebra Q)) ℕ ?m	@Eric Wieser
LinearAlgebra/ExteriorAlgebra/Basic.lean	L80	failed to synthesize: HPow (Submodule R (ExteriorAlgebra R M)) ℕ ?m	@Zhangir Azerbayev, @Adam Topaz, @Eric Wieser
NumberTheory/Padics/MahlerBasis.lean	L275	failed to synthesize: Module ℤ_[p] ℤ_[p]	Giulio Caflisch, @David Loeffler
RingTheory/Algebraic/Integral.lean	L565	failed to synthesize: Module (MvPolynomial σ R) (MvPolynomial σ S)	@Johan Commelin
RingTheory/Kaehler/Polynomial.lean	L66	failed to synthesize: Module (MvPolynomial σ R) (σ →₀ MvPolynomial σ R)	@Andrew Yang
RingTheory/LocalRing/ResidueField/Ideal.lean	L141	failed to synthesize: Module R I.ResidueField	@Andrew Yang
RingTheory/MvPolynomial/Groebner.lean	L131	failed to synthesize: Module (MvPolynomial σ R) (MvPolynomial σ R)	@Antoine Chambert-Loir

[Snir Broshi]

Do you mean push to https://github.com/leanprover-community/mathlib4-nightly-testing/tree/lean-pr-testing-12564, fixing any sorries?

[Snir Broshi]

The sorry links in the table are all 404 to me, the branch isn't in your fork

[Kim Morrison]

Snir Broshi said:

The sorry links in the table are all 404 to me, the branch isn't in your fork

Links all fixed.

[Kim Morrison]

Snir Broshi said:

Do you mean push to https://github.com/leanprover-community/mathlib4-nightly-testing/tree/lean-pr-testing-12564, fixing any sorries?

Yes please. For users that don't have the ability to push direct to that branch, please make a PR to that branch, and mention it here. I will merge asap.

[Kim Morrison]

(I'm happy to add anyone who regularly contributes in the nightly-testing channel to the nightly-testing group, which will give write access to such branches.)

[Matej Penciak]

I made a PR to fix the proofs in LinearAlgebra/SymplecticGroup.lean: https://github.com/leanprover-community/mathlib4-nightly-testing/pull/183

The sorrys amounted to adding an instance by hand for Module R (Matrix (l ⊕ l) (l ⊕ l) R so that the neg_smul and neg_smul_neg lemmas could fire.

[Kim Morrison]

Oh no, most of the broken proofs can actually be fixed by adding more set_option backward.isDefeq.respectTransparency!

[Kim Morrison]

@Matej Penciak, I think that needing to add that instance by hand is a deeper problem that we should minimize, rather than fixing by hand here. Those proofs in SymplecticGroup for now work by adding set_option, so I'll do that on the branch for now.

[Kim Morrison]

Okay, as usual I've been hasty --- let me retract the request for help on this branch for moment. I'm going to see how far I get can adding more set_options, and if that results in a complete build then I will write a script to see how many we can remove elsewhere.

[Kim Morrison]

So far so good. I have a complete build now.

[Robin Arnez]

I have a different fix (which also achieves a full build) that works more with unification hints. That makes the amount of new set_options needed quite low but it might also be a bit hacky to allow Matrix m n a = m -> n -> a reducibly...

[Robin Arnez]

I think there is a general problem of what to do with type defs because instance search is inevitably going to run into situations where it needs to unify the declaration with its body.

[Jireh Loreaux]

I'm happy to look at the error you pinged me for here, but it sounds like you don't want us to? Or is the point that it's appreciated, but not urgent. With the flood of all the discussion related to these changes to core and Mathlib breakage, I'm not sure where we stand.

[Kim Morrison]

@Jireh Loreaux, no longer urgent, I realised I can bash through these problems with more set_option backward..... So investigating what is going on in any pinged file is helpful, but not at all urgent anymore. Sorry for the noise, I'll update again in cases I need help. :-)

[Joël Riou]

I did push https://github.com/leanprover-community/mathlib4-nightly-testing/commit/96f47cae3df2fc99cef7f88ef5aa8cbe350e0c60

[Kim Morrison]

Joël Riou said:

I did push https://github.com/leanprover-community/mathlib4-nightly-testing/commit/96f47cae3df2fc99cef7f88ef5aa8cbe350e0c60

Thanks!

[Kim Morrison]

Update re: lean#12564. It's a mixed bag. It requires adding about 120 new set_option backward.isDefEq.respectTransparency false, but then allows removing 800 other ones...

Progress, but far from complete.

We also have lean#12567 and lean#12572, which we hope will help further, but don't have results for yet.

[Antoine Chambert-Loir]

I tried to start helping, but gh pr checkout 12564 gives me

GraphQL: Could not resolve to a PullRequest with the number of 12564. (repository.pullRequest)

[Robin Arnez]

You'd need to checkout lean-pr-testing-12564 on https://github.com/leanprover-community/mathlib-nightly-testing, not the PR itself

[Antoine Chambert-Loir]

Do I first need to fork that repository?

[Robin Arnez]

You can also use your mathlib fork, you just need to add a remote, i.e. git remote add <whatever> <link>

[Robin Arnez]

And then you can fetch from lean-pr-testing-12564 from <whatever>