a "timeit" command

Stream: lean4

[Arthur Paulino]

Is there a way to know how long it takes for a declaration to typecheck? Something like:

#timeit 100 my_theorem

Then it would run the typechecking 100 times and would tell me an average +- stddev of the duration. If there isn't anything like this, would it be possible to build a custom command for it?

My motivation came up when thinking about having theorems in programs like this. Then I'd try to optimize it for proof speed.

And another question: does it even make sense to worry about this or is the theorem typechecking process completely ignored in the binary after the compilation?

[Mario Carneiro]

I think timeit already has the meaning of "run this once with the following message attached to the measurement". Perhaps #bench is better to emphasize the "run many times to get good confidence" aspect

[Mario Carneiro]

And another question: does it even make sense to worry about this or is the theorem typechecking process completely ignored in the binary after the compilation?

Yes, typechecking is a compile time notion, it doesn't happen at runtime unless you write your own typechecker or call lean internals at runtime

[Mario Carneiro]

It does make sense to optimize theorem speed, but the purpose is to decrease "compile time". Mathlib takes three hours to "compile" because literally all the theorem proving hard work is "compilation"

[Mario Carneiro]

I put "compile" in quotes because mathlib doesn't produce an executable so even after all that work you don't have a program to show for it

[Arthur Paulino]

Makes sense!
I got curious and tried a small experiment running this program on my interpreter:

N := 1000000
n := 0
while n < N do
  f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 := 0
  i := 0
  while i < 20 do
      f := f i
      i := i + 1
  n := n + 1

It's calling that part that uses the theorem many times. These were the results:

             run 1  run 2  run 3  run 4  run 5      avg     stddev
with theorem 14.533 14.527 14.623 14.527 14.571 → 14.5562 ± 0,0416
with sorry   14.553 14.572 14.582 14.549 14.606 → 14.5724 ± 0,0232

Indeed looks the same to me!

But my other question still holds: would it be possible to build a custom #bench command in Lean 4?

[Tomas Skrivan]

(deleted)