slow rw

Stream: general

[Kevin Buzzard]

(deleted: cannot reproduce; turns out I had a bunch of std uncompiled)

[Kevin Buzzard]

So I have spent some time today looking at RingTheory.Kaehler, a poster child for maxHeartbeats and synthInstance.maxHeartbeats bumps. The first time they need bumping is in part because of this rewrite, which takes two seconds for me on a fast machine and 3 or 4 on my laptop. Here's the experiment I did (and which you can do too). Start with a fresh master.

1) I copied this file to Mathlib.RingTheory.Kaehler2. It's just the first 200 or so lines of Mathlib.RingTheory.Kaehler but with trace.profile true at the relevant time (the rewrite which takes 2+ seconds).

2) I ran lake build Mathlib.RingTheory.Kaehler2 > trace.txt (this takes a minute or two and makes a 31 meg file with over 200000 lines).

3) I opened the trace file in a text editor and searched for nsmul =?= AddMonoid.mk. This is the middle line in what looks like a syntactically equal check. In full the check looks like this:

[Meta.isDefEq] [0.012934s] ✅
AddMonoid.mk
  (_ : ∀ (a : S ⊗[R] S →ₗ[R] S ⊗[R] S), 0 + a = a)
  (_ : ∀ (a : S ⊗[R] S →ₗ[R] S ⊗[R] S), a + 0 = a)
  AddMonoid.nsmul =?= AddMonoid.mk
  (_ : ∀ (a : S ⊗[R] S →ₗ[R] S ⊗[R] S), 0 + a = a)
  (_ : ∀ (a : S ⊗[R] S →ₗ[R] S ⊗[R] S), a + 0 = a)
  AddMonoid.nsmul

There are 134 of these, spread evenly through the trace, one occurring about every 1800 lines. Each of these 134 problems takes about 12ms to be solved, and these 1.6 seconds make up the majority of the time spent on the rewrite.

(If you also set trace.Meta.isDefEq true you can see the gigantic trace of apparently syntactically equal stuff which is spewed out every time this goal needs to be solved.)

Each of the 134 goals is a "blocker" for progression in the sense that if you look at the trace you will see that after solving this goal, trace indentation always jumps back 50 or more spaces. The next goal is always one of the following:

[Meta.isDefEq] [0.041673s] ✅ Semiring.toModule =?= Semiring.toModule

[Meta.isDefEq] [0.020788s] ✅ Semiring.toNonUnitalSemiring =?= NonUnitalSemiring.mk
      (_ :
        ∀ (x y z : S ⊗[R] S),
          ↑(↑Algebra.TensorProduct.mul (↑(↑Algebra.TensorProduct.mul x) y))
              z =
            ↑(↑Algebra.TensorProduct.mul x)
              (↑(↑Algebra.TensorProduct.mul y) z))

[Meta.isDefEq] [0.041805s] ✅ CommSemiring.toSemiring =?= Algebra.TensorProduct.instSemiringTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule

[Meta.synthInstance] [0.359371s] ✅ SMul S { x // x ∈ KaehlerDifferential.ideal R S }

[Meta.isDefEq] [0.201068s] ✅ SetLike.instMembership =?= SetLike.instMembership

And then for pretty much all of these goals, they take 1900 lines of trace to solve, along the way expanding out to subgoals which are 30 lines long and then collapsing again to subgoals which are one line long, and each time ending up with 0.012 seconds solving AddMonoid.mk _ _ AddMonoid.nsmul =?= AddMonoid.mk _ _ AddMonoid.nsmul.

I'm not entirely sure what any of this means. Right now I have three questions and one in progress task.

The questions are:

(1) Is 12ms a reasonable amount of time for solving AddMonoid.mk _ _ AddMonoid.nsmul =?= AddMonoid.mk _ _ AddMonoid.nsmul ? Or is this not a reasonable question because I am not asking it with pp.all true so we can't even see what the question is?

(2) How do I access the trace with pp.all true on, so I can see more about what that question is which is taking 12ms? I've tried switching it on in the code but it just crashes VS Code and brings my computer to its knees if I run it on the command line.

(3) The trace would be a bit smaller if I knew the option which will change (_ : ∀ (a : S ⊗[R] S →ₗ[R] S ⊗[R] S), 0 + a = a) to just _. Is there such an option? I'm sure I've asked this before.

The in progress task is that I'm trying to make this example mathlib-free and it's quite an effort. I probably won't get this done tonight. Current progress is here; this is a repo which has a skeleton for CommRing which I will hopefully be able to use at some point.

[Eric Wieser]

This is the middle line in what looks like a syntactically equal check. In full the check looks like this:

Can we somehow make set_option pp.proofs.withTypes false the default for when tracing instance info?

[Eric Wieser]

Or is this not a reasonable question because I am not asking it with pp.all true so we can't even see what the question is?

Yes, this is unfortunately not a reasonable question without knowing the implicit constructor arguments

[Eric Wieser]

This is pretty suspicious:

[Meta.isDefEq] [0.020788s] ✅ Semiring.toNonUnitalSemiring =?= NonUnitalSemiring.mk
      (_ :
        ∀ (x y z : S ⊗[R] S),
          ↑(↑Algebra.TensorProduct.mul (↑(↑Algebra.TensorProduct.mul x) y))
              z =
            ↑(↑Algebra.TensorProduct.mul x)
              (↑(↑Algebra.TensorProduct.mul y) z))

Those proofs don't have the right type: they should be about * not Algebra.TensorProduct.mul

[Eric Wieser]

I'm sure they're defeq, but doe isDefeq know to ignore them completely now?

[Kevin Buzzard]

Eric Wieser said:

This is the middle line in what looks like a syntactically equal check. In full the check looks like this:

Can we somehow make set_option pp.proofs.withTypes false the default for when tracing instance info?

Thanks. It's actually pp.proofs.withType.

This is pretty suspicious:

There are 72 instances of Semiring.toNonUnitalSemiring =?= NonUnitalSemiring.mk in my minimised trace, each taking 15ms to be solved.

[Riccardo Brasca]

I just kicked !3#19234 on the queue. I don't think it will make a huge difference (when ported to mathlib4), but who knows...

[Eric Wieser]

Thanks! I think it made little difference on master, but it helped in another forward-port (edit: #6094)

[Kevin Buzzard]

Thanks! I'm still in the process of trying to understand why this file is slow, but tidying it up always helps.

[Eric Wieser]

Does adding shortcut instances help speed it up at all? Something like this just before KaehlerDifferential.endEquivDerivation'

set_option synthInstance.maxHeartbeats 1500000 in
set_option maxHeartbeats 4400000 in
instance : Module R (KaehlerDifferential.ideal R S).cotangentIdeal := Submodule.module' _
set_option synthInstance.maxHeartbeats 1500000 in
set_option maxHeartbeats 4400000 in
instance : Module S (KaehlerDifferential.ideal R S).cotangentIdeal := Submodule.module' _

set_option synthInstance.maxHeartbeats 1500000 in
set_option maxHeartbeats 4400000 in
instance : SMulCommClass R S (KaehlerDifferential.ideal R S).cotangentIdeal := IsScalarTower.to_smulCommClass

instance : Module R (Derivation R S (KaehlerDifferential.ideal R S).cotangentIdeal) :=
  Derivation.instModule