performance debug

Stream: mathlib4

[Patrick Massot]

I'd like to get help to debug huge performance issues with !4#3383. Each declaration compiles piecewise but some don't compile globally. For instance in

irreducible_def lift {r : R → R → Prop} :
  { f : R →+* T // ∀ ⦃x y⦄, r x y → f x = f y } ≃ (RingQuot r →+* T) :=
  { toFun := fun f' =>
      let f := (f' : R →+* T)
      { toFun := fun x =>
          Quot.lift f
            (by
              rintro _ _ r
              induction r
              case of _ _ r => exact f'.prop r
              case add_left _ _ _ _ r' => rw [map_add, map_add, r']
              case mul_left _ _ _ _ r' => rw [map_mul, map_mul, r']
              case mul_right _ _ _ _ r' => rw [map_mul, map_mul, r'] )
            x.toQuot
        map_zero' := sorry/- by simp only [← zero_quot, f.map_zero] -/
        map_add' := sorry/- by
          rintro ⟨⟨x⟩⟩ ⟨⟨y⟩⟩
          simp only [add_quot, f.map_add x y] -/
        map_one' := sorry/- by simp only [← one_quot, f.map_one] -/
        map_mul' := sorry/- by
          rintro ⟨⟨x⟩⟩ ⟨⟨y⟩⟩
          simp only [mul_quot, f.map_mul x y] -/ }
    invFun := fun F =>
      ⟨F.comp (mkRingHom r), fun x y h => sorry/- by
        dsimp
        rw [mkRingHom_rel h] -/⟩
    left_inv := fun f => sorry/- by
      ext
      simp [mkRingHom_def] -/
    right_inv := fun F => sorry /- by
      ext
      simp [mkRingHom_def] -/ }

Each sorry replaces a proof that actually works. You can un-comment each one separately and it works. But uncommenting all of them at once will make Lean hang forever. A similar problem higher up in the file actually led to timeout and I got it to compile with set_option maxHeartbeats 800000 in, but in the above case I don't even get a timeout, it simply runs forever, consuming all CPU power it can find. More generally editing this file doesn't feel like interactive theorem proving at all, more like "type a line and go make some coffee while Lean thinks about it". I'd be happy to see someone fixing that but I'd be even more interesting in learning how to debug such a disaster.

[Sebastian Ullrich]

For the case that terminates, it would be interesting to see where time is spent using profiler true. When it doesn't terminate, the best approximation to that is running everything under gdb and looking at a few stack traces, which, yes, is a significantly worse user experience

[Patrick Massot]

Sorry about disappearing. Lean 4 killed my computer and I had to reboot to regain control.

[Patrick Massot]

set_option profiler true says

type checking took 377ms
type checking took 929ms
type checking took 971ms
type checking took 1.08s
type checking took 2.4s
compilation new took 104ms
compilation of RingQuot.instSemiring took 19.2s

[Patrick Massot]

Should I say something more to get more info?

[Scott Morrison]

Does forcing it to be noncomputable help?

[Patrick Massot]

I just tried after seeing that suspicious looking compilation thing and it does help!

[Patrick Massot]

or maybe not

[Patrick Massot]

It stops printing compilation of RingQuot.instSemiring took 19.2s but it still takes forever.

[Matthew Ballard]

Tracing isDefEq and/or synthInstance will report timings for each step with profiler

[Patrick Massot]

The actual time with noncomputable is still around 20s.

[Sebastian Ullrich]

