Unaccounted for time when profiling a tactic

Stream: lean4

[Alex Keizer]

I'm trying to profile a slow tactic, but having some trouble deciphering the information from the profiler. Specifically, when I measure the time taken for the theorem as a whole, I get that it takes about 7.5 seconds. But, when I measure the time taken by the tactic elaborator itself, I measure only 3.5 seconds. At first, I figured this difference must be kernel checking or linters (we generate rather large proofs, so this made some sense to me). However, I then tried to disable those via options (debug.skipKernelTC and various options under linter), and saw basically no difference.

Are there any other things done by the theorem elaborator after a tactic is finished that can account for the missing runtime?

Here's the output of the trace profiler:

[Elab.command] [7.406624] theorem sha512_225_instructions : SHA512Bench 225 := fun s0 _ h =>
      by
      intros
      sym_n 225
      all_goals sorry ▼
  [step] [3.263754]
      intros
      sym_n 225
      all_goals sorry ▶
  [def.maxSharing] [0.052831] share common exprs
  [def.processPreDef] [0.021418] process pre-definitions

Notice the ~3 seconds or so unaccounted for in the trace.

And for completeness, here's the full theorem with all the options I set:

set_option debug.skipKernelTC true
set_option linter.constructorNameAsVariable false
set_option linter.deprecated false
set_option linter.missingDocs false
set_option linter.omit false
set_option linter.suspiciousUnexpanderPatterns false
set_option linter.unnecessarySimpa false
set_option linter.unusedRCasesPattern false
set_option linter.unusedSectionVars false
set_option linter.unusedVariables false
set_option profiler true
set_option trace.profiler true
theorem sha512_225_instructions : SHA512Bench 225 := fun s0 _ h => by
  intros
  sym_n 225
  all_goals sorry

[Henrik Böving]

These "time leaks" are pretty annoying to find in general, they usually require doing some actual profiling with a C profiler and then adding a withTraceNode to the part of the compiler that is actually at fault here.

[Sebastian Ullrich]

The kernel and linters however are definitely logged when above the threshold

[Alex Keizer]

After a long and painful process of putting trace nodes everywhere, I've found the culprit: metavariable instantiation.

Rather confusingly, there is an instantiateMVarsProfiling in MutualDef, defined as

def instantiateMVarsProfiling (e : Expr) : MetaM Expr := do
  profileitM Exception s!"instantiate metavars" (← getOptions) do
    instantiateMVars e

I kind of assumed the profiling here referred to the profiler whose traces I was looking at it, so I didn't put a trace class here at first. That was a mistake, somehow the profileIt def does not seem to actually cause it to be part of the profile

[Alex Keizer]

Here's a PR that adds the relevant trace node: https://github.com/leanprover/lean4/pull/5501

[Henrik Böving]

There is two profilers right now set_option profiler true which you can also access from the command line and notably C++ can also use which is controlled by profileitM and set_option trace.profiler which withTraceNode uses.