chore: add radar benchmark suite (leanprover-community#33762)

This PR adds the benchmark suite to mathlib that radar has already been using for a while. It can also be run standalone following the instructions in `scripts/bench/README.md`. Radar will automatically switch to this suite once merged.

Compared to the radar bench suite, there have been some smaller changes:
1. All measurement results are now collected in the `measurements.jsonl` file. Previously, some results were instead emitted via stdout/stderr, but that makes it more difficult to run the bench suite standalone.
2. The `lint` benchmark now no longer includes the build of `runLinter` in its measurements, only the linting itself.

Co-authored-by: Joscha <joscha@plugh.de>

Author: Garmelon

scripts/README.md

@@ -15,6 +15,7 @@ to learn about it as well!
   If these web pages are deprecated or removed, we should remove these scripts.
 
 **Repository analysis and reporting**
+- `bench` is mathlib's benchmark suite. View its [README.md](bench/README.md) for more details.
 - `user_activity_report.py`
   Generates a comprehensive report of all users with repository access and their last commit activity.
   Shows username, age of last commit, and access level, sorted by commit recency (most recent first).

scripts/bench/README.md

@@ -0,0 +1,38 @@
+# Mathlib4 benchmark suite
+
+This directory contains the mathlib4 benchmark suite.
+It is built around [radar](github.com/leanprover/radar)
+and benchmark results can be viewed
+on the [Lean FRO radar instance](https://radar.lean-lang.org/repos/mathlib4).
+
+To execute the entire suite, run `scripts/bench/run` in the repo root.
+To execute an individual benchmark, run `scripts/bench/<benchmark>/run` in the repo root.
+All scripts output their measurements into the file `measurements.jsonl`.
+
+Radar sums any duplicated measurements with matching metrics.
+To post-process the `measurements.jsonl` file this way in-place,
+run `scripts/bench/combine.py` in the repo root after executing the benchmark suite.
+
+The `*.py` symlinks exist only so the python files are a bit nicer to edit
+in text editors that rely on the file ending.
+
+## Adding a benchmark
+
+To add a benchmark to the suite, follow these steps:
+
+1. Create a new folder containing a `run` script and a `README.md` file describing the benchmark,
+   as well as any other files required for the benchmark.
+2. Edit `scripts/bench/run` to call the `run` script of your new benchmark.
+
+## How radar executes the benchmark suite
+
+Radar requires a _bench repo_ to be configured for each repo.
+The bench repo contains scripts that execute benchmarks and present the results to radar
+following the
+[bench repo specification](https://github.com/leanprover/radar/blob/62bffab39025a1c2039499ae7a85b1ad446286d9/README.md#bench-repo-specification).
+
+The bench repo for mathlib4 is
+[leanprover/radar-bench-mathlib4](https://github.com/leanprover/radar-bench-mathlib4).
+It calls the bench suite inside the mathlib repository and passes the results on to radar.
+It expects all measurements to be presented through the `measurements.jsonl` file,
+_not_ through stdout/stderr (even though this would be allowed by the bench script specification).

scripts/bench/build/README.md

@@ -0,0 +1,27 @@
+# The `build` benchmark
+
+This benchmark executes a complete build of mathlib4 and collects global and per-module metrics.
+
+The following metrics are collected by a wrapper around the entire build process:
+
+- `build//instructions`
+- `build//maxrss`
+- `build//task-clock`
+- `build//wall-clock`
+
+The following metrics are collected from `leanc --profile` and summed across all modules:
+
+- `build/profile/<name>//wall-clock`
+
+The following metrics are collected from `lakeprof report`:
+
+- `build/lakeprof/longest build path//wall-clock`
+- `build/lakeprof/longest rebuild path//wall-clock`
+
+The following metrics are collected individually for each module:
+
+- `build/module/<name>//lines`
+- `build/module/<name>//instructions`
+
+If the file `build_upload_lakeprof_report` is present in the repo root,
+the lakeprof report will be uploaded once the benchmark run concludes.

scripts/bench/build/fake-root/bin/lean

@@ -0,0 +1,94 @@
+#!/usr/bin/env python3
+
+import argparse
+import json
+import re
+import subprocess
+import sys
+from pathlib import Path
+
+NAME = "build"
+REPO = Path()
+BENCH = REPO / "scripts" / "bench"
+OUTFILE = REPO / "measurements.jsonl"
+
+
+def save_result(metric: str, value: float, unit: str | None = None) -> None:
+    data = {"metric": metric, "value": value}
+    if unit is not None:
+        data["unit"] = unit
+    with open(OUTFILE, "a+") as f:
+        f.write(f"{json.dumps(data)}\n")
+
+
+def run(*command: str) -> None:
+    result = subprocess.run(command)
+    if result.returncode != 0:
+        sys.exit(result.returncode)
+
+
+def run_stderr(*command: 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
+
+
+def get_module(setup: Path) -> str:
+    with open(setup) as f:
+        return json.load(f)["name"]
+
+
+def count_lines(module: str, path: Path) -> None:
+    with open(path) as f:
+        lines = sum(1 for _ in f)
+    save_result(f"{NAME}/module/{module}//lines", lines)
+
+
+def run_lean(module: str) -> None:
+    stderr = run_stderr(
+        f"{BENCH}/measure.py",
+        *("-t", f"{NAME}/module/{module}"),
+        *("-m", "instructions"),
+        "--",
+        *("lean", "--profile", "-Dprofiler.threshold=9999999"),
+        *sys.argv[1:],
+    )
+
+    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))
+            if match.group(3) == "ms":
+                seconds = seconds / 1000
+            save_result(f"{NAME}/profile/{name}//wall-clock", seconds, "s")
+
+
+def main() -> None:
+    if sys.argv[1:] == ["--print-prefix"]:
+        print(Path(__file__).resolve().parent.parent)
+        return
+
+    if sys.argv[1:] == ["--githash"]:
+        run("lean", "--githash")
+        return
+
+    parser = argparse.ArgumentParser()
+    parser.add_argument("lean", type=Path)
+    parser.add_argument("--setup", type=Path)
+    args, _ = parser.parse_known_args()
+
+    lean: Path = args.lean
+    setup: Path = args.setup
+
+    module = get_module(setup)
+    count_lines(module, lean)
+    run_lean(module)
+
+
+if __name__ == "__main__":
+    main()

scripts/bench/build/fake-root/bin/lean.py

@@ -0,0 +1 @@
+lean

scripts/bench/build/lakeprof_report_template.html

@@ -0,0 +1,74 @@
+<!DOCTYPE html>
+<html>
+  <head>
+    <meta charset="UTF-8" />
+    <title>Lakeprof Report</title>
+  </head>
+  <body>
+    <h1>Lakeprof Report</h1>
+    <button type="button" id="btn_fetch">View build trace in Perfetto</button>
+    <pre><code>__LAKEPROF_REPORT__</code></pre>
+
+    <script type="text/javascript">
+      // https://perfetto.dev/docs/visualization/deep-linking-to-perfetto-ui
+      // https://gist.github.com/chromy/170c11ce30d9084957d7f3aa065e89f8
+
+      const BASE_URL = __BASE_URL__;
+      const ORIGIN = "https://ui.perfetto.dev";
+
+      const btnFetch = document.getElementById("btn_fetch");
+
+      async function fetchAndOpen(traceUrl) {
+        const resp = await fetch(traceUrl);
+        // Error checking is left as an exercise to the reader.
+        const blob = await resp.blob();
+        const arrayBuffer = await blob.arrayBuffer();
+        openTrace(arrayBuffer, traceUrl);
+      }
+
+      function openTrace(arrayBuffer, traceUrl) {
+        const win = window.open(ORIGIN);
+        if (!win) {
+          btnFetch.style.background = "#f3ca63";
+          btnFetch.onclick = () => openTrace(arrayBuffer);
+          btnFetch.innerText =
+            "Popups blocked, click here to open the trace file";
+          return;
+        }
+
+        const timer = setInterval(() => win.postMessage("PING", ORIGIN), 50);
+
+        const onMessageHandler = (evt) => {
+          if (evt.data !== "PONG") return;
+
+          // We got a PONG, the UI is ready.
+          window.clearInterval(timer);
+          window.removeEventListener("message", onMessageHandler);
+
+          const reopenUrl = new URL(location.href);
+          reopenUrl.hash = `#reopen=${traceUrl}`;
+          win.postMessage(
+            {
+              perfetto: {
+                buffer: arrayBuffer,
+                title: "Lake Build Trace",
+                url: reopenUrl.toString(),
+              },
+            },
+            ORIGIN
+          );
+        };
+
+        window.addEventListener("message", onMessageHandler);
+      }
+
+      // This is triggered when following the link from the Perfetto UI's sidebar.
+      if (location.hash.startsWith("#reopen=")) {
+        const traceUrl = location.hash.substr(8);
+        fetchAndOpen(traceUrl);
+      }
+
+      btnFetch.onclick = () => fetchAndOpen(`${BASE_URL}/lakeprof.trace_event`);
+    </script>
+  </body>
+</html>

scripts/bench/build/lakeprof_report_upload.py

@@ -0,0 +1,44 @@
+#!/usr/bin/env python3
+
+import json
+import subprocess
+import sys
+from pathlib import Path
+
+
+def run(*args: str) -> None:
+    subprocess.run(args, check=True)
+
+
+def run_stdout(*command: str, cwd: str | None = None) -> str:
+    result = subprocess.run(command, capture_output=True, encoding="utf-8", cwd=cwd)
+    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
+
+
+def main() -> None:
+    script_file = Path(__file__)
+    template_file = script_file.parent / "lakeprof_report_template.html"
+
+    sha = run_stdout("git", "rev-parse", "@").strip()
+    base_url = f"https://speed.lean-lang.org/mathlib4-out/{sha}"
+    report = run_stdout("lakeprof", "report", "-prc")
+    with open(template_file) as f:
+        template = f.read()
+
+    template = template.replace("__BASE_URL__", json.dumps(base_url))
+    template = template.replace("__LAKEPROF_REPORT__", report)
+
+    with open("index.html", "w") as f:
+        f.write(template)
+
+    run("curl", "-T", "index.html", f"{base_url}/index.html")
+    run("curl", "-T", "lakeprof.log", f"{base_url}/lakeprof.log")
+    run("curl", "-T", "lakeprof.trace_event", f"{base_url}/lakeprof.trace_event")
+
+
+if __name__ == "__main__":
+    main()

scripts/bench/build/run

@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+BENCH="scripts/bench"
+
+# Prepare build
+# Use build cache for proofwidgets, but not for anything else.
+lake clean
+LEAN_PATH=$(lean --print-libdir) lake build proofwidgets
+rm -f .lake/packages/batteries/.lake/build/bin/runLinter
+
+# Run build
+LAKE_OVERRIDE_LEAN=true LEAN=$(realpath "$BENCH/build/fake-root/bin/lean") \
+  "$BENCH/measure.py" -t build \
+  -m instructions -m maxrss -m task-clock -m wall-clock -- \
+  lakeprof record lake build --no-cache
+
+# Analyze lakeprof data
+lakeprof report -pj | jq -c '{metric: "build/lakeprof/longest build path//wall-clock", value: .[-1][2], unit: "s"}' >> measurements.jsonl
+lakeprof report -rj | jq -c '{metric: "build/lakeprof/longest rebuild path//wall-clock", value: .[-1][2], unit: "s"}' >> measurements.jsonl
+
+# Upload lakeprof report
+# Guarded to prevent accidental uploads (which wouldn't work anyways) during local runs.
+if [ -f build_upload_lakeprof_report ]; then
+  python3 "$BENCH/build/lakeprof_report_upload.py"
+fi

scripts/bench/combine.py

@@ -0,0 +1,31 @@
+#!/usr/bin/env python3
+
+import argparse
+import json
+from pathlib import Path
+
+OUTFILE = Path() / "measurements.jsonl"
+
+if __name__ == "__main__":
+    parser = argparse.ArgumentParser(
+        description=f"Combine duplicated measurements in {OUTFILE.name} the way radar does, by summing their values."
+    )
+    args = parser.parse_args()
+
+    values: dict[str, float] = {}
+    units: dict[str, str | None] = {}
+
+    with open(OUTFILE, "r") as f:
+        for line in f:
+            data = json.loads(line)
+            metric = data["metric"]
+            values[metric] = values.get(metric, 0) + data["value"]
+            units[metric] = data.get("unit")
+
+    with open(OUTFILE, "w") as f:
+        for metric, value in values.items():
+            unit = units.get(metric)
+            data = {"metric": metric, "value": value}
+            if unit is not None:
+                data["unit"] = unit
+            f.write(f"{json.dumps(data)}\n")

scripts/bench/lint/README.md

@@ -0,0 +1,9 @@
+## The `lint` benchmark
+
+This benchmark runs `lake exe runLinter Mathlib`.
+It measures the following metrics:
+
+- `lint//instructions`
+- `lint//maxrss`
+- `lint//task-clock`
+- `lint//wall-clock`