Timeout of `whnf` in linear map

Stream: mathlib4

[Nailin Guan]

When I was working on defining a linear map, a strange time out occur:
If I fill in toFun and map_add', things works fine.

let f2 : Ext (ModuleCat.of R (Shrink.{v} (R ⧸ Ideal.ofList rs'))) M n →ₗ[R]
      Ext (ModuleCat.of R (QuotSMulTop a (Shrink.{v} (R ⧸ Ideal.ofList rs')))) M (n + 1) := {
        toFun := S_exact.extClass.precomp M (add_comm 1 n)
        map_add' := by simp
        map_smul' := by simp }

However if use __ for the first two

let f2 : Ext (ModuleCat.of R (Shrink.{v} (R ⧸ Ideal.ofList rs'))) M n →ₗ[R]
      Ext (ModuleCat.of R (QuotSMulTop a (Shrink.{v} (R ⧸ Ideal.ofList rs')))) M (n + 1) := {
       __ := S_exact.extClass.precomp M (add_comm 1 n)
        map_smul' := by simp }

It get into timeout. Is this just being too complicated and push it over the edge or there are some other reasons?

[Kenny Lau]

have you tried increasing maxheartbeat?

[Nailin Guan]

I increased to 250000 it failed also, but 300000 works.

[Jovan Gerbscheid]

We can't diagnose your problem unless you provide a #mwe

[Nailin Guan]

Producing this mwe is hard as this piles on many existing works on different branches. Sorry

[Kenny Lau]

you can also try to see if extracting __ as a let statement (or have) inside the definition helps

[Kenny Lau]

and provide its type

[Kenny Lau]

wait you're in a let already, what

[Kenny Lau]

in that case put the let/have before f2

[Nailin Guan]

This time 300000 failed, 350000 passed. I think if it doesn't exceed too much I can leave it there until the preliminaries are ready, we are planning to get this into mathlib.

[Alex Meiburg]

There might be one 'shortcut' instance you can add that will accelerate it a lot.

[Jovan Gerbscheid]

If you want to diagnose the issue yourself, you can try different combinations of

set_option trace.profiler true
set_option trace.Meta.Tactic.simp true
set_option trace.Meta.Tactic.isDefEq true