1. Quickstart🔗

A complete benchmark project in three files.

In lakefile.toml:

name = "myproject"
defaultTargets = ["bench"]

[[require]]
name = "lean-bench"
git = "https://github.com/kim-em/lean-bench.git"
rev = "main"

[[lean_lib]]
name = "MyProject"

[[lean_exe]]
name = "bench"
root = "MyProject.Bench"

In MyProject.lean:

def myFib : Nat → Nat
  | 0 => 0 | 1 => 1 | n + 2 => myFib n + myFib (n + 1)

In MyProject/Bench.lean:

import LeanBench
import MyProject

setup_benchmark myFib n => 2 ^ n

def main (args : List String) : IO UInt32 :=
  LeanBench.Cli.dispatch args

$ lake exe bench list
registered benchmarks:
  myFib    expected complexity: 2 ^ n

1. 1.1. Build and run
2. 1.2. Optional per-param setup
3. 1.3. Complexity expressions
4. 1.4. Tags and filtering
5. 1.5. CI-budget mode
6. 1.6. Configuring a benchmark
7. 1.7. Reading the output
8. 1.8. Auto-fit
9. 1.9. Compare divergence reports
10. 1.10. Fixed-problem benchmarks
11. 1.11. Caveats