KaehlerDifferential.mvPolynomialEquiv typechecking

Stream: mathlib4

[Kevin Buzzard]

I was fiddling with typeclass priorities and I found a change which had a positive impact on over 50 files but randomly had a big negative impact on the declaration docs#KaehlerDifferential.mvPolynomialEquiv . However there's already something wrong with this declaration; even before my change the kernel is having huge problems with typechecking some auxiliary definitions. Check out this trace on master (obtained by dumping

set_option trace.profiler.useHeartbeats true
set_option trace.profiler true

at the top of the file, compiling it on the command line (which takes ages and hammers your machine) and then inspecting the output):

info: Mathlib/RingTheory/Kaehler/Polynomial.lean:44:14: [Elab.async] [57765600.000000] Lean.addDecl
  [Kernel] [57765534.000000] ✅️ typechecking declarations [KaehlerDifferential.mvPolynomialEquiv._proof_1]
info: Mathlib/RingTheory/Kaehler/Polynomial.lean:38:15: [Elab.async] [54494621.000000] Lean.addDecl
  [Kernel] [54494569.000000] ✅️ typechecking declarations [KaehlerDifferential.mvPolynomialEquiv._proof_2]
info: Mathlib/RingTheory/Kaehler/Polynomial.lean:34:4: [Elab.async] [6230.000000] Lean.addDecl
  [Kernel] [6177.000000] ✅️ typechecking declarations [KaehlerDifferential.mvPolynomialEquiv._proof_3]
info: Mathlib/RingTheory/Kaehler/Polynomial.lean:34:4: [Elab.async] [49344.000000] Lean.addDecl
  [Kernel] [49290.000000] ✅️ typechecking declarations [KaehlerDifferential.mvPolynomialEquiv._proof_4]
info: Mathlib/RingTheory/Kaehler/Polynomial.lean:34:4: [Elab.async] [49335.000000] Lean.addDecl
  [Kernel] [49281.000000] ✅️ typechecking declarations [KaehlerDifferential.mvPolynomialEquiv._proof_5]

Most proofs are checked in milliseconds but KaehlerDifferential.mvPolynomialEquiv._proof_1 and proof_2 take four orders of magnitude more (the timing is in mheartbeats but this is several seconds; weirdly if I don't use heartbeats then I can't find the output in the trace, but I can see orange bars on VSCode sitting on the def long after the proof has compiled, which usually indicates the kernel having some trouble).

@Sebastian Ullrich magically added a -implicitDefEqProofs to a simp call in #33794 and this saved 77.5G instructions. I think that there are going to be plenty more examples in mathlib (particularly in the harder commutative algebra stuff which is being used in algebraic geometry) where the kernel is having a hard time and some of them might have simple fixes. But I can't find a simple fix for this one: I dumped -implicitDefEqProofs in front of all the simp calls but it didn't seem to fix the problem. Is there a way to understand what's happening here? I ask because my change made many timings better but it doubled the already absurdly long time it took to typecheck these two proofs, which is wrecking my argument for the change :-)

[Aaron Liu]

Do we know which part of the proof the kernel is having a hard time with? First I would start inserting sorry until it becomes fast.

[Kevin Buzzard]

Huh! I had assumed that the moment I started putting sorrys in the proof the kernel would just skip typechecking, but you're right, it's still slow even with some sorries in the proofs. Will investigate further.

[Aaron Liu]

well I narrowed it down

[Aaron Liu]

it seems the single branch of the Finsupp.induction_linear is somewhat slow

[Kevin Buzzard]

There are two things here, right? (1) the proofs are slow (orange bars on the entire proofs) and (2) after the proof has finished, the typechecking is also slow (orange bars just on the def line)

Rather annoyingly, I don't yet see how to see how many heartbeats typechecking is taking without compiling on the command line.(found it in the infoview)

[Aaron Liu]

yes, for now I'm only counting the typechecking after the proof

[Aaron Liu]

by putting it in the web editor and seeing how long the yellow bar remains

[Kevin Buzzard]

