issue !4#12228: slow typeclass synthesis: takes 19000 hea...

Stream: triage

[Random Issue Bot]

Today I chose issue 12228 for discussion!

slow typeclass synthesis: takes 19000 heartbeats in to fail in AddMonoidHomClass (ℂ →*₀ ℝ) ℂ ℝ
Created by @Kim Morrison (@semorrison) on 2024-04-18
Labels: slow-typeclass-synthesis

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

This looks to be fixed now (possibly by lean4#4092). If someone who knows what they're talking about sees this and is convinced this is no longer an issue, it can be closed. Certainly the error is gone:

import Mathlib

open Complex in
set_option synthInstance.maxHeartbeats 3000 in
example (z : ℂ) : normSq (-z) = normSq z := by simp

now works fine

[Kim Morrison]

Yes, we can close this. There are a bunch of slow-typeclass-synthesis issues, hopefully all gone now. If someone would be able to check these and close as appropriate that would be great!

[Johan Commelin]

Going through them now

[Johan Commelin]

#13528 adds a file with tests to guard against regressions.