running time is 0ms...?

Stream: new members

[Asei Inoue]

import Lean

open Lean Elab Command Term Meta

elab "#time " stx:command : command => do
  let start_time ← IO.monoMsNow

  elabCommand stx

  let end_time ← IO.monoMsNow

  logInfo m!"time: {end_time - start_time}ms"

def naivePower (x n : Nat) :=
  aux x n 1
where aux (x n acc : Nat) :=
  match n with
  | 0 => acc
  | n + 1 => aux x n (acc * x)

/-
time: 490ms
-/
#time #eval naivePower 2 110000

def main : IO Unit := do
  let start_time ← IO.monoMsNow
  let result := naivePower 2 110000
  let end_time ← IO.monoMsNow
  IO.println s!"result: {result}"
  IO.println s!"naive power: ({end_time - start_time} ms)"

-- time: 0 ms
#eval main

[Asei Inoue]

why #eval main outputs time : 0ms?

[Henrik Böving]

Most likely because the naivePower got lifted out of main and is being precomputed

[Asei Inoue]

Thank you. how to prevent this?

[Simon Daniel]

if you compute naivePower in IO it does not seem to lift it out of main (but somehow the timing is different to the one of #time ~137ms)

def naivePower (x n : Nat): IO Nat := ...