max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add radar-based bench suite for stdlib (#11264)

Browse source 
This PR adds a new [radar]-based [temci]-less bench suite that replaces
the `stdlib` benchmarks from the old suite and also measures per-module
instruction counts. All other benchmarks from the old suite are
unaffected.

The readme at `tests/bench-radar/README.md` explains in more detail how
the bench suite is structured and how it works. The readmes in the
benchmark subdirectories explain what each benchmark does and which
metrics it collects.

All metrics except `stdlib//max dynamic symbols` were ported to the new
suite, though most have been renamed.

[radar]: https://github.com/leanprover/radar
[temci]: https://github.com/parttimenerd/temci
This commit is contained in:
Garmelon 2025-11-25 13:59:30 +01:00 • committed by GitHub
parent 9338aabed9
commit debafca7e1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
14 changed files with 656 additions and 165 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

96
script/bench.sh
View file

@ -1,96 +0,0 @@
#!/usr/bin/env bash
set -euxo pipefail
cmake --preset release 1>&2
# We benchmark against stage2/bin to test new optimizations.
timeout -s KILL 1h time make -C build/release -j$(nproc) stage3 1>&2
export PATH=$PWD/build/release/stage2/bin:$PATH
# The extra opts used to be passed to the Makefile during benchmarking only but with Lake it is
# easier to configure them statically.
cmake -B build/release/stage3 -S src -DLEAN_EXTRA_LAKEFILE_TOML='weakLeanArgs=["-Dprofiler=true", "-Dprofiler.threshold=9999999", "--stats"]' 1>&2
(
cd tests/bench
timeout -s KILL 1h time temci exec --config speedcenter.yaml --in speedcenter.exec.velcom.yaml 1>&2
temci report run_output.yaml --reporter codespeed2
)
if [ -d .git ]; then
DIR="$(git rev-parse @)"
BASE_URL="https://speed.lean-lang.org/lean4-out/$DIR"
{
cat <<'EOF'
<!DOCTYPE html>
<html>
<head>
<meta charset="UTF-8">
<title>Lakeprof Report</title>
</head>
<h1>Lakeprof Report</h1>
<button type="button" id="btn_fetch">View build trace in Perfetto</button>
<script type="text/javascript">
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);
}
EOF
cat <<EOF
btnFetch.onclick = () => fetchAndOpen("$BASE_URL/lakeprof.trace_event");
</script>
EOF
echo "<pre><code>"
(cd src; lakeprof report -prc)
echo "</code></pre>"
echo "</body></html>"
} | tee index.html
curl -T index.html $BASE_URL/index.html
curl -T src/lakeprof.log $BASE_URL/lakeprof.log
curl -T src/lakeprof.trace_event $BASE_URL/lakeprof.trace_event
fi

25
tests/bench-radar/README.md Normal file
View file

