measuring proof efficiency

Stream: lean4

[Bartosz Piotrowski]

I wonder if there is some established way of measuring "proof efficiency," meaning how easy it is to compile it.

I learned about #count_heartbeats command, but I'm not sure if this is the best metric for that; also I'm not sure how to use it properly: when I prepend a theorem with #count_heartbeats in, sometimes Lean freezes completely, and sometimes warnings appear in the proof (which otherwise was correct and without warnings).

I also see there is the --profile flag for the lean command, which seems very useful and works fine, but there is a problem of substantial variance across runs.

So I'd be grateful for some insights about this!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hey Bartosz! I don't have a great answer for you; I have been wondering about this myself lately.

One crude metric is to check the size of the proof term using docs#Lean.Expr.numObjs, but different terms of the same size can have drastically different kernel proof checking times, so size is not a great measure.

For measuring the kernel checking compute in terms of heartbeats, I have been using

let d : DefinitionVal := sorry -- get this from the environment or from somewhere
-- the option is critical to ensure `addDecl` waits for the kernel
let (_, heartbeats) <- withOptions (fun opts => Elab.async.set opts false) do
withHeartbeats do
withoutModifyingEnv <| addDecl <| .defnDecl { d with name := d.name ++ `bench }

[Bartosz Piotrowski]

Thanks a lot, Wojciech!