slow typechecking

Stream: lean4

[Kevin Buzzard]

With set_option trace.profiler true in some declaration which depends heavily on mathlib, the proofs seem to be relatively quick but at the end I get

  [Kernel] [1.163096] typechecking declaration
  [Kernel] [2.462965] typechecking declaration
  [Kernel] [10.721389] typechecking declaration
  [Kernel] [27.633739] typechecking declaration
  [Kernel] [1.370556] typechecking declaration

Is there a way for me to turn on other trace options so I can see what's going on?

[Kim Morrison]

Unfortunately there's not much you can do to get timing information inside the kernel, unless you're willing to use external profiling tools, but even then you have very little visibility into what is happening in the kernel.

[Floris van Doorn]

The kernel being slow probably means that you're having a "heavy rfl" in your proof.I recommend sorrying parts of the proof to see what tactic is causing the slowness.

[Kevin Buzzard]

Oh I know that, it's aesop_cat :-)

[Joël Riou]

In the situation that I believe Kevin is referring to here, introducing an auxiliary definition (for one of the fields of the structure that was defined) has basically solved the issue.

[Kevin Buzzard]

So just to get this straight, it's possible that in the middle of a tactic proof I can call rfl to close a subgoal, and this can succeed quickly (ie it's heavy but we didn't notice yet), and then when I close the main goal it can take a very long time to process the declaration? Or is it more subtle than this?

[Kevin Buzzard]

I have seen rfl take ages in category theory when simp is immediate, but I had always understood that it was the tactic running which took a long time, not that the tactic succeeded quickly and then the kernel struggled later on.

[Eric Wieser]

I would guess this happens because rfl in the elaborator respects / can be guided by reducibility, but the concept of reducibility is absent in the kernel?

[Mario Carneiro]

There is a new debug option coming to the next version of lean which lets you skip kernel checking, which can be used to diagnose whether it is the kernel or elaborator taking the time

[Sebastian Ullrich]

trace.profiler, which Kevin is using, already gives you that. The issue is that there are no traces inside the kernel to tell you more.