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

@@ -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/<name>//wall-clock`
+- `build/stat/<name>//amount`
+- `build/stat/<name>//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/<name>//lines`
+- `build/module/<name>//cycles`
 - `build/module/<name>//instructions`
+- `build/module/<name>//bytes .ilean`
+- `build/module/<name>//bytes .olean`
+- `build/module/<name>//bytes .olean.server`
+- `build/module/<name>//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.

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()

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
 

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 = {

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.
 

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"))