Slow coercions

Stream: mathlib4

[Oliver Nash]

I just opened a PR !4#5263 which golfs a proof using tauto. This golf was possible in Lean 3 but was unacceptably slow but happily in Lean 4 it is nice and fast.

However while making this change, I noticed that the rest of the proof takes maybe twice as a long in Lean 4 as in Lean 3. I had a quick look using the profiler and I see that most of the slowness in Lean 4 is due to repeated typeclass searches for CoeT. To be precise I see 20 instances of:

typeclass inference of CoeT took 384ms
typeclass inference of CoeT took 368ms
typeclass inference of CoeT took 328ms
typeclass inference of CoeT took 306ms
typeclass inference of CoeT took 307ms
typeclass inference of CoeT took 309ms
typeclass inference of CoeT took 307ms
typeclass inference of CoeT took 308ms
typeclass inference of CoeT took 335ms
typeclass inference of CoeT took 307ms
typeclass inference of CoeT took 307ms
typeclass inference of CoeT took 309ms
typeclass inference of CoeT took 307ms
typeclass inference of CoeT took 308ms
typeclass inference of CoeT took 306ms
typeclass inference of CoeT took 306ms
typeclass inference of CoeT took 312ms
typeclass inference of CoeT took 324ms
typeclass inference of CoeT took 319ms
typeclass inference of CoeT took 312ms

(adding up to nearly 6.5 seconds).

[Oliver Nash]

I would be grateful for help answering:

1. Is this a known regression in Mathlib 4?
2. How can I debug this further?

[Floris van Doorn]

Use set_option trace.Meta.synthInstance true to figure out what thing it's trying to coerce

[Oliver Nash]

Thanks, I'll try that now!

[Oliver Nash]

Floris van Doorn said:

Use set_option trace.Meta.synthInstance true to figure out what thing it's trying to coerce

Using this I learned that Lean was (repeatedly) taking about 500ms to find a way to coerce from docs4#Nat.Primes to docs4#Real so I added a commit which does:

--  set u : Nat.Primes → 𝕊 := fun p => ↑((↑(1 : ℕ) : ℝ) / p * T)
+  set u : Nat.Primes → 𝕊 := fun p => ↑((↑(1 : ℕ) : ℝ) / ((p : ℕ) : ℝ) * T)

This makes most of the slow CoeT searches disappear, and knocks about 5s off the proof which is great.

[Oliver Nash]

I'm still disappointed that:

1. This explicit coercion is now necessary when it was not in Lean 3, but more importantly,
2. Apparently any edit anywhere inside this ~100 line proof triggers the whole proof to recompile resulting in a near-impossible workflow: the Lean 3 proof suffered much less from this phenomenon.

Any further advice most gratefully received.

[Ruben Van de Velde]

stop can help with 2 (but maybe the proof should be split)

[Oliver Nash]

I admit many a 100-line proof should be split but I contend that this proof should not need splitting and that we should demand our tools can handle something like this.

Something to think about once the port is finished I guess.

[Eric Wieser]

Does save also help here?

[Oliver Nash]

Eric Wieser said:

Does save also help here?

It seems neither save nor stop helps.

[Oliver Nash]

Btw save is familar but stop is new: are the synonyms? Oh I see not.