Using `timeit` for the entire program

Stream: lean4

[František Silváši]

Should the time obtained as "lean-measured" by executing f x

  def main : IO Unit := do timeit "lean-measured: " (f x)

roughly correspond with the execution time of the program as measured by the OS?

I am in a scenario where I expect nothing much to be happening, timeit reporting ~10ms and the program taking about half a second to execute.

It's hard to make an MWE for this.

[Leonardo de Moura]

... roughly correspond with the execution time of the program as measured by the OS?

Correct.

I am in a scenario where I expect nothing much to be happening, timeit reporting ~10ms and the program taking about half a second to execute.

This issue is due to transformations applied by the Lean compiler. In the future, we will make sure these transformations are automatically disabled when compiling a timeit expression. In the meantime, you can avoid the problem by writing an auxiliary function with the following annotations.

set_option compiler.extract_closed false in
@[noinline] def aux : IO Unit :=
  f x

def main : IO Unit :=
  timeit "time: " aux

[František Silváši]

Thank you.

[Sebastian Ullrich]

Note that perf and similar profilers work quite well on compiled Lean programs without the need for annotations