From a0d0abcdc5a59368d0a920b7a89cb5c02903bc8a Mon Sep 17 00:00:00 2001 From: Garmelon Date: Fri, 28 Nov 2025 15:40:43 +0100 Subject: [PATCH] chore: update and add benchmark metrics (#11420) This PR adds per-module `.ilean` and `.olean` file size metrics, global and per-module cycle counting, and adds back `lean --stat`-based metrics. It also renames some `size/*` metrics to get rid of the name `stdlib`. --- tests/bench-radar/build/README.md | 10 ++++- tests/bench-radar/build/lean_wrapper.py | 50 ++++++++++++++++++++++--- tests/bench-radar/build/run | 2 +- tests/bench-radar/measure.py | 1 + tests/bench-radar/size/README.md | 36 +++++++++--------- tests/bench-radar/size/run | 16 ++++---- 6 files changed, 81 insertions(+), 34 deletions(-) diff --git a/tests/bench-radar/build/README.md b/tests/bench-radar/build/README.md index 82bac07af2..0b071c40bf 100644 --- a/tests/bench-radar/build/README.md +++ b/tests/bench-radar/build/README.md @@ -5,14 +5,17 @@ and collects global and per-module metrics. The following metrics are collected by a wrapper around the entire build process: +- `build//cycles` - `build//instructions` - `build//maxrss` - `build//task-clock` - `build//wall-clock` -The following metrics are collected from `leanc --profile` and summed across all modules: +The following metrics are collected from `leanc --profile` and `leanc --stat` and summed across all modules: - `build/profile///wall-clock` +- `build/stat///amount` +- `build/stat///bytes` The following metrics are collected from `lakeprof report`: @@ -22,7 +25,12 @@ The following metrics are collected from `lakeprof report`: The following metrics are collected individually for each module: - `build/module///lines` +- `build/module///cycles` - `build/module///instructions` +- `build/module///bytes .ilean` +- `build/module///bytes .olean` +- `build/module///bytes .olean.server` +- `build/module///bytes .olean.private` If the file `build_upload_lakeprof_report` is present in the repo root, the lakeprof report will be uploaded once the benchmark run concludes. diff --git a/tests/bench-radar/build/lean_wrapper.py b/tests/bench-radar/build/lean_wrapper.py index a4e3303881..977c4e35e3 100755 --- a/tests/bench-radar/build/lean_wrapper.py +++ b/tests/bench-radar/build/lean_wrapper.py @@ -5,6 +5,7 @@ import json import re import subprocess import sys +from collections import Counter from pathlib import Path NAME = "build" @@ -28,13 +29,13 @@ def run(*command: str) -> None: sys.exit(result.returncode) -def run_stderr(*command: str) -> str: +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.stderr + return result.stdout, result.stderr def get_module(setup: Path) -> str: @@ -48,20 +49,31 @@ def count_lines(module: str, path: Path) -> None: save_result(f"{NAME}/module/{module}//lines", lines) +def count_bytes(module: str, path: Path, suffix: str) -> None: + try: + bytes = path.with_suffix(suffix).stat().st_size + except FileNotFoundError: + return + save_result(f"{NAME}/module/{module}//bytes {suffix}", bytes, "B") + + def run_lean(module: str) -> None: - stderr = run_stderr( + stdout, stderr = run_capture( f"{BENCH}/measure.py", *("-t", f"{NAME}/module/{module}"), *("-o", f"{OUT}"), *("-m", "instructions"), + *("-m", "cycles"), "--", - *(f"{STAGE2}/bin/lean.wrapped", "--profile", "-Dprofiler.threshold=9999999"), + f"{STAGE2}/bin/lean.wrapped", + *("--profile", "-Dprofiler.threshold=9999999"), + "--stat", *sys.argv[1:], ) + # Output of `lean --profile` + # See timeit.cpp for the time format for line in stderr.splitlines(): - # Output of `lean --profile` - # See timeit.cpp for the time format if match := re.fullmatch(r"\t(.*) ([\d.]+)(m?s)", line): name = match.group(1) seconds = float(match.group(2)) @@ -69,20 +81,46 @@ def run_lean(module: str) -> None: seconds = seconds / 1000 save_result(f"{NAME}/profile/{name}//wall-clock", seconds, "s") + # Output of `lean --stat` + stat = Counter[str]() + for line in stdout.splitlines(): + if match := re.fullmatch(r"number of (imported .*):\s+(\d+)$", line): + name = match.group(1) + count = int(match.group(2)) + stat[name] += count + for name, count in stat.items(): + if count > 0: + if name.endswith("bytes"): + save_result(f"{NAME}/stat/{name}//bytes", count, "B") + else: + save_result(f"{NAME}/stat/{name}//amount", count) + def main() -> None: parser = argparse.ArgumentParser() parser.add_argument("lean", type=Path) parser.add_argument("--setup", type=Path) + parser.add_argument("--i", "-i", type=Path) + parser.add_argument("--o", "-o", type=Path) args, _ = parser.parse_known_args() lean: Path = args.lean setup: Path = args.setup + ilean: Path | None = args.i + olean: Path | None = args.o module = get_module(setup) + count_lines(module, lean) run_lean(module) + if ilean is not None: + count_bytes(module, ilean, ".ilean") + if olean is not None: + count_bytes(module, olean, ".olean") + count_bytes(module, olean, ".olean.server") + count_bytes(module, olean, ".olean.private") + if __name__ == "__main__": main() diff --git a/tests/bench-radar/build/run b/tests/bench-radar/build/run index c1dd0cb897..77517c0042 100755 --- a/tests/bench-radar/build/run +++ b/tests/bench-radar/build/run @@ -22,7 +22,7 @@ cp "$BENCH/build/lean_wrapper.py" "$STAGE2/bin/lean" # Build stage3 "$BENCH/measure.py" -t build \ - -m instructions -m maxrss -m task-clock -m wall-clock -- \ + -m cycles -m instructions -m maxrss -m task-clock -m wall-clock -- \ lakeprof record -- \ make -C build/release -j"$(nproc)" stage3 diff --git a/tests/bench-radar/measure.py b/tests/bench-radar/measure.py index 482ac332ff..0155c6d01f 100755 --- a/tests/bench-radar/measure.py +++ b/tests/bench-radar/measure.py @@ -38,6 +38,7 @@ PERF_METRICS = { "task-clock": PerfMetric("task-clock", factor=1e-9, unit="s"), "wall-clock": PerfMetric("duration_time", factor=1e-9, unit="s"), "instructions": PerfMetric("instructions"), + "cycles": PerfMetric("cycles"), } RUSAGE_METRICS = { diff --git a/tests/bench-radar/size/README.md b/tests/bench-radar/size/README.md index b0031448e2..8e3757474d 100644 --- a/tests/bench-radar/size/README.md +++ b/tests/bench-radar/size/README.md @@ -1,30 +1,30 @@ # The `size` benchmark This benchmark measures the number and size of a few kinds of files. -It expects to be executed after the `stdlib` benchmark. +It expects to be executed after the `build` benchmark. The following general metrics are collected: - `size/libleanshared.so//bytes` -The following metrics are collected for the entirety of stdlib: +The following metrics are collected from the entire build process: -- `size/stdlib/.c//files` -- `size/stdlib/.c//lines` -- `size/stdlib/.cpp//files` -- `size/stdlib/.cpp//lines` -- `size/stdlib/.lean//files` -- `size/stdlib/.lean//lines` -- `size/stdlib/.ilean//files` -- `size/stdlib/.ilean//bytes` -- `size/stdlib/.olean//files` -- `size/stdlib/.olean//bytes` -- `size/stdlib/.olean.server//files` -- `size/stdlib/.olean.server//bytes` -- `size/stdlib/.olean.private//files` -- `size/stdlib/.olean.private//bytes` -- `size/stdlib/.ir//files` -- `size/stdlib/.ir//bytes` +- `size/all/.c//files` +- `size/all/.c//lines` +- `size/all/.cpp//files` +- `size/all/.cpp//lines` +- `size/all/.lean//files` +- `size/all/.lean//lines` +- `size/all/.ilean//files` +- `size/all/.ilean//bytes` +- `size/all/.olean//files` +- `size/all/.olean//bytes` +- `size/all/.olean.server//files` +- `size/all/.olean.server//bytes` +- `size/all/.olean.private//files` +- `size/all/.olean.private//bytes` +- `size/all/.ir//files` +- `size/all/.ir//bytes` The following metrics are collected only for the `Init` library. diff --git a/tests/bench-radar/size/run b/tests/bench-radar/size/run index fa7ea2c856..f149ee29ae 100755 --- a/tests/bench-radar/size/run +++ b/tests/bench-radar/size/run @@ -47,14 +47,14 @@ if __name__ == "__main__": ) # Stdlib - measure_lines("size/stdlib/.c", STAGE3_TEMP.glob("**/*.c")) - measure_bytes("size/stdlib/.ir", STAGE3_LEAN.glob("**/*.ir")) - measure_lines("size/stdlib/.cpp", SRC.glob("**/*.cpp")) - measure_lines("size/stdlib/.lean", SRC.glob("**/*.lean")) - measure_bytes("size/stdlib/.ilean", STAGE3_LEAN.glob("**/*.ilean")) - measure_bytes("size/stdlib/.olean", STAGE3_LEAN.glob("**/*.olean")) - measure_bytes("size/stdlib/.olean.server", STAGE3_LEAN.glob("**/*.olean.server")) - measure_bytes("size/stdlib/.olean.private", STAGE3_LEAN.glob("**/*.olean.private")) + measure_lines("size/all/.c", STAGE3_TEMP.glob("**/*.c")) + measure_bytes("size/all/.ir", STAGE3_LEAN.glob("**/*.ir")) + measure_lines("size/all/.cpp", SRC.glob("**/*.cpp")) + measure_lines("size/all/.lean", SRC.glob("**/*.lean")) + measure_bytes("size/all/.ilean", STAGE3_LEAN.glob("**/*.ilean")) + measure_bytes("size/all/.olean", STAGE3_LEAN.glob("**/*.olean")) + measure_bytes("size/all/.olean.server", STAGE3_LEAN.glob("**/*.olean.server")) + measure_bytes("size/all/.olean.private", STAGE3_LEAN.glob("**/*.olean.private")) # Init measure_bytes("size/init/.olean", STAGE3_LEAN.glob("Init/**/*.olean"))