chore: repeat some benchmarks to avoid outliers

tests/README.md

@@ -249,6 +249,15 @@ These bash variables (set via `<file>.init.sh`) are used by the run script:
   A bash variable containing the expected exit code of the program.
   When set to `nonzero` instead of a numerical value, the exit code must not be 0.
 
+- `TEST_REPEAT`:
+  A number specifying how often to repeat the benchmark.
+  The resulting measurements are averaged.
+  Has no effect when testing.
+
+- `TEST_REPEAT_DROP_HIGHEST`, `TEST_REPEAT_DROP_LOWEST`:
+  A number specifying how many extreme measurements to drop before averaging.
+  Only takes effect if `TEST_REPEAT` is set.
+
 For performance reasons, elab tests can use prebuilt header snapshots.
 Building the snapshots and wiring them into the ctest suite (as the `build_lean_header_snapshots.sh` setup fixture) is gated by the `LEAN_HEADER_SNAPSHOTS` CMake option, which currently defaults to `OFF`.
 Use of the snapshots at runtime is further controlled by the `LEAN_HEADER_SNAPSHOTS` environment variable:
@@ -310,6 +319,15 @@ These bash variables (set via `<file>.init.sh`) are used by the run script:
   A bash variable containing the expected exit code of the program.
   When set to `nonzero` instead of a numerical value, the exit code must not be 0.
 
+- `TEST_REPEAT`:
+  A number specifying how often to repeat the benchmark.
+  The resulting measurements are averaged.
+  Has no effect when testing.
+
+- `TEST_REPEAT_DROP_HIGHEST`, `TEST_REPEAT_DROP_LOWEST`:
+  A number specifying how many extreme measurements to drop before averaging.
+  Only takes effect if `TEST_REPEAT` is set.
+
 ## The `interactive` test pile
 
 These tests are designed to test LSP server requests at a given position in the input file.

tests/bench/build/lakeprof_report_upload.py

@@ -7,8 +7,8 @@
 
 # Determine paths relative to the current file.
 script_file = Path(__file__)
-src_dir = script_file.parent.parent.parent.parent / "src"
 template_file = script_file.parent / "lakeprof_report_template.html"
+src_dir = script_file.parent.parent.parent.parent / "src"
 
 
 def run_stdout(*command: str, cwd: Path | None = None) -> str:

tests/bench/build/lean_wrapper.py

@@ -35,15 +35,6 @@ def run(*command: str) -> None:
         sys.exit(result.returncode)
 
 
-def run_capture(*command: str) -> tuple[str, str]:
-    result = subprocess.run(command, capture_output=True, encoding="utf-8")
-    if result.returncode != 0:
-        print(result.stdout, end="", file=sys.stdout)
-        print(result.stderr, end="", file=sys.stderr)
-        sys.exit(result.returncode)
-    return result.stdout, result.stderr
-
-
 def get_module(setup: Path) -> str:
     with open(setup) as f:
         return json.load(f)["name"]

tests/compile_bench/incr_header_load.lean

@@ -1,19 +1,15 @@
 /-!
 Bench: time `lean --incr-load=…` reusing a pre-saved snapshot whose header is `import Lean`.
 The snapshot is pre-created by `.before.sh` so that the measurement only covers loading,
-not the cost of producing the snapshot.
+not the cost of producing the snapshot. The snapshot is read-only and left in place (rather
+than deleted here) so it can be reused across this benchmark's repeated invocations.
 -/
 
 unsafe def main : IO Unit := do
   let src  : System.FilePath := "_tmp_incr_header_load_src.lean"
   let snap : System.FilePath := "_tmp_incr_header_load.snap"
-  let deps := snap.addExtension "deps"
 
   let _ ← IO.Process.run {
     cmd  := "lean"
     args := #[s!"--incr-load={snap}", src.toString]
   }
-
-  IO.FS.removeFile src
-  IO.FS.removeFile snap
-  IO.FS.removeFile deps

tests/compile_bench/incr_header_load.lean.init.sh

@@ -0,0 +1,2 @@
+TEST_REPEAT=2
+TEST_REPEAT_DROP_HIGHEST=1

tests/compile_bench/run_bench.sh

@@ -25,9 +25,7 @@ if [[ -n $DO_COMPILE ]]; then
   lean --c="$1.c" -Dcompiler.postponeCompile=false "${TEST_LEAN_ARGS[@]}" "$1" || fail "Failed to compile $1 into $1.c"
   leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$1.out" "${TEST_LEANC_ARGS[@]}" "$1.c" || fail "Failed to compile $1.c"
 
