Skip to content

Commit a0d0abc

Browse files
GarmelonGarmelon
authored
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`.
1 parent 5ef1c8d commit a0d0abc

File tree

6 files changed

+81
-34
lines changed

6 files changed

+81
-34
lines changed

‎tests/bench-radar/build/README.md‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,17 @@ and collects global and per-module metrics.
55

66
The following metrics are collected by a wrapper around the entire build process:
77

8+
- `build//cycles`
89
- `build//instructions`
910
- `build//maxrss`
1011
- `build//task-clock`
1112
- `build//wall-clock`
1213

13-
The following metrics are collected from `leanc --profile` and summed across all modules:
14+
The following metrics are collected from `leanc --profile` and `leanc --stat` and summed across all modules:
1415

1516
- `build/profile/<name>//wall-clock`
17+
- `build/stat/<name>//amount`
18+
- `build/stat/<name>//bytes`
1619

1720
The following metrics are collected from `lakeprof report`:
1821

@@ -22,7 +25,12 @@ The following metrics are collected from `lakeprof report`:
2225
The following metrics are collected individually for each module:
2326

2427
- `build/module/<name>//lines`
28+
- `build/module/<name>//cycles`
2529
- `build/module/<name>//instructions`
30+
- `build/module/<name>//bytes .ilean`
31+
- `build/module/<name>//bytes .olean`
32+
- `build/module/<name>//bytes .olean.server`
33+
- `build/module/<name>//bytes .olean.private`
2634

2735
If the file `build_upload_lakeprof_report` is present in the repo root,
2836
the lakeprof report will be uploaded once the benchmark run concludes.

‎tests/bench-radar/build/lean_wrapper.py‎

Lines changed: 44 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
import re
66
import subprocess
77
import sys
8+
from collections import Counter
89
from pathlib import Path
910

1011
NAME = "build"
@@ -28,13 +29,13 @@ def run(*command: str) -> None:
2829
sys.exit(result.returncode)
2930

3031

31-
def run_stderr(*command: str) -> str:
32+
def run_capture(*command: str) -> tuple[str, str]:
3233
result = subprocess.run(command, capture_output=True, encoding="utf-8")
3334
if result.returncode != 0:
3435
print(result.stdout, end="", file=sys.stdout)
3536
print(result.stderr, end="", file=sys.stderr)
3637
sys.exit(result.returncode)
37-
return result.stderr
38+
return result.stdout, result.stderr
3839

3940

4041
def get_module(setup: Path) -> str:
@@ -48,41 +49,78 @@ def count_lines(module: str, path: Path) -> None:
4849
save_result(f"{NAME}/module/{module}//lines", lines)
4950

5051

52+
def count_bytes(module: str, path: Path, suffix: str) -> None:
53+
try:
54+
bytes = path.with_suffix(suffix).stat().st_size
55+
except FileNotFoundError:
56+
return
57+
save_result(f"{NAME}/module/{module}//bytes {suffix}", bytes, "B")
58+
59+
5160
def run_lean(module: str) -> None:
52-
stderr = run_stderr(
61+
stdout, stderr = run_capture(
5362
f"{BENCH}/measure.py",
5463
*("-t", f"{NAME}/module/{module}"),
5564
*("-o", f"{OUT}"),
5665
*("-m", "instructions"),
66+
*("-m", "cycles"),
5767
"--",
58-
*(f"{STAGE2}/bin/lean.wrapped", "--profile", "-Dprofiler.threshold=9999999"),
68+
f"{STAGE2}/bin/lean.wrapped",
69+
*("--profile", "-Dprofiler.threshold=9999999"),
70+
"--stat",
5971
*sys.argv[1:],
6072
)
6173

74+
# Output of `lean --profile`
75+
# See timeit.cpp for the time format
6276
for line in stderr.splitlines():
63-
# Output of `lean --profile`
64-
# See timeit.cpp for the time format
6577
if match := re.fullmatch(r"\t(.*) ([\d.]+)(m?s)", line):
6678
name = match.group(1)
6779
seconds = float(match.group(2))
6880
if match.group(3) == "ms":
6981
seconds = seconds / 1000
7082
save_result(f"{NAME}/profile/{name}//wall-clock", seconds, "s")
7183

84+
# Output of `lean --stat`
85+
stat = Counter[str]()
86+
for line in stdout.splitlines():
87+
if match := re.fullmatch(r"number of (imported .*):\s+(\d+)$", line):
88+
name = match.group(1)
89+
count = int(match.group(2))
90+
stat[name] += count
91+
for name, count in stat.items():
92+
if count > 0:
93+
if name.endswith("bytes"):
94+
save_result(f"{NAME}/stat/{name}//bytes", count, "B")
95+
else:
96+
save_result(f"{NAME}/stat/{name}//amount", count)
97+
7298

7399
def main() -> None:
74100
parser = argparse.ArgumentParser()
75101
parser.add_argument("lean", type=Path)
76102
parser.add_argument("--setup", type=Path)
103+
parser.add_argument("--i", "-i", type=Path)
104+
parser.add_argument("--o", "-o", type=Path)
77105
args, _ = parser.parse_known_args()
78106

79107
lean: Path = args.lean
80108
setup: Path = args.setup
109+
ilean: Path | None = args.i
110+
olean: Path | None = args.o
81111

82112
module = get_module(setup)
113+
83114
count_lines(module, lean)
84115
run_lean(module)
85116

117+
if ilean is not None:
118+
count_bytes(module, ilean, ".ilean")
119+
if olean is not None:
120+
count_bytes(module, olean, ".olean")
121+
count_bytes(module, olean, ".olean.server")
122+
count_bytes(module, olean, ".olean.private")
123+
86124

87125
if __name__ == "__main__":
88126
main()

‎tests/bench-radar/build/run‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ cp "$BENCH/build/lean_wrapper.py" "$STAGE2/bin/lean"
2222

2323
# Build stage3
2424
"$BENCH/measure.py" -t build \
25-
-m instructions -m maxrss -m task-clock -m wall-clock -- \
25+
-m cycles -m instructions -m maxrss -m task-clock -m wall-clock -- \
2626
lakeprof record -- \
2727
make -C build/release -j"$(nproc)" stage3
2828

‎tests/bench-radar/measure.py‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ class RusageMetric:
3838
"task-clock": PerfMetric("task-clock", factor=1e-9, unit="s"),
3939
"wall-clock": PerfMetric("duration_time", factor=1e-9, unit="s"),
4040
"instructions": PerfMetric("instructions"),
41+
"cycles": PerfMetric("cycles"),
4142
}
4243

