What is wrong with RingTheory.Kaehler?

Stream: mathlib4

[Kevin Buzzard]

This is from #7257.

Screenshot-from-2023-09-26-18-20-47.png

Whatever could explain that? RingTheory.Kaehler is just a laughing stock. Every time someone sneezes in the vicinity of mathlib it takes slightly longer to compile. What is going on? Where does one start debugging?

[Kevin Buzzard]

Line 419

local instance instR : Module R (KaehlerDifferential.ideal R S).cotangentIdeal :=
  Submodule.module' _

The profiler trace is

[Elab.command] [2.316087s] /-- A shortcut instance to prevent timing out. Hopefully to be removed in the future. -/
    local instance instR : Module R (KaehlerDifferential.ideal R S).cotangentIdeal :=
      Submodule.module' _ ▼
  [step] [0.032803s] expected type: Prop, term
      IsScalarTower R S M ▶
  [step] [0.033099s] expected type: Type (max v u), term
      Module R (KaehlerDifferential.ideal R S).cotangentIdeal ▶
  [step] [1.319372s] expected type: Module R { x // x ∈ Ideal.cotangentIdeal (KaehlerDifferential.ideal R S) }, term
      Submodule.module' _ ▼
    [Meta.synthInstance] [0.125008s] ✅ SMul R (S ⊗[R] S ⧸ KaehlerDifferential.ideal R S ^ 2) ▶
    [Meta.isDefEq] [0.012858s] ✅ ?m.760468 =?= Submodule.Quotient.instSMul' (KaehlerDifferential.ideal R S ^ 2) ▶
    [Meta.synthInstance] [0.847184s] ✅ Module R (S ⊗[R] S ⧸ KaehlerDifferential.ideal R S ^ 2) ▶
    [Meta.isDefEq] [0.247414s] ✅ ?m.760469 =?= Submodule.Quotient.module' (KaehlerDifferential.ideal R S ^ 2) ▼
      [assign] [0.247408s] ✅ ?m.760469 := Submodule.Quotient.module' (KaehlerDifferential.ideal R S ^ 2) ▼
        [checkTypes] [0.247371s] ✅ (?m.760469 : Module R
              (S ⊗[R] S ⧸
                KaehlerDifferential.ideal R S ^
                  2)) := (Submodule.Quotient.module'
              (KaehlerDifferential.ideal R S ^ 2) : Module R (S ⊗[R] S ⧸ KaehlerDifferential.ideal R S ^ 2)) ▼
          [] [0.247367s] ✅ Module R
                (S ⊗[R] S ⧸
                  KaehlerDifferential.ideal R S ^ 2) =?= Module R (S ⊗[R] S ⧸ KaehlerDifferential.ideal R S ^ 2) ▼
            [] [0.012813s] ✅ S ⊗[R] S ⧸ KaehlerDifferential.ideal R S ^ 2 =?= S ⊗[R] S ⧸ KaehlerDifferential.ideal R S ^ 2 ▶
            [] [0.234528s] ✅ NonUnitalNonAssocSemiring.toAddCommMonoid =?= AddCommGroup.toAddCommMonoid ▼
              [] [0.234426s] ✅ NonUnitalNonAssocSemiring.toAddCommMonoid =?= AddCommMonoid.mk _ ▼
                [] [0.234419s] ✅ NonAssocSemiring.toNonUnitalNonAssocSemiring.1 =?= AddCommMonoid.mk _ ▼
                  [] [0.234356s] ✅ AddCommMonoid.mk _ =?= AddCommMonoid.mk _ ▼
                    [] [0.025764s] ✅ RingCon.Quotient
                          (Ideal.Quotient.ringCon
                            (KaehlerDifferential.ideal R S ^ 2)) =?= S ⊗[R] S ⧸ KaehlerDifferential.ideal R S ^ 2 ▶
                    [] [0.208557s] ✅ AddMonoidWithOne.toAddMonoid =?= SubNegMonoid.toAddMonoid ▼
                      [] [0.208449s] ✅ AddGroupWithOne.toAddMonoidWithOne.2 =?= AddGroup.toSubNegMonoid.1 ▼
                        [] [0.208404s] ✅ AddMonoidWithOne.toAddMonoid =?= SubNegMonoid.toAddMonoid ▼
                          [] [0.208378s] ✅ (Function.Surjective.addMonoidWithOne Quotient.mk'' _ _ _ _ _
                                  _).2 =?= (Function.Surjective.subNegMonoid Quotient.mk'' _ _ _ _ _ _ _).1 ▼
                            [] [0.208356s] ✅ AddMonoid.mk _ _ AddMonoid.nsmul =?= AddMonoid.mk _ _ AddMonoid.nsmul ▼
                              [] [0.052568s] ✅ AddMonoid.nsmul =?= AddMonoid.nsmul ▶
                              [] [0.025516s] ✅ RingCon.Quotient
                                    (Ideal.Quotient.ringCon
                                      (KaehlerDifferential.ideal R S ^
                                        2)) =?= AddCon.Quotient
                                    (QuotientAddGroup.con (Submodule.toAddSubgroup (KaehlerDifferential.ideal R S ^ 2))) ▶
                              [] [0.078742s] ✅ AddMonoid.toAddSemigroup =?= AddMonoid.toAddSemigroup ▶
                              [] [0.051482s] ✅ AddMonoid.toZero =?= AddMonoid.toZero ▶
    [Meta.synthInstance] [0.051575s] ✅ IsScalarTower R (S ⊗[R] S ⧸ KaehlerDifferential.ideal R S ^ 2)
          (S ⊗[R] S ⧸ KaehlerDifferential.ideal R S ^ 2) ▶
    [Meta.isDefEq] [0.015287s] ✅ ?m.760470 =?= isScalarTower_R_right R S ▶
  [Kernel] [0.025764s] typechecking declaration
All Messages (3)

and all that [] [0.078742s] ✅ AddMonoid.toAddSemigroup =?= AddMonoid.toAddSemigroup ▶ stuff looks superficially like it's a with problem. @Matthew Ballard have you eliminated that possibility though?

If

[] [0.234528s] ✅ NonUnitalNonAssocSemiring.toAddCommMonoid =?= AddCommGroup.toAddCommMonoid ▼

is anything to go by, we're paying a lot in typeclass inference in that file.

[Matthew Ballard]

#6854 is a more targeted elimination of with in Function.Surjective.X/ Function.Injective.X def's used in these instances. The regressions from CI are very similar.

[Matthew Ballard]

This comports with my poking at the synthesis traces in this file and in AG

[Matthew Ballard]

#6858 is probably a better reference

[Kevin Buzzard]

#6854 never compiled, was never benched as far as I can see, and has now been closed. Is that what you meant?

OK maybe it's not a with issue: this

[Meta.isDefEq] [0.489021s] ✅ SubNegMonoid.toAddMonoid =?= SubNegMonoid.toAddMonoid

is unfolding to things which really aren't syntactically equal. The divergence is here:

  [Meta.isDefEq] [0.112779s] ✅ fun
          n x ↦
        n •
          x =?= fun
          n x ↦
        n • x
    [Meta.isDefEq] [0.057235s] ✅ {
          x //
          x ∈
            ↑AddSubgroup.opposite
              (Submodule.toAddSubgroup
                (KaehlerDifferential.ideal
                    R
                    S •
                  ⊤)) } =?= {
          x //
          x ∈
            ↑AddSubgroup.opposite
              (Submodule.toAddSubgroup
                (Submodule.restrictScalars
                  S
                  (KaehlerDifferential.ideal
                      R
                      S •
                    ⊤))) }

Note the extra Submodule.restrictScalars on one side but not the other.

[Matthew Ballard]

Those weren't benched. But there were timeouts all over Kaehler (and Jacobson)

[Matthew Ballard]

I don't see the AG consequences there but digging through things in AG landed me back at Function.Injective/Function.Surjective def's also

[Kevin Buzzard]

Oh I understand your posts now :-) I'm supposed to be looking at the CI failures! Yeah this is the sort of thing I meant by "if you sneeze near mathlib it times out". I think Jireh had a similar thing -- "I'm working with C* algebras and I changed something and Kaehler broke even though it has nothing to do with what I'm doing"