FWIW _proof_1 seems to be left_inv and _proof_2 is right_inv, perhaps unsurprisingly (note that they're not in this order in the code). I see -- so when I sorried one proof, typechecking of the declaration still took ages because it was still struggling with the other one.

[Aaron Liu]

well I figured out what's slow

[Aaron Liu]

docs#Derivation.liftKaehlerDifferential_comp_D is a problem for some reason

[Aaron Liu]

when simp uses it to rewrite the goal

[Aaron Liu]

specifically using this lemma to rewrite the goal takes a long time for the kernel to typecheck

[Aaron Liu]

if I rewrite the goal and then go back into the proof and replace the rewriting proof (the proof that the rewritten goal is equal to the original) with sorry then it's fast again

[Aaron Liu]

and if I have the lemma but don't use it to rewrite the goal it's fast again

[Aaron Liu]

so it's probably some typeclass unification or something

[Kevin Buzzard]

This sort of thing is typically not good:

                                                                        [] [181487.000000] ✅️ DistribMulAction.toDistribSMul =?= DistribMulAction.toDistribSMul ▼
                                                                          [delta] [181322.000000] ✅️ DistribMulAction.toDistribSMul =?= DistribMulAction.toDistribSMul ▼
                                                                            [] [52486.000000] ✅️ CommRing.toCommSemiring.toMonoidWithZero.toMonoid =?= CommRing.toCommSemiring.toMonoidWithZero.toMonoid ▼
                                                                              [] [52240.000000] ✅️ CommRing.toCommSemiring.toMonoidWithZero.1 =?= CommRing.toCommSemiring.toMonoidWithZero.1 ▼
                                                                                [] [51573.000000] ✅️ { toMul := CommRing.toCommSemiring.toMul, mul_assoc := ⋯, toOne := CommRing.toCommSemiring.toOne,
                                                                                      one_mul := ⋯, mul_one := ⋯,
                                                                                      npow := Semiring.npow,
                                                                                      npow_zero := ⋯,
                                                                                      npow_succ :=
                                                                                        ⋯ } =?= {
                                                                                      toMul :=
                                                                                        CommRing.toCommSemiring.toMul,
                                                                                      mul_assoc := ⋯,
                                                                                      toOne :=
                                                                                        CommRing.toCommSemiring.toOne,
                                                                                      one_mul := ⋯, mul_one := ⋯,
                                                                                      npow := Semiring.npow,
                                                                                      npow_zero := ⋯, npow_succ := ⋯ } ▼

[Kevin Buzzard]

Ploughing through the simp trace for liftKaehlerDifferential_comp_D with pp.all on, here is something which is taking quite a lot of heartbeats:

[isDefEq] [815425.000000] ✅️ @Module.{max u u_1, max u_1 u} (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R inst✝))
                          (@KaehlerDifferential.{u, max u_1 u} R
                            (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R inst✝)) inst✝
                            (@MvPolynomial.instCommRingMvPolynomial.{u, u_1} R σ inst✝)
                            (@MvPolynomial.algebra.{u, u, u_1} R R σ (@CommRing.toCommSemiring.{u} R inst✝)
                              (@CommRing.toCommSemiring.{u} R inst✝)
                              (@Algebra.id.{u} R (@CommRing.toCommSemiring.{u} R inst✝))))
                          (@CommSemiring.toSemiring.{max u u_1}
                            (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R inst✝))
                            (@MvPolynomial.commSemiring.{u, u_1} R σ (@CommRing.toCommSemiring.{u} R inst✝)))
                          (@AddCommGroup.toAddCommMonoid.{max u_1 u}
                            (@KaehlerDifferential.{u, max u_1 u} R
                              (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R inst✝)) inst✝
                              (@MvPolynomial.instCommRingMvPolynomial.{u, u_1} R σ inst✝)
                              (@MvPolynomial.algebra.{u, u, u_1} R R σ (@CommRing.toCommSemiring.{u} R inst✝)
                                (@CommRing.toCommSemiring.{u} R inst✝)
                                (@Algebra.id.{u} R (@CommRing.toCommSemiring.{u} R inst✝))))
                            (@instAddCommGroupKaehlerDifferential.{max u_1 u, u} R
                              (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R inst✝)) inst✝
                              (@MvPolynomial.instCommRingMvPolynomial.{u, u_1} R σ inst✝)
                              (@MvPolynomial.algebra.{u, u, u_1} R R σ (@CommRing.toCommSemiring.{u} R inst✝)
                                (@CommRing.toCommSemiring.{u} R inst✝)
                                (@Algebra.id.{u} R
                                  (@CommRing.toCommSemiring.{u} R
                                    inst✝))))) =?= @Module.{max u u_1, max u u_1}
                          (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R inst✝))
                          (@KaehlerDifferential.{u, max u u_1} R
                            (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R inst✝)) inst✝
                            (@MvPolynomial.instCommRingMvPolynomial.{u, u_1} R σ inst✝)
                            (@MvPolynomial.algebra.{u, u, u_1} R R σ (@CommRing.toCommSemiring.{u} R inst✝)
                              (@CommRing.toCommSemiring.{u} R inst✝)
                              (@Algebra.id.{u} R (@CommRing.toCommSemiring.{u} R inst✝))))
                          (@CommSemiring.toSemiring.{max u u_1}
                            (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R inst✝))
                            (@CommRing.toCommSemiring.{max u u_1}
                              (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R inst✝))
                              (@MvPolynomial.instCommRingMvPolynomial.{u, u_1} R σ inst✝)))
                          (@AddCommGroup.toAddCommMonoid.{max u u_1}
                            (@KaehlerDifferential.{u, max u u_1} R
                              (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R inst✝)) inst✝
                              (@MvPolynomial.instCommRingMvPolynomial.{u, u_1} R σ inst✝)
                              (@MvPolynomial.algebra.{u, u, u_1} R R σ (@CommRing.toCommSemiring.{u} R inst✝)
                                (@CommRing.toCommSemiring.{u} R inst✝)
                                (@Algebra.id.{u} R (@CommRing.toCommSemiring.{u} R inst✝))))
                            (@instAddCommGroupKaehlerDifferential.{max u u_1, u} R
                              (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R inst✝)) inst✝
                              (@MvPolynomial.instCommRingMvPolynomial.{u, u_1} R σ inst✝)
                              (@MvPolynomial.algebra.{u, u, u_1} R R σ (@CommRing.toCommSemiring.{u} R inst✝)
                                (@CommRing.toCommSemiring.{u} R inst✝)
                                (@Algebra.id.{u} R (@CommRing.toCommSemiring.{u} R inst✝)))))

