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.

[Marcelo Lynch]

Reviving a very old thread but I couldn't find any more recent discussions on the topic... Does anyone know if there are standard ways of doing this?

I was playing around with this especially interested in measuring the execution of some async tasks, so I just came up with (https://github.com/marcelolynch/timers) some simple Stopwatch / TimedTask structures to wrap a regular Task with timing, say

def demo : IO Unit := do
  let sw ← Stopwatch.startNew
  IO.println s!"Elapsed: {(← sw.elapsed)}"

  let t1 : TimedTask (Except IO.Error String) ← startNew (do
    IO.sleep 3000
    return "done")

  match t1.getMeasured with
  | Except.ok r => IO.println s!"result: {r.1}, duration: {r.2}"
  | Except.error e => IO.println s!"error: {e}"

it also works for timing pure computations via Task.spawn

  let t3 : TimedTask Nat ← startNewPure (Task.spawn (fun _ =>
    (List.range 1000000).foldl (fun acc n => acc + n) 0))

Not sure if I'm reinventing any wheels here...