Kaehler differential variable weirdness

Stream: mathlib4

[Kevin Buzzard]

Anne pointed out here that it's really easy to see the slowest files in mathlib nowadays. I had not ever internalised this before. They go on to point out that the slowest file in mathlib right now is Mathlib.RingTheory.Kaehler and because I'm on a long train journey I thought I'd take a look. Everything is sluggish. It seemed hard to point a finger at anything specific because traces just indicated that everything was a bit slow.

In this file, the Kaehler differentials KaehlerDifferential R S (with S an R-algebra) are defined at the top, with notation Ω[S⁄R]. One of the first things to happen is the totally innocuous instance

instance : Nonempty (Ω[S⁄R]) := ⟨0⟩

Profiling this line indicates that it takes 0.2 seconds! That feels to me like a big reason this file is slow -- if you can't even make 0 in less than 0.2 seconds, what are the chances that you can prove a theorem in graduate level commutative algebra in less than 5 seconds?

So I looked at the trace, and it's the usual stuff, everything's a bit slow but nothing's horrible. For example nearly half of the 0.2 seconds is taken up by this:

    [step] [0.013582] expected type: Type (max u_1 u), term
        Module R M ▶
    [step] [0.012432] expected type: Type (max u_1 v), term
        Module S M ▶
    [step] [0.061313] expected type: Prop, term
        IsScalarTower R S M ▶

and...hey, wait a minute? What is M?

M is nothing. M is a variable introduced earlier on, to do something else. It has nothing to do with what is happening right now.

Whatever is it doing in the trace?

[Sébastien Gouëzel]

If M is not around (say because you add a section above), then the instance synthesis is 10 times faster...

[Sébastien Gouëzel]

We really need lean#2452.

[Kevin Buzzard]

Yes. But why is it faster?

set_option trace.profiler true in
set_option trace.Meta.synthInstance true in
instance : Nonempty (Ω[S⁄R]) := ⟨0⟩

#exit

gives me a (partially unfolded) trace of

[Elab.command] [0.233924] set_option trace.Meta.synthInstance true in
    instance : Nonempty (Ω[S⁄R]) :=
      ⟨0⟩ ▼
  [] [0.233810] instance : Nonempty (Ω[S⁄R]) :=
        ⟨0⟩ ▼
    [Meta.synthInstance] ✅ CommSemiring R ▶
    [Meta.synthInstance] ✅ Semiring S ▶
    [step] [0.015477] expected type: Type (max u_1 u), term
        Module R M ▶
    [step] [0.014480] expected type: Type (max u_1 v), term
        Module S M ▶
    [step] [0.069023] expected type: Prop, term
        IsScalarTower R S M ▶
    [Meta.synthInstance] ✅ CommRing R ▶
    [Meta.synthInstance] ✅ CommRing S ▶
    [Meta.synthInstance] ✅ Algebra R S ▶
    [step] [0.013912] expected type: Nonempty (Ω[S⁄R]), term
        ⟨0⟩ ▶

What does [step] mean, and why are we taking the step towards Module R M? I've unfolded the traces above this (the proofs that R is a CommSemiring and S is a Semiring) and I can't see any mention of M.

[Sébastien Gouëzel]

This is crazy. It doesn't have anything to do with the statement to be proven:

def foo : ℕ := 0

(at the same place in this file) shows the same steps, and takes 0.15s on my computer.

[Kevin Buzzard]

Lol no wonder the file is slow :-)

Confirmed at my end:

[Elab.command] [0.129403] def foo : ℕ :=
      0 ▼
  [step] [0.010888] expected type: Type (max v u), term
      Algebra R S
  [step] [0.023373] expected type: Type (max u_1 u), term
      Module R M ▶
  [step] [0.014868] expected type: Type (max u_1 v), term
      Module S M ▶
  [step] [0.071719] expected type: Prop, term
      IsScalarTower R S M ▶

ha ha ha, something is really wrong here :-)

[Sébastien Gouëzel]

More minimal example:

import Mathlib.Algebra.Algebra.Defs

variable (R S M : Type) [CommRing R] [CommRing S] [Algebra R S]
  [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]

set_option trace.profiler true
set_option trace.Meta.synthInstance true
def foo : ℕ := 0

takes 0.14s to elaborate, and the steps mention R, S and M.

[Sébastien Gouëzel]

Better example:

import Mathlib.Algebra.Algebra.Defs

variable (R S M : Type) [CommRing R] [CommRing S]
  [Algebra R S] -- comment this line to remove the crazy steps in `foo`.

set_option trace.profiler true
set_option trace.Meta.synthInstance true
def foo : ℕ := 0

where the steps in the definition of foo mention Algebra R S. My understanding is the following: when you define foo, then the variables are around, and might be used in the definition, so Lean has to make sense of these variables even before starting to process your definition (because it might involve these variables). So it has to understand what Algebra R S means, which means finding some typeclasses on R and S.

[Andrew Yang]

I wonder if you have found any other culprit? There are lots of files with these variables lying around but only this particular file is exceptionally painful to deal with, so I guess this is not the root cause? My vague feeling is that quotients of complex structures are costly but I don't have a good reason/example.

[Michael Stoll]

Maybe something like this explains why the search for Module instances is so high up in the list (see here)?

[Kevin Buzzard]

I agree that this is unlikely to be the main problem in this file.

[Kim Morrison]

I've made a Mathlib free minimization of this at lean#4253.

[Patrick Massot]

Kim do you think that investigating this is really worth the trouble instead of working on the crucial lean4#2452 that will probably at least change the issue completely (and hopefully fix it)?

[Kim Morrison]

I'm not sure. As noted on lean4#2452, we weren't ready to start work on that yet. Perhaps this example changes that? Or perhaps someone will think of an intermediate fix.

[Patrick Massot]

I’m sure that seeing beginners next week will give you one more reason to want lean4#2452 fixed :wink: