`#time` コマンドが遅いように見えることを注意する

#time コマンドはべらぼうに遅く見えるが、「エラボレーションにかかっている時間」を全部測っているから遅いのであって、別に計算が遅いわけではない。

lean --run で測るのと lake exe で測るのも異なるので、それも注意

def fibonacci (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 => fibonacci n + fibonacci (n + 1)

#time #eval fibonacci 16

def main : IO Unit := do
  let starting := (← IO.monoNanosNow).toFloat
  let result := fibonacci 16
  let ending := (← IO.monoNanosNow).toFloat

  IO.println s!"実行結果: {result}"
  IO.println s!"実行時間: {(ending - starting) / 1000} μs"

実行時間を main で計測したものによると、数マイクロ秒程度

Playground on  main [!?]
❯ lean --run .\Playground\Time.lean
987
time: 13ms
実行結果: 987
実行時間: 1.100000 μs

Playground on  main [!?]
❯ lake exe time
ℹ [2/4] Replayed Playground.Time
info: Playground/Time.lean:9:6: 987
info: Playground/Time.lean:9:0: time: 13ms
実行結果: 987
実行時間: 0.100000 μs

Python の場合

なお Python で同様のコードを書いて実行して計測してみると 300マイクロ秒くらいであった。ただし環境にもよる。

import time

def fibonacci(n: int):
    """フィボナッチ数を計算する"""
    if n == 0:
        return 0
    elif n == 1:
        return 1
    else:
        return fibonacci(n - 1) + fibonacci(n - 2)


start = time.perf_counter()

result = fibonacci(16)

end = time.perf_counter()

print(f"計算結果: {result}")
print(f"実行時間: {(end - start) * 1000_000:.1f} マイクロ秒")

Start with the Playground/Time.lean example and its #time entry point. Compare the shown lean --run and lake exe time outputs, then document that elaboration time is included and that the two commands measure different stages. Done means the example makes the apparent slowness and the distinction between measurement methods clear.