debugging slow simps

Stream: lean4

[James Gallicchio]

No MWE, but do people have tips for debugging very slow simp calls? I have a mutual block where set_option profile true reports this back:

tactic execution of Lean.Parser.Tactic.unfold took 388ms
simp took 160ms
simp took 866ms
simp took 1.68s
simp took 100ms
simp took 1.55s

and that's with half the proofs behind stop. Advice would be appreciated!!

[James Gallicchio]

(also, 388ms for a call to unfold seems a bit crazy to me, is that maybe the cost of the lazily generated equational lemmas or something?)

[Sebastian Ullrich]

Standard reply: have you tried trace.profiler? I actually don't remember if I've tested it on simp yet

[James Gallicchio]

Ah, definitely a bit more information, at least lets me figure out exactly which simp calls are so slow. But not much debug info beyond which simps are slow:

          [] [0.169936s] simp [reduce] ▼
            [Kernel] [0.010725s] typechecking declaration
            [Kernel] [0.010832s] typechecking declaration

[James Gallicchio]

Ah, set_option trace.Meta.Tactic.simp true lists all the simp lemmas which it's trying and failing to apply, which leads me to some probably bad simp lemmas I've marked simp

[James Gallicchio]

okay, I was a bit suspicious of this simp lemma to begin with:

@[simp] theorem Finset.app_mapEquiv_symm (...)
  : f' = f.1 → f' ((Finset.mapEquiv s f).symm x) = x.val := by ...

It seems simp is quite zealously applying this to every instance of application... Is that because the head of the LHS term is an application with a variable? I was hoping this would be indexed in such a way that it only triggers when Finset.mapEquiv is involved, but I don't know have any idea how the indexing algorithm works.