Measure compute time

Stream: lean4

[pcpthm]

How to measure the time of pure computation? I can use IO.monoMsNow to get the current time but I need to ensure the computation is done between two calls to the IO.monoMsNow function.

The best I come up with is a "black box" API (α → IO α), like so:

@[noinline] opaque blackBox : α → IO α := pure

def compute : Nat → Nat := sorry -- expensive computation

def func (input : Nat) : IO Nat := do
  let startTime ← IO.monoMsNow
  let input ← blackBox input
  let output ← blackBox $ compute input
  let endTime ← IO.monoMsNow
  println! "time: {endTime - startTime}"
  return output

But it relies on the behavior that blackBox is not inlined.

Maybe it doesn't much make sense if α is a singleton type.

[Henrik Böving]

You want docs4#timeit, if it's a pure computation you can just Function.comp pure yourFunction

[pcpthm]

Unfortunately, timeit doesn't work:

def computeFib (n : Nat) : Nat := Id.run do
  let mut (a, b) := (0, 1)
  for _ in [1:n] do
    (a, b) := ((a + b) % 10000, a)
  return a

def main : IO Unit := do
  let input := (← (← IO.getStdin).getLine).trim.toNat!
  let output ← timeit "time" do
    return computeFib input
  println! "{output}"

And input 100000000. The result is time 0.00021ms even though it is actually taking 1s.

I guess this is because computeFib input can be computed before timeit starts.
Thus, to make computation happen inside the timeit block, I need to get input inside the timeit block. However, that means the time it takes to input (waiting for user input) will be counted for the time.

Also, I want to more flexible output than the fixed timeout output.

[Sebastian Ullrich]

pcpthm said:

But it relies on the behavior that blackBox is not inlined.

What's the problem with that? It's not really different from https://doc.rust-lang.org/std/hint/fn.black_box.html

[pcpthm]

A concern was even if Lean doesn't inline a function, an C compiler will inline the function later. But thinking about that, the C compiler is usually not reordering statements, so it is okay I guess.

I guess, in the end, because computation time is not something semantic, probably there is no way to truly ensure something like this.

[pcpthm]

Like, even if blackBox was truly opaque, a hypothetical transformation of code:

do blackBox (compute (<- blackBox input))

to

let precomputedFor0 := compute 0
do match <- blackBox input with
  | 0 => blackBox precomputedFor0
  | input => blackBox (compute input)

is valid and the computation time will be bogus.