benchmarking commands

Stream: lean4

[Mario Carneiro]

Here's a benchmarking command for @Scott Morrison :

import Lean

section
open Lean Elab Command

syntax (name := timeCmd)  "#time " command : command

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

end

set_option maxRecDepth 100000 in
#time example : (List.range 500).length = 500 := rfl

[Mario Carneiro]

Here's a variation using timeit, which I don't like as much because it puts the output in the "output" panel that is usually reserved for fatal errors

def Lean.Elab.Command.CommandElabM.timeit (msg : String) (m : CommandElabM α) : CommandElabM α :=
  fun ctx s => do
    let a ← IO.toEIO (fun ex => Exception.error ctx.ref ex.toString) $
      _root_.timeit msg $ (m ctx s).toIO'
    match a with
    | Except.ok a => a
    | Except.error e => throw e

@[commandElab timeCmd] def elabTimeCmd : CommandElab
  | `(#time $stx:command) => (elabCommand stx).timeit "time"
  | _ => throwUnsupportedSyntax

[Scott Morrison]

Should I be terrified that (List.range n).length = n seems to be cubic in n? :-)

[Scott Morrison]

Could you explain to me why you chose the name elabCmdStx?

[Mario Carneiro]

copypasta

[Mac]

Scott Morrison said:

Should I be terrified that (List.range n).length = n seems to be cubic in n? :-)

I suspect this probably has to do with memory concerns (like locality of reference and allocations/deallocations) in iterating through the list. For n < 100, the example takes about n milliseconds. It is only past that that things start to get unwieldy.

[Mac]

For example, I believe List objects are 24 bytes (3 lean_objects -- each 8 bytes long). So 100 of them is already 2.4KB.

[Mac]

Though, I guess since proofs are interpreted, the List would be in terms of Expr instead? (And that would take up even more memory.)