4344
RUSAGE_METRICS = {

‎tests/bench-radar/size/README.md‎

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,30 @@
11
# The `size` benchmark
22

33
This benchmark measures the number and size of a few kinds of files.
4-
It expects to be executed after the `stdlib` benchmark.
4+
It expects to be executed after the `build` benchmark.
55

66
The following general metrics are collected:
77

88
- `size/libleanshared.so//bytes`
99

10-
The following metrics are collected for the entirety of stdlib:
10+
The following metrics are collected from the entire build process:
1111

12-
- `size/stdlib/.c//files`
13-
- `size/stdlib/.c//lines`
14-
- `size/stdlib/.cpp//files`
15-
- `size/stdlib/.cpp//lines`
16-
- `size/stdlib/.lean//files`
17-
- `size/stdlib/.lean//lines`
18-
- `size/stdlib/.ilean//files`
19-
- `size/stdlib/.ilean//bytes`
20-
- `size/stdlib/.olean//files`
21-
- `size/stdlib/.olean//bytes`
22-
- `size/stdlib/.olean.server//files`
23-
- `size/stdlib/.olean.server//bytes`
24-
- `size/stdlib/.olean.private//files`
25-
- `size/stdlib/.olean.private//bytes`
26-
- `size/stdlib/.ir//files`
27-
- `size/stdlib/.ir//bytes`
12+
- `size/all/.c//files`
13+
- `size/all/.c//lines`
14+
- `size/all/.cpp//files`
15+
- `size/all/.cpp//lines`
16+
- `size/all/.lean//files`
17+
- `size/all/.lean//lines`
18+
- `size/all/.ilean//files`
19+
- `size/all/.ilean//bytes`
20+
- `size/all/.olean//files`
21+
- `size/all/.olean//bytes`
22+
- `size/all/.olean.server//files`
23+
- `size/all/.olean.server//bytes`
24+
- `size/all/.olean.private//files`
25+
- `size/all/.olean.private//bytes`
26+
- `size/all/.ir//files`
27+
- `size/all/.ir//bytes`
2828

2929
The following metrics are collected only for the `Init` library.
3030

‎tests/bench-radar/size/run‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -47,14 +47,14 @@ if __name__ == "__main__":
4747
)
4848

4949
# Stdlib
50-
measure_lines("size/stdlib/.c", STAGE3_TEMP.glob("**/*.c"))
51-
measure_bytes("size/stdlib/.ir", STAGE3_LEAN.glob("**/*.ir"))
52-
measure_lines("size/stdlib/.cpp", SRC.glob("**/*.cpp"))
53-
measure_lines("size/stdlib/.lean", SRC.glob("**/*.lean"))
54-
measure_bytes("size/stdlib/.ilean", STAGE3_LEAN.glob("**/*.ilean"))
55-
measure_bytes("size/stdlib/.olean", STAGE3_LEAN.glob("**/*.olean"))
56-
measure_bytes("size/stdlib/.olean.server", STAGE3_LEAN.glob("**/*.olean.server"))
57-
measure_bytes("size/stdlib/.olean.private", STAGE3_LEAN.glob("**/*.olean.private"))
50+
measure_lines("size/all/.c", STAGE3_TEMP.glob("**/*.c"))
51+
measure_bytes("size/all/.ir", STAGE3_LEAN.glob("**/*.ir"))
52+
measure_lines("size/all/.cpp", SRC.glob("**/*.cpp"))
53+
measure_lines("size/all/.lean", SRC.glob("**/*.lean"))
54+
measure_bytes("size/all/.ilean", STAGE3_LEAN.glob("**/*.ilean"))
55+
measure_bytes("size/all/.olean", STAGE3_LEAN.glob("**/*.olean"))
56+
measure_bytes("size/all/.olean.server", STAGE3_LEAN.glob("**/*.olean.server"))
57+
measure_bytes("size/all/.olean.private", STAGE3_LEAN.glob("**/*.olean.private"))
5858

5959
# Init
6060
measure_bytes("size/init/.olean", STAGE3_LEAN.glob("Init/**/*.olean"))

0 commit comments

Comments
 (0)