That sounds weird, it should at least get faster by that amount if the line disappears. If the expensive definition dominates file processing time (up to that point with #exit after it), you can also run it on the cmdline with lean --profile to print a grand total.

[Patrick Massot]

Tracing isDefEq and synthInstance doesn't show anything striking to me.

[Patrick Massot]

Sebastian, could you tell what I should run on the command line exactly?

[Sebastian Ullrich]

lake env lean --profile <file.lean>

[Patrick Massot]

Thanks. Without noncomputable:

lake env lean --profile Mathlib/Algebra/RingQuot.lean
interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.251._spec_1 took 102ms
import took 313ms
type checking took 375ms
type checking took 930ms
type checking took 963ms
type checking took 1.07s
type checking took 2.38s
compilation new took 105ms
compilation of RingQuot.instSemiring took 19.2s
elaboration took 11.2s
Mathlib/Algebra/RingQuot.lean:327:0: warning: using 'exit' to interrupt Lean
cumulative profiling times:
    attribute application 1.87ms
    compilation 19.3s
    compilation new 138ms
    dsimp 0.456ms
    elaboration 11.3s
    import 313ms
    initialization 39ms
    interpretation 805ms
    linting 56.2ms
    parsing 14.3ms
    simp 135ms
    tactic execution 110ms
    type checking 5.87s
    typeclass inference 581ms

[Patrick Massot]

with noncomputable:

lake env lean --profile Mathlib/Algebra/RingQuot.lean
interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.251._spec_1 took 102ms
import took 467ms
type checking took 375ms
type checking took 923ms
type checking took 960ms
type checking took 1.07s
type checking took 2.39s
elaboration took 10.9s
Mathlib/Algebra/RingQuot.lean:327:0: warning: using 'exit' to interrupt Lean
cumulative profiling times:
    attribute application 1.86ms
    compilation 46.1ms
    compilation new 33.1ms
    dsimp 0.456ms
    elaboration 11s
    import 467ms
    initialization 30.8ms
    interpretation 798ms
    linting 56.3ms
    parsing 14.7ms
    simp 136ms
    tactic execution 112ms
    type checking 5.87s
    typeclass inference 589ms

[Sebastian Ullrich]

That's still not very fast, but does the second version at least feel faster? (You can also prepend time to the cmdline to make that more precise)

[Patrick Massot]

time says:

real    0m38,883s
user    0m38,023s
sys 0m0,860s

vs

real    0m19,635s
user    0m19,280s
sys 0m0,356s

[Patrick Massot]

So the second version is indeed faster.

[Patrick Massot]

But both are horrible.

[Scott Morrison]

Without noncomputable:

% time lake env lean --profile Mathlib/Algebra/RingQuot.lean
interpretation of Std.Linter.UnreachableTactic.initFn._@.Std.Linter.UnreachableTactic._hyg.1411 took 108ms
interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.251._spec_1 took 133ms
import took 650ms
type checking took 580ms
type checking took 1.43s
type checking took 1.46s
type checking took 1.61s
type checking took 3.35s
compilation new took 135ms
compilation of RingQuot.instSemiring took 25.8s
elaboration took 17.1s
Mathlib/Algebra/RingQuot.lean:330:0: warning: using 'exit' to interrupt Lean
cumulative profiling times:
        attribute application 2.78ms
        compilation 25.8s
        compilation new 181ms
        dsimp 0.531ms
        elaboration 17.3s
        import 650ms
        initialization 30ms
        interpretation 1.58s
        linting 71.7ms
        parsing 18.1ms
        simp 187ms
        tactic execution 159ms
        type checking 8.66s
        typeclass inference 771ms
lake env lean --profile Mathlib/Algebra/RingQuot.lean  54.57s user 1.67s system 99% cpu 56.271 total

with noncomputable

% time lake env lean --profile Mathlib/Algebra/RingQuot.lean
interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.251._spec_1 took 133ms
import took 665ms
type checking took 584ms
type checking took 1.41s
type checking took 1.47s
type checking took 1.65s
type checking took 3.41s
elaboration took 17.3s
Mathlib/Algebra/RingQuot.lean:330:0: warning: using 'exit' to interrupt Lean
cumulative profiling times:
        attribute application 2.82ms
        compilation 68.2ms
        compilation new 46.7ms
        dsimp 0.562ms
        elaboration 17.5s
        import 665ms
        initialization 29.9ms
        interpretation 1.56s
        linting 71.8ms
        parsing 18.6ms
        simp 187ms
        tactic execution 158ms
        type checking 8.75s
        typeclass inference 779ms
lake env lean --profile Mathlib/Algebra/RingQuot.lean  29.55s user 1.04s system 99% cpu 30.610 total

[Sebastian Ullrich]

The high type checking (kernel) time is curious, we don't see that very often. Could it be that the produced (proof) term is simply humongous?

[Matthew Ballard]

Which declarations are chewing up the processor in particular? Just lift?

[Scott Morrison]

The relevant declaration is

instance instSemiring (r : R → R → Prop) : Semiring (RingQuot r) where
  add := (· + ·)
  mul := (· * ·)
  zero := 0
  one := 1
  natCast := natCast r
  natCast_zero := by simp [Nat.cast, natCast_def, ← zero_quot]
  natCast_succ := by simp [Nat.cast, natCast_def, ← one_quot, add_quot]
  add_assoc := by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [add_quot, add_assoc]
  zero_add := by
    rintro ⟨⟨⟩⟩
    simp [add_quot, ← zero_quot, zero_add]
  add_zero := by
    rintro ⟨⟨⟩⟩
    simp only [add_quot, ← zero_quot, add_zero]
  zero_mul := by
    rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← zero_quot, zero_mul]
  mul_zero := by
    rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← zero_quot, mul_zero]
  add_comm := by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [add_quot, add_comm]
  mul_assoc := by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [mul_quot, mul_assoc]
  one_mul := by
    rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← one_quot, one_mul]
  mul_one := by
    rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← one_quot, mul_one]
  left_distrib := by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [mul_quot, add_quot, left_distrib]
  right_distrib := by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [mul_quot, add_quot, right_distrib]
  npow n x := x ^ n
  npow_zero := by
    rintro ⟨⟨⟩⟩
    simp only [pow_quot, ← one_quot, pow_zero]
  npow_succ := by
    rintro n ⟨⟨⟩⟩
    simp only [pow_quot, mul_quot, pow_succ]
  nsmul := (· • ·)
  nsmul_zero := by
    rintro ⟨⟨⟩⟩
    simp only [smul_quot, zero_smul, zero_quot]
  nsmul_succ := by
    rintro n ⟨⟨⟩⟩
    simp only [smul_quot, nsmul_eq_mul, Nat.cast_add, Nat.cast_one, add_mul, one_mul,
               add_comm, add_quot]