The two terms there are almost the same. One difference (occuring throughout the term) is universe ordering: @Module.{max u u_1, max u_1 u}) vs @Module.{max u u_1, max u u_1}). The other one is

(@MvPolynomial.commSemiring.{u, u_1} R σ (@CommRing.toCommSemiring.{u} R i)) =
    (@CommRing.toCommSemiring.{max u u_1}
      (@MvPolynomial.{u_1, u} σ R (@CommRing.toCommSemiring.{u} R i))
      (@MvPolynomial.instCommRingMvPolynomial.{u, u_1} R σ i))

(i = inst✝) embedded in the two terms, and these are equal under with_reducible_and_instances rfl but not under with_reducible rfl.

Changing (σ : Type*) to (σ : Type u) makes the declaration instant, i.e. all problems magically go away (but presumably this isn't an acceptable change).

[Kevin Buzzard]

Oh lol, it's one of these: if I add two new universes t and w then (σ : Type w) is slow but (σ : Type t) is super-quick.

So the problem is that u_1 is after u in the alphabet.

[Aaron Liu]

Kevin Buzzard said:

Changing (σ : Type*) to (σ : Type u) makes the declaration instant, i.e. all problems magically go away (but presumably this isn't an acceptable change).

why not

[Kevin Buzzard]

Changing to Type u is no good because R already has Type u so the definition becomes less general. Changing to Type t maybe has some chance though. Christian Merten tried something like once before and Matt Ballard was not happy with the idea. However I am hoping that this time the extra debugging (thanks a lot for pointing me to the right place) will enable us to get further, although perhaps some people had managed to see this far the last time we discussed this sort of issue. I think Matt's main objection was "we don't have a clue what is going on so this looks like a dirty hack" and perhaps now we do.

#34088

[Edward van de Meent]

i suppose this example should go on the same heap as #26018 ? (the mathlib issue "Kernel type checking performance depends on lexicographic ordering of universe variables")

[Kevin Buzzard]

Yeah it's the same thing in the same part of mathlib. I didn't know there was an issue -- thanks.

[Edward van de Meent]

i figured there would be one since we've run into this weird behaviour before, but surprisingly there wasn't one on the lean4 repo...

[Edward van de Meent]

indeed it turned out to be reported as a mathlib issue (presumably because a proper MWE for this hasn't been found yet)

[Johan Commelin]

For others: part of this discussion has moved/continued at #lean4 > kernel universe normalization issue

[Anne Baanen]

Let's decide on how to move forward on this issue, at least in Mathlib. I assume (but I would be very happy to be corrected if I'm wrong) that a fix for lean4#12102 is not going to arrive soon. So in the meantime, shall we merge the workaround in #34088?

I would like to argue in favour of merging: if we close #34088 without merging, the price we pay is noticeably higher build times for each commit changing something upstream, until the slow unification issue is resolved. I find the gains of keeping the status quo quite small: v is not a much weirder name for a universe variable than u. (If we "accidentally" got the names in the right alphabetic order in the first place, we would not have wanted to change it to the current form.) And a Mathlib contributor who experiences a slow declaration is generally not immediately after going to look for and find a specific Lean issue and then also be able solve it. If we have multiple places in the source code referring to the same Lean bug, that is easily searchable evidence that we encountered the issue multiple times, and should help prioritizing this issue.

Also, we have previously merged similar workarounds. (e.g. #26008; maybe we should add a link to lean4#12102 in the comment?)

[Sébastien Gouëzel]

Yeah, now that we have a minimization and a report upstream, I think it makes sense to merge the workaround.

[Kevin Buzzard]

I spent a week or so occasionaly trying to save more time but I have now given up and I am happy with #34088 . I can make another universe change in the changed file which makes it even faster, but it makes another file slower, and if I then try to fix that file then it makes 5 more files slower. One universe name change made JacobiZariski +600G slower. The situation is random and awful. I conjecture that this universe nonsense is one of the reasons JacobiZariski is so bad.

In case people are wondering why I even care about making the declaration in this PR faster, I think it increases the argument for #34077 which is what I was really interested in before going down this universe rabbithole.

[Anne Baanen]

Thanks for the experiments! I'll merge #34088 in 24 hours, unless someone objects.