@ -0,0 +1,25 @@
# Lean 4 benchmark suite
This directory contains the new Lean 4 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/lean4).
To run the entire benchmark suite, execute the script called `run`.
Benchmarks are organized into subdirectories.
Each benchmark directory must contain a script called `run` that executes the benchmark,
as well as any additional benchmark-specific required files.
Ideally, each benchmark directory also contains a `README.md` explaining the benchmark.
A benchmark's `run` script emits measurements as JSON objects
as defined by radar's [bench repo specification](https://github.com/leanprover/radar?tab=readme-ov-file#bench-repo-specification).
It can emit the measurement in one of two ways:
1. Append the measurement to the file `radar.jsonl` in the repository root.
This file follows the [JSON Lines](https://jsonlines.org/) format.
2. Print a line on stdout or stderr containing `radar::measurement=` followed by the measurement.
After the measurement, only whitespace is allowed.
All scripts related to the new benchmark suite are contained in this directory.
The files at `tests/bench` belong to the old suite.
The `*.py` symlinks are only for convenience when editing the python scripts in VSCode,
so the python extensions (in particular pyrefly) treat it as a python file.

28
tests/bench-radar/build/README.md Normal file
View file

@ -0,0 +1,28 @@
# The `build` benchmark
This benchmark executes a complete build of the stage3 stdlib
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.

74
tests/bench-radar/build/lakeprof_report_template.html Normal file
View file

@ -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>

44
tests/bench-radar/build/lakeprof_report_upload.py Normal file
View file

@ -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/lean4-out/{sha}"
report = run_stdout("lakeprof", "report", "-prc", cwd="src")
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", "src/lakeprof.log", f"{base_url}/lakeprof.log")
run("curl", "-T", "src/lakeprof.trace_event", f"{base_url}/lakeprof.trace_event")
if __name__ == "__main__":
main()

88
tests/bench-radar/build/lean_wrapper.py Executable file
View file

@ -0,0 +1,88 @@
#!/usr/bin/env python3
import argparse
import json
import re
import subprocess
import sys
from pathlib import Path
NAME = "build"
REPO = Path("..")
BENCH = REPO / "tests" / "bench-radar"
STAGE2 = REPO / "build" / "release" / "stage2"
OUT = REPO / "radar.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(OUT, "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}"),
*("-o", f"{OUT}"),
*("-m", "instructions"),
"--",
*(f"{STAGE2}/bin/lean.wrapped", "--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:
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()

40
tests/bench-radar/build/run Executable file
View file

@ -0,0 +1,40 @@
#!/usr/bin/env bash
set -euxo pipefail
BENCH="tests/bench-radar"
STAGE2="build/release/stage2"
STAGE3="build/release/stage3"
# Build previous stages and warm up stage3
cmake --preset release
timeout -s KILL 1h time make -C build/release -j"$(nproc)" stage3
find "$STAGE3" -name "*.olean" -delete
# Use stage2 binaries from now on
#
# Otherwise, tools like lakeprof use the global lean installation,
# which may not exist or be the right version.
export PATH="$PWD/$STAGE2/bin:$PATH"
# Substitute our own wrapper script
mv "$STAGE2/bin/lean" "$STAGE2/bin/lean.wrapped"
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 -- \
lakeprof record -- \
make -C build/release -j"$(nproc)" stage3
# Analyze lakeprof data
mv lakeprof.log src
pushd src
lakeprof report -pj | jq -r '"radar::measurement=\({metric: "build/lakeprof/longest build path//wall-clock", value: .[-1][2], unit: "s"})"'
lakeprof report -rj | jq -r '"radar::measurement=\({metric: "build/lakeprof/longest rebuild path//wall-clock", value: .[-1][2], unit: "s"})"'
popd
# 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

149
tests/bench-radar/measure.py Executable file
View file

@ -0,0 +1,149 @@
#!/usr/bin/env python3
# Wrap around a command with perf and rusage to measure some metrics. Output the
# results either on stdout or to a file, according to the radar bench script
# specification.
import argparse
import json
import os
import resource
import subprocess
import sys
import tempfile
from dataclasses import dataclass
from pathlib import Path
@dataclass
class PerfMetric:
event: str
factor: float = 1
unit: str | None = None
@dataclass
class RusageMetric:
name: str
factor: float = 1
unit: str | None = None
PERF_UNITS = {
"msec": 1e-3,
"ns": 1e-9,
}
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"),
}
RUSAGE_METRICS = {
"maxrss": RusageMetric("ru_maxrss", factor=1000, unit="b"), # KiB on linux
}
def measure_perf(cmd: list[str], events: list[str]) -> dict[str, tuple[float, str]]:
with tempfile.NamedTemporaryFile() as tmp:
cmd = [
*["perf", "stat", "-j", "-o", tmp.name],
*[arg for event in events for arg in ["-e", event]],
*["--", *cmd],
]
# Execute command
env = os.environ.copy()
env["LC_ALL"] = "C" # or else perf may output syntactically invalid json
result = subprocess.run(cmd, env=env)
if result.returncode != 0:
sys.exit(result.returncode)
# Collect results
perf = {}
for line in tmp:
data = json.loads(line)
if "event" in data and "counter-value" in data:
perf[data["event"]] = float(data["counter-value"]), data["unit"]
return perf
@dataclass
class Result:
category: str
value: float
unit: str | None
def fmt(self, topic: str) -> str:
metric = f"{topic}//{self.category}"
if self.unit is None:
return json.dumps({"metric": metric, "value": self.value})
return json.dumps({"metric": metric, "value": self.value, "unit": self.unit})
def measure(cmd: list[str], metrics: list[str]) -> list[Result]:
# Check args
unknown_metrics = []
for metric in metrics:
if metric not in RUSAGE_METRICS and metric not in PERF_METRICS:
unknown_metrics.append(metric)
if unknown_metrics:
raise Exception(f"unknown metrics: {', '.join(unknown_metrics)}")
# Prepare perf events
events: list[str] = []
for metric in metrics:
if info := PERF_METRICS.get(metric):
events.append(info.event)
# Measure
perf = measure_perf(cmd, events)
rusage = resource.getrusage(resource.RUSAGE_CHILDREN)
# Extract results
results = []
for metric in metrics:
if info := PERF_METRICS.get(metric):
if info.event in perf:
value, unit = perf[info.event]
else:
# Without the corresponding permissions,
# we only get access to the userspace versions of the counters.
value, unit = perf[f"{info.event}:u"]
value *= PERF_UNITS.get(unit, info.factor)
results.append(Result(metric, value, info.unit))
if info := RUSAGE_METRICS.get(metric):
value = getattr(rusage, info.name) * info.factor
results.append(Result(metric, value, info.unit))
return results
if __name__ == "__main__":
parser = argparse.ArgumentParser()
parser.add_argument("-t", "--topic", action="append", default=[])
parser.add_argument("-m", "--metric", action="append", default=[])
parser.add_argument("-o", "--output", type=Path)
parser.add_argument("cmd", nargs="*")
args = parser.parse_args()
topics: list[str] = args.topic
metrics: list[str] = args.metric
output: Path | None = args.output
cmd: list[str] = args.cmd
results = measure(cmd, metrics)
if output:
with open(output, "a+") as f:
for result in results:
for topic in topics:
f.write(f"{result.fmt(topic)}\n")
else:
for result in results:
for topic in topics:
print(f"radar::measurement={result.fmt(topic)}")

97
tests/bench-radar/repeatedly.py Executable file
View file

@ -0,0 +1,97 @@
#!/usr/bin/env python3
# Repeatedly run a command that outputs radar measurements on stdout or stderr.
# Average the results and re-emit them.
import argparse
import json
import subprocess
import sys
from dataclasses import dataclass
from pathlib import Path
OUTPUT_PREFIX = "radar::measurement="
@dataclass
class Measurement:
metric: str
value: float
unit: str | None
def fmt(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}
)
def parse_measurement(line: str) -> Measurement | None:
start = line.find(OUTPUT_PREFIX)
if start < 0:
return
data = json.loads(line[start + len(OUTPUT_PREFIX) :].strip())
return Measurement(data["metric"], data["value"], data.get("unit"))
def run_once(cmd: list[str], quiet: bool) -> list[Measurement]:
proc = subprocess.run(cmd, capture_output=True, encoding="utf-8")
if proc.returncode != 0:
print(proc.stdout, end="", file=sys.stdout)
print(proc.stderr, end="", file=sys.stderr)
sys.exit(proc.returncode)
# We must not print the lines containing the measurements, else radar will collect them.
measurements = []
for line in proc.stdout.splitlines():
if m := parse_measurement(line):
measurements.append(m)
elif not quiet:
print(line, file=sys.stdout)
for line in proc.stderr.splitlines():
if m := parse_measurement(line):
measurements.append(m)
elif not quiet:
print(line, file=sys.stderr)
return measurements
def repeatedly(cmd: list[str], iterations: int, quiet: bool) -> list[Measurement]:
totals: dict[str, Measurement] = {}
for i in range(iterations):
for measurement in run_once(cmd, quiet):
if existing := totals.get(measurement.metric):
measurement.value += existing.value
totals[measurement.metric] = measurement
for measurement in totals.values():
measurement.value /= iterations
return list(totals.values())
if __name__ == "__main__":
parser = argparse.ArgumentParser()
parser.add_argument("-n", "--iterations", type=int, default=5)
parser.add_argument("-q", "--quiet", action="store_true")
parser.add_argument("-o", "--output", type=Path)
parser.add_argument("cmd", nargs="*")
args = parser.parse_args()
iterations: int = args.iterations
quiet: bool = args.quiet
output: Path | None = args.output
cmd: list[str] = args.cmd
measurements = repeatedly(cmd, iterations, quiet)
if output:
with open(output, "a+") as f:
for result in measurements:
f.write(f"{result.fmt()}\n")
else:
for result in measurements:
print(f"{OUTPUT_PREFIX}{result.fmt()}")

8
tests/bench-radar/run_build Executable file
View file

@ -0,0 +1,8 @@
#!/usr/bin/env bash
set -euo pipefail
echo "Running benchmark: build"
tests/bench-radar/build/run
echo "Running benchmark: size"
tests/bench-radar/size/run

36
tests/bench-radar/size/README.md Normal file
View file

@ -0,0 +1,36 @@
# 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.
The following general metrics are collected:
- `size/libleanshared.so//bytes`
The following metrics are collected for the entirety of stdlib:
- `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`
The following metrics are collected only for the `Init` library.
- `size/init/.olean//files`
- `size/init/.olean//bytes`
- `size/init/.olean.server//files`
- `size/init/.olean.server//bytes`
- `size/init/.olean.private//files`
- `size/init/.olean.private//bytes`

64
tests/bench-radar/size/run Executable file
View file

