Timing and repeated samples

Establish a reproducible measurement

Suppose somebody says, "builds got slower after yesterday's import cleanup." One timed run shows where the time went. Repeated samples show whether the change is stable. Warmups distinguish cold behavior from the warmed-up path used during day-to-day work.

The JSON report keeps the exact command, raw samples, and summary together, so a later comparison does not depend on a median copied from terminal history.

lev --timings build --no-sync --offline
lev profile --warmup 1 --repeat 5
lev inspect performance --warmup 1 --repeat 5 --json --output profile.json -- lake build MyTarget

Measurement tools and their scope

Lean work can be timed at several layers. time is enough for a quick total, and hyperfine is a stronger general benchmark runner. lev adds project-aware phase timing, reports, and file ranking around Lake and Lean.

lev --timings separates lev's preparation from the delegated process. When the command phase dominates, repeated samples and file ranking can narrow the cause further.

Locate the slow layer with --timings

Read the phase that owns most of the run. If the command phase dominates, inspect Lake or Lean next. If preparation dominates, investigate work outside the proof.

lev records timestamps around its own boundaries and treats the delegated child process as one measured phase. The command row separates lev's orchestration from the build or test process.

lev --timings build --no-sync --offline

lev timing: environment 0.001 ms
lev timing: prepare 140.983 ms
lev timing: locks 0.343 ms
Build completed successfully.
lev timing: command 299.666 ms
lev timing: total 441.176 ms

Read the proportions first. Here the delegated command dominates, while preparation is still visible. Timing lines go to stderr so stdout stays available for the command's own output or JSON.

The rows come directly from lev's execution path:

How to read this run

• environment is effectively zero, so selector resolution is not the cause.
• prepare is noticeable but not dominant, so lev preflight work exists but is not the main problem.
• locks is negligible, so there is no real evidence of contention.
• command owns most of the run, so the next question belongs inside Lake or Lean.

Measure repeated commands with lev profile

Once the delegated command is the slow layer, one run is weak evidence. A shell loop often loses whether there was a warmup, whether the first run was excluded, and what the individual samples were. lev profile records those choices with the run.

Lev prepares the project and acquires shared locks once, executes optional warmups, then times each measured child process from immediately before process launch until it exits. The report records enough context to repeat and explain the run later.

# Defaults to lake build
lev profile --warmup 1 --repeat 5

# Measure a target or arbitrary command
lev profile --warmup 1 --repeat 5 -- lake build MyTarget
lev profile --warmup 2 --repeat 10 -- lake test

# Grouped command mode records the richer inspection schema
lev inspect performance --warmup 1 --repeat 5

lev: performance warmup 1/1
Build completed successfully.
lev: performance sample 1/5
Build completed successfully.
lev: performance sample 2/5
Build completed successfully.
lev: performance sample 3/5
Build completed successfully.
lev: performance sample 4/5
Build completed successfully.
lev: performance sample 5/5
Build completed successfully.
performance: 5 samples, command `lake build`
     1:    299.147 ms
     2:    297.862 ms
     3:    309.765 ms
     4:    304.074 ms
     5:    304.723 ms
  min    297.862 ms  median    304.074 ms  mean    303.114 ms  max    309.765 ms

Warmup progress is printed separately and never enters the sample list. That separation matters when the first run populates caches or when Lake spends the first pass discovering that outputs are already current.

What warmups do

A warmup is a complete command execution before measurement. It can populate operating-system page caches, initialize compiler state persisted on disk, or let Lake discover that outputs are already current. Lev excludes warmup durations from the measured distribution.

A useful habit is to state the experiment plainly: "one warmup, then five measured incremental builds." If that sentence sounds wrong, the run setup is probably wrong too.

Read the statistics carefully

Minimum

The fastest observed sample. Useful as a lower bound, but easy to overvalue.

Median

The middle sample after sorting. Less sensitive than the mean to a single noisy run.

Mean

The arithmetic average. Useful for total expected cost, but pulled by outliers.

Maximum

The slowest observed sample. Investigate when tail latency matters.

The current report does not calculate standard deviation or confidence intervals, so keep the raw samples. Five runs can expose obvious noise. Small claimed improvements deserve larger, interleaved A/B experiments.

• Keep toolchain, project revision, target, power mode, and machine fixed.
• Record whether caches are cold, warm, or intentionally cleared.
• Avoid running unrelated CPU-, memory-, or I/O-heavy jobs at the same time.
• Compare distributions and source changes, not only the best number.

Small differences need more than a median row. Keep the raw samples, the exact command, and the run conditions, or the result will be hard to defend a week later.

Save a stable JSON report

lev inspect performance \
  --warmup 1 \
  --repeat 5 \
  --json \
  --output profile.json \
  -- lake build MyTarget

{
  "schema": "lev.cli.inspect.performance/v1",
  "data": {
    "project": "/tmp/lev-doc-profile.GP0wJ1/project",
    "toolchain": "leanprover/lean4:v4.18.0",
    "mode": "command",
    "command": "lake build MyTarget",
    "files": [],
    "baseline": null,
    "warmup": 1,
    "requested_repeats": 5,
    "completed_repeats": 5,
    "samples_ms": [
      302.655627,
      304.326952,
      299.18028400000003,
      298.12469000000004,
      298.515086
    ],
    "summary": {
      "min_ms": 298.12469000000004,
      "median_ms": 299.18028400000003,
      "mean_ms": 300.5605278,
      "max_ms": 304.326952
    },
    "exit_code": 0
  }
}

The JSON keeps every measured sample alongside the summary row. Save it when you want to compare a later run without relying on terminal copy-paste.

jq '.data | {command, samples_ms, summary}' profile.json

If a measured process fails, lev records that sample's elapsed time, stops immediately, writes a partial report with completed_repeats, and returns the child's exit code. If a warmup fails, no measured sample is reported: text output says so directly, and JSON sets summary to null instead of inventing zero timings.

File ranking and Lean traces

Once the slowdown is real and the command phase still owns it, the next job is to narrow the project down. Rank the files first. Open a native Lean trace only for the modules that stay expensive after that cut.

File ranking and baselines covers the project-wide pass. Lean profiler covers trace.profiler, Firefox Profiler export, and heartbeat mode inside the selected file.