Speed and time stamps in Lean 4

Stream: lean4

[Kind Bubble]

How do I measure the speed of my Lean code?

It would be nice if there were some kind of date which worked well under toString.

Best,
Dean

[Jannis Limperg]

For a simple timing function, you can use this:

@[inline]
def time [Monad m] [MonadLiftT BaseIO m] (x : m α) : m (α × Nat) := do
  let start ← monoNanosNow
  let a ← x
  let stop ← monoNanosNow
  return (a, stop - start)

@[inline]
def time' [Monad m] [MonadLiftT BaseIO m] (x : m Unit) : m Nat := do
  let start ← monoNanosNow
  x
  let stop ← monoNanosNow
  return stop - start

Afaik noone has written a decent time and date library yet (which is surprisingly subtle).

[Tomas Skrivan]

Timing library would be nice, there is also timeit function, example.

I'm not surprised noone wrote time and date library, obligatory computerphile video on that topic :)

[Kind Bubble]

Thanks very much this works great.

-- Kind Bubble

[Henrik Böving]

Tomas Skrivan said:

Timing library would be nice, there is also timeit function, example.

I'm not surprised noone wrote time and date library, obligatory computerphile video on that topic :)

I tried copying haskells time stuff a while ago but I got too confused by what was going on to be honest xddd

[Chris Bailey]

@Jannis Limperg @Tomas Skrivan There is a date/time library for Lean 4. When std and mathlib are more stable I have a bunch of improvements and changes to make, but the functionality is there, as are the proofs that were doable with the infrastructure available at the time.