[Matthew Ballard]

But #6858 only really touches one file which seems like a nerve for Kaehler

[Matthew Ballard]

(It is not relevant for this discussion but there is also a ton of compiling Kaehler)

[Kevin Buzzard]

Oh wow it is exactly the two red files in the screenshot which start timing out all over the place in that PR. It would be really good to get to the bottom of this.

[Matthew Ballard]

Rebuilding it now

[Riccardo Brasca]

@Andrew Yang is what you did for flt-regular maybe relevant for this file?

[Matthew Ballard]

Is there a link to the commit(s)?

[Matthew Ballard]

Link

[Andrew Yang]

I just added instances like these
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/slowness.20in.20ring.20theory.20file/near/378638708
I think this is already tried on this file before?

[Matthew Ballard]

Yeah, and then lean4#2478 fights that change

[Matthew Ballard]

Bench

[Scott Morrison]

At this point does it makes sense to just discard RingTheory.Kaehler and rewrite it from scratch?

[Eric Wieser]

I don't know if that would help much

[Eric Wieser]

I regularly run into timeouts when working with tensor products

[Matthew Ballard]

This seems to be the worst of the bad performers from #7257

[Matthew Ballard]

I was hoping for more unambiguously bad. I have no sense atm what differentiates the green from the red

[Kevin Buzzard]

Does making tensor products irreducible help with tensor product timeouts? I have a PR which does this but it correctly has conflicts and I've been traveling all day yesterday and today so I didn't fix it up yet.

I think the problem with this file might be that there are some defeq non-diamonds regarding actions which take a long time to be proved defeq.

That failure to synthesize Smul R R (for R some complicated commuting) is pretty weird though

[Eric Wieser]

It's really rather handy to have the fact that lift f (x \otimes y) = f x y be true by definition on the tensor product, which I think any attempt at irreducibility would lose

[Eric Wieser]

Eric Wieser said:

I regularly run into timeouts when working with tensor products

#7394 is my current example of this, where building the definitions is impossible due to every edit taking multiple minutes to apply

[Johan Commelin]

Eric Wieser said:

It's really rather handy to have the fact that lift f (x \otimes y) = f x y be true by definition on the tensor product, which I think any attempt at irreducibility would lose

But should this really be a defeq? Do you get into DTT hell without it? Or is it just convenient, but could simp also take care of it?

[Kevin Buzzard]

I think this is not the only problem...

[Sebastien Gouezel]

I would be really happy to drop defeq if it leads to performance improvements. After all, this defeq is an implementation detail, and a simp lemma would be just as good.