simple performance test

Stream: Is there code for X?

[Asei Inoue]

We know that you can measure execution time with #time. However, it is not clear how to bind the execution time to a variable. Is it possible to verify in code that "the process finishes within x milliseconds"?

[Chris Bailey]

You can observe the durations you get back from things like monoMsNow, but the declarations are opaque, so there's no way to write a theorem proving something like forall (input), runtime (f input) <= n_millis. You can provide a sort of runtime guarantee by just branching on the measured execution time if it's above/below a certain threshold. That being said there are a lot of OS/hardware details that go into measuring real-world time, so it's a guarantee with an asterisk.

[Chris Bailey]

Also reading your question again, I think you can just subtract (t_after - t_before) to get the duration, you should be able to get that from IO.monoMsNow. The source code for timeCmd is a pretty reasonable example:

@[command_elab timeCmd] def timeCmdElab : CommandElab
  | `(#time%$tk $stx:command) => do
    let start ← IO.monoMsNow
    elabCommand stx
    logInfoAt tk m!"time: {(← IO.monoMsNow) - start}ms"
  | _ => throwUnsupportedSyntax

[Asei Inoue]

@Chris Bailey Thank you!