-  capture_only "$1" \
-    "$TEST_DIR/measure.py" -t "$TOPIC" -o "$1.measurements.jsonl" -a -d -- \
-    "./$1.out" "${TEST_ARGS[@]}"
+  capture_and_measure "$1" "$TOPIC" "./$1.out" "${TEST_ARGS[@]}"
   check_exit_is "${TEST_EXIT:-0}"
   extract_measurements "$TOPIC"
 
@@ -45,8 +43,7 @@ if [[ -n $DO_INTERPRET ]]; then
 
   TOPIC="interpreted/$(basename "$1" .lean)"
 
-  capture_only "$1" \
-    "$TEST_DIR/measure.py" -t "$TOPIC" -o "$1.measurements.jsonl" -a -d -- \
+  capture_and_measure "$1" "$TOPIC" \
     lean -Dlinter.all=false "${TEST_LEANI_ARGS[@]}" --run "$1" "${TEST_ARGS[@]}"
   check_exit_is "${TEST_EXIT:-0}"
   extract_measurements "$TOPIC"

tests/elab_bench/run_bench.sh

@@ -3,10 +3,11 @@ run_before "$1"
 
 TOPIC="elab/$(basename "$1" .lean)"
 
+rm -f "$1.measurements.jsonl"
+
 # `--root` to infer same private names as in the server
 # Elab.inServer to allow for arbitrary `#eval`
-capture_only "$1" \
-  "$TEST_DIR/measure.py" -t "$TOPIC" -o "$1.measurements.jsonl" -d -- \
+capture_and_measure "$1" "$TOPIC" \
   lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true "${TEST_LEAN_ARGS[@]}" "$1"
 normalize_mvar_suffixes
 normalize_reference_urls

tests/measure.py

@@ -7,7 +7,6 @@
 import subprocess
 import sys
 import tempfile
-from argparse import Namespace
 from dataclasses import dataclass
 from pathlib import Path
 from typing import Tuple
@@ -184,8 +183,7 @@ def main(
     return measured.stdout, measured.stderr
 
 
-@dataclass
-class Args(Namespace):
+class Args:
     topic: list[str]
     metric: list[str]
     default_metrics: bool
@@ -243,7 +241,7 @@ class Args(Namespace):
         default=[],
         help="arguments to pass to the command",
     )
-    args = parser.parse_args(namespace=Args)
+    args = parser.parse_args(namespace=Args())
 
     metrics = set(args.metric)
     if args.default_metrics:

tests/repeatedly.py