@ -0,0 +1,64 @@
#!/usr/bin/env python3
import json
from pathlib import Path
from typing import Iterable
SRC = Path("src")
STAGE3 = Path("build/release/stage3")
STAGE3_TEMP = STAGE3 / "lib" / "temp"
STAGE3_LEAN = STAGE3 / "lib" / "lean"
def print_result(metric: str, value: float, unit: str | None = None) -> None:
data = {"metric": metric, "value": value}
if unit is not None:
data["unit"] = unit
print(f"radar::measurement={json.dumps(data)}")
def measure_bytes(topic: str, paths: Iterable[Path], files: bool = True) -> None:
amount = 0
total = 0
for path in paths:
amount += 1
total += path.stat().st_size
if files:
print_result(f"{topic}//files", amount)
print_result(f"{topic}//bytes", total, "B")
def measure_lines(topic: str, paths: Iterable[Path]) -> None:
amount = 0
total = 0
for path in paths:
amount += 1
with open(path) as f:
total += sum(1 for _ in f)
print_result(f"{topic}//files", amount)
print_result(f"{topic}//lines", total)
if __name__ == "__main__":
measure_bytes(
"size/libleanshared.so",
[STAGE3_LEAN / "libleanshared.so"],
files=False,
)
# 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"))
# Init
measure_bytes("size/init/.olean", STAGE3_LEAN.glob("Init/**/*.olean"))
measure_bytes("size/init/.olean.server", STAGE3_LEAN.glob("Init/**/*.olean.server"))
measure_bytes(
"size/init/.olean.private", STAGE3_LEAN.glob("Init/**/*.olean.private")
)

1
tests/bench-radar/size/run.py Symbolic link
View file

@ -0,0 +1 @@
run

71
tests/bench/speedcenter.exec.velcom.yaml
View file

@ -1,6 +1,6 @@
- attributes:
description: stdlib
tags: [stdlib]
description: Init.Prelude async
tags: [other]
time: &time
#runner: time
# alternative config: use `perf stat` for extended properties
@ -15,73 +15,6 @@
"branch-misses",
]
rusage_properties: ["maxrss"]
run_config:
<<: *time
cwd: ../../src
cmd: |
set -euxo pipefail
bash -c 'set -eo pipefail; find ${BUILD:-../build/release}/stage3 -name "*.olean" -delete; lakeprof record make -C ${BUILD:-../build/release}/stage3 -j$(nproc) 2>&1 | ../tests/bench/accumulate_profile.py'
lakeprof report -p | awk '{if ($3) cum = $3} END {print "longest build path: " cum}'
lakeprof report -r | awk '{if ($3) cum = $3} END {print "longest rebuild path: " cum}'
max_runs: 2
parse_output: true
# initialize stage3 cmake + warmup
build_config:
cmd: |
bash -c 'make -C ${BUILD:-../build/release} stage3 -j$(nproc)'
- attributes:
description: stdlib size
tags: [stdlib]
run_config:
cwd: ../../
cmd: |
set -euxo pipefail
echo -n 'lines: '
find src -name '*.lean' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'bytes .olean: '
find ${BUILD:-build/release}/stage3/lib/lean -name '*.olean' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'bytes .olean.server: '
find ${BUILD:-build/release}/stage3/lib/lean -name '*.olean.server' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'bytes .olean.private: '
find ${BUILD:-build/release}/stage3/lib/lean -name '*.olean.private' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'bytes .ir: '
find ${BUILD:-build/release}/stage3/lib/lean -name '*.ir' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'lines C: '
find ${BUILD:-build/release}/stage3/lib/temp -name '*.c' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'lines C++: '
find src \( -name '*.h' -o -name '*.cpp' \) -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'max dynamic symbols: '
find ${BUILD:-build/release}/stage3/lib/lean -name '*.so' -exec bash -c 'nm --extern-only --defined-only {} | wc -l' \; | sort --reverse --numeric-sort | head -n1
max_runs: 1
runner: output
- attributes:
description: Init size
tags: [stdlib]
run_config:
cwd: ../../
cmd: |
set -euxo pipefail
echo -n 'bytes .olean: '
find ${BUILD:-build/release}/stage3/lib/lean/Init -name '*.olean' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'bytes .olean.server: '
find ${BUILD:-build/release}/stage3/lib/lean/Init -name '*.olean.server' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'bytes .olean.private: '
find ${BUILD:-build/release}/stage3/lib/lean/Init -name '*.olean.private' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
max_runs: 1
runner: output
- attributes:
description: libleanshared.so
tags: [stdlib]
run_config:
cmd: |
set -eu
echo -n 'binary size: '
wc -c ${BUILD:-../../build/release}/stage3/lib/lean/libleanshared.so | cut -d' ' -f 1
max_runs: 1
runner: output
- attributes:
description: Init.Prelude async
tags: [other]
run_config:
<<: *time
cwd: ../../src