LinearAlgebra.QuotientPi !4#2378

Stream: mathlib4

[Calvin Lee]

I got this all building, but it's very slow (requires bumping maxHeartbeats by 50%)
the issue appears to be rewrite of quotientPiLift_mk, but I can't figure out how to unify it faster (and set_option trace.Meta.whnf true isn't giving me anything)

[Calvin Lee]

another oddity is that simp only [Pi.single_eq_same] is unable to close a goal when repeat (rw [Pi.single_eq_same]) is. For some reason simp is not rewriting exhaustively.

[Jireh Loreaux]

Did you see the type ascriptions I added for mk and friends in LinearAlgebra.Quotient? They drastically sped up elaboration and in some cases prevented timeouts.

[Calvin Lee]

interesting, I see this now
I'll try adding some type hints, but there aren't that many Quotient.mks in the type of definitions in this file

[Jireh Loreaux]

It seems like adding those in a few places in this file helps, but not so much where you need it the most. The profiler said this declaration was spending all it's time in TC inference. And looking at the TC trace, it seems that it's ending up with bad goals like Semiring ?m1 or AddCommGroup ?m2 in various places, and this is even after I tried to add type ascriptions I thought might help in this declaration. To me it seems like TC inference is going on a wild goose chase and it eventually gets the goose and returns home, but it just spends forever doing it.

[Calvin Lee]

what flags are you using to debug this? e.g. figure out what stages it's taking the most time in and the TC trace

[Jireh Loreaux]

set_option profiler true and set_option trace.Meta.snythInstances true (the latter might not be quite right, just use autocomplete)

[Calvin Lee]

set_option profiler true seems to indicate a lot of time was also spent in a simp, i'll try to bring that down with simp onlys

[Calvin Lee]

I'm going to add "help wanted" to this PR.
I wanted to do it myself to practice (since it isn't very critical) but the timeouts are really hard to solve. I've some idea of what's going wrong, but I still can't speed instance search (I've tried manually adding instances and removing others from the search, and it hasn't helped more than a second).