@@ -0,0 +1,172 @@
+#!/usr/bin/env python3
+
+import argparse
+import json
+import subprocess
+import sys
+from contextlib import contextmanager
+from dataclasses import dataclass
+from pathlib import Path
+
+
+@dataclass
+class Measurement:
+    metric: str
+    value: float
+    unit: str | None
+
+    @classmethod
+    def from_json_str(cls, s: str) -> "Measurement":
+        data = json.loads(s.strip())
+        return cls(data["metric"], data["value"], data.get("unit"))
+
+    def to_json_str(self) -> str:
+        if self.unit is None:
+            return json.dumps({"metric": self.metric, "value": self.value})
+        return json.dumps(
+            {"metric": self.metric, "value": self.value, "unit": self.unit}
+        )
+
+
+@contextmanager
+def temporarily_move_outfile(outfile: Path):
+    outfile_tmp = outfile.with_name(outfile.name + ".repeatedly_tmp")
+    if outfile_tmp.exists():
+        raise Exception(f"{outfile_tmp} already exists")
+
+    outfile.touch()
+    outfile.rename(outfile_tmp)
+    try:
+        yield
+    finally:
+        outfile_tmp.rename(outfile)
+
+
+def read_measurements_from_outfile(outfile: Path) -> list[Measurement]:
+    measurements = []
+    with open(outfile, "r") as f:
+        for line in f:
+            measurements.append(Measurement.from_json_str(line))
+    return measurements
+
+
+def write_measurements_to_outfile(
+    outfile: Path, measurements: list[Measurement]
+) -> None:
+    with open(outfile, "a") as f:
+        for measurement in measurements:
+            f.write(f"{measurement.to_json_str()}\n")
+
+
+def run_once(cmd: list[str], outfile: Path) -> list[Measurement]:
+    with temporarily_move_outfile(outfile):
+        proc = subprocess.run(cmd)
+        if proc.returncode != 0:
+            sys.exit(proc.returncode)
+
+        return read_measurements_from_outfile(outfile)
+
+
+def sum_by_metric(measurements: list[Measurement]) -> dict[str, Measurement]:
+    totals: dict[str, Measurement] = {}
+    for measurement in measurements:
+        if existing := totals.get(measurement.metric):
+            measurement.value += existing.value
+        totals[measurement.metric] = measurement
+    return totals
+
+
+def repeatedly(
+    cmd: list[str],
+    iterations: int,
+    outfile: Path,
+    drop_highest: int = 0,
+    drop_lowest: int = 0,
+) -> list[Measurement]:
+    by_metric: dict[str, list[Measurement]] = {}
+
+    for i in range(iterations):
+        for metric, measurement in sum_by_metric(run_once(cmd, outfile)).items():
+            by_metric.setdefault(metric, []).append(measurement)
+
+    if drop_highest + drop_lowest >= iterations:
+        raise ValueError(
+            f"drop_highest ({drop_highest}) + drop_lowest ({drop_lowest}) must be "
+            f"less than the number of iterations ({iterations})"
+        )
+
+    results = []
+    for metric, measurements in by_metric.items():
+        if drop_highest or drop_lowest:
+            measurements.sort(key=lambda m: m.value)
+            measurements = measurements[drop_lowest : len(measurements) - drop_highest]
+        if not measurements:
+            continue
+        unit = measurements[0].unit
+        value = sum(m.value for m in measurements) / len(measurements)
+        results.append(Measurement(metric, value, unit))
+
+    return results
+
+
+class Args:
+    iterations: int
+    drop_highest: int
+    drop_lowest: int
+    outfile: Path
+    cmd: str
+    args: list[str]
+
+
+if __name__ == "__main__":
+    parser = argparse.ArgumentParser(
+        description="Repeatedly run a command, averaging the measurements it writes.",
+    )
+    parser.add_argument(
+        "-n",
+        "--iterations",
+        type=int,
+        default=5,
+        help="number of iterations",
+    )
+    parser.add_argument(
+        "-H",
+        "--drop-highest",
+        type=int,
+        default=0,
+        help="drop the n highest values of each metric before averaging",
+    )
+    parser.add_argument(
+        "-L",
+        "--drop-lowest",
+        type=int,
+        default=0,
+        help="drop the n lowest values of each metric before averaging",
+    )
+    parser.add_argument(
+        "-o",
+        "--outfile",
+        type=Path,
+        default=Path("measurements.jsonl"),
+        help="measurements file the command under test writes to",
+    )
+    parser.add_argument(
+        "cmd",
+        help="command to repeatedly run",
+    )
+    parser.add_argument(
+        "args",
+        nargs="*",
+        default=[],
+        help="arguments to pass to the command",
+    )
+    args = parser.parse_args(namespace=Args())
+
+    measurements = repeatedly(
+        [args.cmd] + args.args,
+        args.iterations,
+        args.outfile,
+        args.drop_highest,
+        args.drop_lowest,
+    )
+    write_measurements_to_outfile(args.outfile, measurements)

tests/util.sh

@@ -117,6 +117,27 @@ function capture_exit {
   check_exit_is "$EXPECTED"
 }
 
+# Run a command wrapped with `capture_only` and `measure.py`.
+# Additionally wrap with `repeatedly.py` if `TEST_REPEAT` is set,
+# respecting `TEST_REPEAT_DROP_HIGHEST` and `TEST_REPEAT_DROP_LOWEST`.
+# The first argument specifies the output file path.
+# The second argument specifies the topic for the measurements.
+# The remaining arguments are the command to run.
+# Sets $EXIT to the exit code and $CAPTURED to the output file path.
+function capture_and_measure {
+  local file="$1" topic="$2"; shift 2
+  if [[ -n "${TEST_REPEAT:-}" ]]; then
+    capture_only "$file" \
+      "$TEST_DIR/repeatedly.py" -n "$TEST_REPEAT" \
+      -H "${TEST_REPEAT_DROP_HIGHEST:-0}" -L "${TEST_REPEAT_DROP_LOWEST:-0}" \
+      -o "$file.measurements.jsonl" -- \
+      "$TEST_DIR/measure.py" -t "$topic" -o "$file.measurements.jsonl" -d -- "$@"
+  else
+    capture_only "$file" \
+      "$TEST_DIR/measure.py" -t "$topic" -o "$file.measurements.jsonl" -a -d -- "$@"
+  fi
+}
+
 function source_init {
   if [[ -f "$1.init.sh" ]]; then
     source "$1.init.sh"