lean-bench

4.7. Fixed-problem median🔗

For a setup_fixed_benchmark registration there is no parameter sweep. The harness runs one warmup call followed by repeats measured calls (default 5) and reports median, min, max, plus a hash-agreement check across repeats (see Quickstart). Two things to watch for:

  • Non-determinism shows up as hash divergence. Different hashes across repeats of the same benchmark mean the function isn't pure (or its Hashable instance is unstable). The report flags this as hashes diverged. Fix the benchmark before trusting any of its timing numbers.

  • The first measured call is post-warmup but still cold-ish. A single warmup is enough to load FFI libraries and trigger module init, but for an algorithm with its own internal caching (memo tables, lazy initialisation) the first measured call may still be slower than the rest. Reading the median rather than the mean defends against this naturally; raise repeats if min/max spread on your hardware is too wide for a 5-sample median.