Force a Lean evaluation

Stream: lean4

[Matej Penciak]

I was hoping to set up some very basic tools for benchmarking, but unfortunately my naiive attempt doesn't work (MWE)

def f : Nat → Nat := (37 ^ ·)

def main : IO Unit := do
  let before ← IO.monoNanosNow
  discard $ pure (f $ 2 ^ 20 - 17)
  let after ← IO.monoNanosNow
  IO.println (after - before)

It seems like the Lean compiler is smart enough to eliminate the un-used line discard $ pure (f $ 2^20 -17), and I'm not getting any sensible timing information (you can even try this with some insanely expensive computation)

I arrived at a kind of unsatisfying hack that works:

def main : IO Unit := do
  let mut times : Array Nat := .mkEmpty 20
  let mut answer := 0
  for i in [:20] do
    let before ← IO.monoNanosNow
    answer := (f (2^i - 17))
    let after ← IO.monoNanosNow
    times := times.push (after - before)
  IO.println times

Is there a way of using something like discard without Lean being too clever?

[Henrik Böving]

we have docs4#timeit

[Matej Penciak]

Looking at the type signature I'm not sure I understand how to use that it... Is there a way to get the timing out?

[Matej Penciak]

It also seems to suffer from the same issue about being optimized out if I use timeit <| discard ...

[James Gallicchio]

timeit prints the output to debug. I used basically your hack in the past:

def time (f : IO α) : IO (Nat × α) := do
  let pre ← IO.monoMsNow
  let ret ← f
  let post ← IO.monoMsNow
  pure (post-pre, ret)

which also just forces the result to not be optimized away