e14230c0f3
Thereby avoiding the overhead of one python interpreter per wrapped lean call during the build benchmarks. |
||
|---|---|---|
| .. | ||
| fake_root/bin | ||
| lakeprof_report_template.html | ||
| lakeprof_report_upload.py | ||
| lean_wrapper.py | ||
| README.md | ||
| run_bench.sh | ||
The build benchmark
This benchmark executes a complete build of the stage3 stdlib from stage2 and collects global and per-module metrics. This is different from most other benchmarks, which benchmark the stage the bench suite is being executed in.
The following metrics are collected by a wrapper around the entire build process:
build//cyclesbuild//instructionsbuild//maxrssbuild//task-clockbuild//wall-clock
The following metrics are collected from leanc --profile and leanc --stat and summed across all modules:
build/profile/<name>//wall-clockbuild/stat/<name>//amountbuild/stat/<name>//bytes
The following metrics are collected from lakeprof report:
build/lakeprof/longest build path//wall-clockbuild/lakeprof/longest rebuild path//wall-clock
The following metrics are collected individually for each module:
build/module/<name>//linesbuild/module/<name>//cyclesbuild/module/<name>//instructionsbuild/module/<name>//bytes .ileanbuild/module/<name>//bytes .oleanbuild/module/<name>//bytes .olean.serverbuild/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.