which conspicuously has many structure fields, each with a tactic proof.

[Scott Morrison]

(This is the one Patrick and I are timing. lift is further down the file (past the #exit) and even slower.)

[Matthew Ballard]

Does bisecting the fields help narrow it down?

[Scott Morrison]

I remember long ago in lean3 some quadratic effect?

[Patrick Massot]

Matthew, lift doesn't compile at all. Currently we focus on one that does compile if you push MaxHearbeats enough.

[Scott Morrison]

Indeed, sorrying the second half of the proofs drops elaboration time to 2s.

[Matthew Ballard]

Is it snappy with just the data carrying fields?

[Scott Morrison]

Similarly, sorrying instead the first half of the proofs drops elaboration time to 0.4s.

[Scott Morrison]

So it is a non-local effect of the many proofs...

[Matthew Ballard]

Those proofs overlap quite a bit

[Scott Morrison]

overlap?

[Patrick Massot]

Yes, you can sorry any combination of half the proofs to get something fast.

[Matthew Ballard]

The elements of the lists in the calls to simp overlap.

[Matthew Ballard]

Hypothetically if *_quot is somewhat slow them doing them in succession is very slow

[Scott Morrison]

The proof terms generated are getting bigger as you go through the list of fields:

[Patrick Massot]

Maybe the proof terms somehow include the proof terms of the previous fields?

[Scott Morrison]

Yes.

[Matthew Ballard]

Would factoring some stuff out to separate declarations prevent this?

[Scott Morrison]

Proof of add_assoc (_proof_1) is 67kb, proof of zero_add (_proof_2) is 260kb, but if you comment out add_assoc then the proof of zero_add drops to 30kb.

[Scott Morrison]

(These are all with pp.all.)

[Scott Morrison]

@Matthew Ballard, presumably, but I think we want to treat this as a Lean bug for now. This is not good behaviour!

[Matthew Ballard]

What are the sizes in ML3?

[Scott Morrison]

Ah.. simple but terrible explanation. :-)

[Scott Morrison]

The HAdd instance that is being used in the proof of zero_add is:

(@HAdd.hAdd.{u_1, u_1, u_1} (@RingQuot.{u_1} R inst r) (@RingQuot.{u_1} R inst r) (@RingQuot.{u_1} R inst r)
      (@instHAdd.{u_1} (@RingQuot.{u_1} R inst r)
        (@AddSemigroup.toAdd.{u_1} (@RingQuot.{u_1} R inst r)
          (@AddSemigroup.mk.{u_1} (@RingQuot.{u_1} R inst r)
            (@Add.mk.{u_1} (@RingQuot.{u_1} R inst r) fun (x x_1 : @RingQuot.{u_1} R inst r) =>
              @HAdd.hAdd.{u_1, u_1, u_1} (@RingQuot.{u_1} R inst r) (@RingQuot.{u_1} R inst r)
                (@RingQuot.{u_1} R inst r)
                (@instHAdd.{u_1} (@RingQuot.{u_1} R inst r) (@RingQuot.instAddRingQuot.{u_1} R inst r)) x x_1) ...

i.e. it is being deduced from an AddSemigroup which contains the proof of add_assoc!

[Scott Morrison]

This then snowballs as we get to the later fields, and the instances being used recursively contain copies of the proofs from earlier steps (which contain instances which ...).

[Scott Morrison]

This is all with pp.all on, so the sizes I'm seeing are a bit unfair.

[Scott Morrison]

(Subexpression sharing, etc)

[Yaël Dillies]

Is that a general drawback of new structures, then?

[Scott Morrison]

@Sebastian Ullrich, does this make sense to you?

[Patrick Massot]

Thank you very much Scott for investigating this. This definitely reveals a bug either in Lean or in how mathlib uses Lean. There isn't much point in finding a workaround, we need a systematic fix.

[Mario Carneiro]

this is a known issue, I think

[Patrick Massot]

Is there a known fix then?

[Mario Carneiro]

It happens in ml3 as well, when you try to construct a deeply nested structure "in one go" without breaking out the parents into their own declarations

[Scott Morrison]

How slow was this in mathlib3? I don't remember.

[Mario Carneiro]

I would hope it doesn't get too bad, because of the abstraction of the _proof_i theorems

[Scott Morrison]

It seems they are not being abstracted properly here, however.

[Mario Carneiro]

it's possible that the way this abstraction is handled in lean 4 has changed in a way that is making the kernel see the full term

[Scott Morrison]

The actual proofs are showing up in the later proofs.

[Scott Morrison]

(That is, with pp.all.)

[Scott Morrison]

But I would have hoped that they are behind _proof_n.

[Mario Carneiro]

can this be MWE'd?

[Mario Carneiro]

Patrick Massot said:

Is there a known fix then?

there is a known workaround, which is as Matthew said: make a lemma

[Sebastian Ullrich]

I believe proofs are abstracted only after term elaboration

[Scott Morrison]

And that hasn't changed, I guess?

[Mario Carneiro]

I guess this is caused by a metavariable for the proof appearing in many places, somewhere in the structure instance elaborator

[Mario Carneiro]

even then it seems like it should be mostly okay since you get a dag-like term

[Mario Carneiro]

and after abstraction it shouldn't matter

[Mario Carneiro]

but shouldn't abstraction happen before it is sent to the kernel?

[Sebastian Ullrich]

You also mentioned another workaround above:
Mario Carneiro said:

breaking out the parents into their own declarations

This is a form of making the implicit term sharing explicit. Binding the suspected repeated metavariable with a let would be another explicit sharing solution, but that might not be trivial at all to achieve.

[Mario Carneiro]

I worry about let binders in instances making things weird in typeclass inference after unfolding

[Mario Carneiro]

not sure how much of an issue that is in reality

[Sebastian Ullrich]

Yes, it could definitely affect other things. But ideally it shouldn't be more problematic than splitting the code into multiple instances manually.

[Patrick Massot]

What is the Lean 4 syntax to say that missing fields should be taken from a previous named declaration?

[Mario Carneiro]

__ := should work

[Sebastian Ullrich]

I don't think identical proofs are abstracted into the same proof_N declaration, so abstracting after duplication doesn't help all that much

[Mario Carneiro]

oof

[Mario Carneiro]

way to break term sharing

[Sebastian Ullrich]

My bad, there is indeed a cache

[Patrick Massot]

I can confirm this "fixes" the issue. But it's really really unnatural and ugly here.

[Mario Carneiro]

really? Looking at that definition above I would say it cries out for being factored into smaller pieces

[Mario Carneiro]

it's a bunch of things dependent over a function which is itself a quotient lift with a big proof in it

[Patrick Massot]

I'm talking about the SemiRing instance.

[Mario Carneiro]

you don't have to break it into every single parent, just enough to solve the performance issues

[Mario Carneiro]

like the notation typeclasses I would probably skip

[Mario Carneiro]

but you could split a semiring instance into a AddMonoid instance, a Monoid instance, and a semiring instance

[Patrick Massot]

I went with

instance instAddCommMonoid (r : R → R → Prop) : AddCommMonoid (RingQuot r) where
  add := (· + ·)
  zero := 0
  add_assoc := by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [add_quot, add_assoc]
  zero_add := by
    rintro ⟨⟨⟩⟩
    simp [add_quot, ← zero_quot, zero_add]
  add_zero := by
    rintro ⟨⟨⟩⟩
    simp only [add_quot, ← zero_quot, add_zero]
  add_comm := by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [add_quot, add_comm]
  nsmul := (· • ·)
  nsmul_zero := by
    rintro ⟨⟨⟩⟩
    simp only [smul_quot, zero_smul, zero_quot]
  nsmul_succ := by
    rintro n ⟨⟨⟩⟩
    simp only [smul_quot, nsmul_eq_mul, Nat.cast_add, Nat.cast_one, add_mul, one_mul,
               add_comm, add_quot]

instance instMonoidWithZero (r : R → R → Prop) : MonoidWithZero (RingQuot r) where
  mul_assoc := by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [mul_quot, mul_assoc]
  one_mul := by
    rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← one_quot, one_mul]
  mul_one := by
    rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← one_quot, mul_one]
  zero_mul := by
    rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← zero_quot, zero_mul]
  mul_zero := by
    rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← zero_quot, mul_zero]
  npow n x := x ^ n
  npow_zero := by
    rintro ⟨⟨⟩⟩
    simp only [pow_quot, ← one_quot, pow_zero]
  npow_succ := by
    rintro n ⟨⟨⟩⟩
    simp only [pow_quot, mul_quot, pow_succ]

instance instSemiring (r : R → R → Prop) : Semiring (RingQuot r) where
  natCast := natCast r
  natCast_zero := by simp [Nat.cast, natCast_def, ← zero_quot]
  natCast_succ := by simp [Nat.cast, natCast_def, ← one_quot, add_quot]
  left_distrib := by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [mul_quot, add_quot, left_distrib]
  right_distrib := by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [mul_quot, add_quot, right_distrib]
  nsmul := (· • ·)
  nsmul_zero := by
    rintro ⟨⟨⟩⟩
    simp only [smul_quot, zero_smul, zero_quot]
  nsmul_succ := by
    rintro n ⟨⟨⟩⟩
    simp only [smul_quot, nsmul_eq_mul, Nat.cast_add, Nat.cast_one, add_mul, one_mul,
               add_comm, add_quot]
  __ := instAddCommMonoid r
  __ := instMonoidWithZero r

[Patrick Massot]

Which roughly split in three equal pieces. But mathematically this is meaningless.

[Patrick Massot]

The reason it is meaningless is that R already has all the required typeclasses anyway.

[Mario Carneiro]

sure it is meaningful. You don't need to give the full proof of semiring at once

[Patrick Massot]

Since they are needed to talk about RingQuot r

[Mario Carneiro]

lemma 1 is that it's a monoid, lemma 2 is that it's also an add monoid, and lemma 3 is that the structures cohere

[Scott Morrison]

It does seem like it wouldn't be too hard to MWE this, which might be worth doing just to help document the issue, even if no mitigation is planned.

[Scott Morrison]

I think I'm with Mario that this is fine as library code, but with Patrick that this is a horrible footgun.

[Mario Carneiro]

oh absolutely

[Scott Morrison]

It certainly feels like you should just be able to do all the easy proofs one after the other, so it's easy to write something extremely non-performant.

[Scott Morrison]

I'd also like to know why we got away with this in ml3.

[Mario Carneiro]

flat structures might play a role, although you still get some of the same issues as long as you have multiple layers of hierarchy

[Patrick Massot]

Needless to see, none of these proof would appear in the real world. The most you can hope for is explicitly leaving them to readers.

[Mario Carneiro]

I think about why lean couldn't just do this definition splitting automatically, but then things get weird as far as what the proof state actually is while you are proving it

[Mario Carneiro]

because these dependent proofs are actually visible in the tactic state if you click around

[Mario Carneiro]

and if we make a definition then you might have to block on some part of the proof getting finished before you can even proceed to show errors on the dependent parts

[Mario Carneiro]

which IIRC is a thing that actually happened in lean 3 in some situations

[Floris van Doorn]

These humongous subgoals also cause/expose the performance problems that to_additive has in some files. In !4#3580 adding a single dsimp only in a proof speeds up to_additive 4x.