From 09600f2ca45b69682c24bdd576458cd4e3259822 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 6 Aug 2025 13:25:45 +0200 Subject: [PATCH] chore: add `lakeprof` benchmarks (#9709) --- script/bench.sh | 84 +++++++++++++++++++++++- tests/bench/accumulate_profile.py | 4 +- tests/bench/speedcenter.exec.velcom.yaml | 10 +-- 3 files changed, 90 insertions(+), 8 deletions(-) diff --git a/script/bench.sh b/script/bench.sh index 8e4d28a98d..8f87427beb 100755 --- a/script/bench.sh +++ b/script/bench.sh @@ -1,9 +1,9 @@ #!/usr/bin/env bash -set -euo pipefail +set -euxo pipefail cmake --preset release -DUSE_LAKE=ON 1>&2 -# We benchmark against stage 2 to test new optimizations. +# 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 @@ -11,6 +11,86 @@ export PATH=$PWD/build/release/stage2/bin:$PATH # 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' + + + + + Lakeprof Report + +

Lakeprof Report

+ + +EOF + echo "
"
+        (cd src; lakeprof report -prc)
+        echo "
" + echo "" + } | 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 diff --git a/tests/bench/accumulate_profile.py b/tests/bench/accumulate_profile.py index 1a21ff947d..9b96bb09d3 100755 --- a/tests/bench/accumulate_profile.py +++ b/tests/bench/accumulate_profile.py @@ -6,8 +6,8 @@ import sys cats = collections.defaultdict(lambda: 0) for line in sys.stdin: - if m := re.match(r"(.+?) ([\d.]+)(m?)s", line) or \ - re.match(r"\s*(number of imported bytes|number of imported consts|number of imported entries):\s+(\d+)()", line): + if m := re.search(r"\t(.+?) ([\d.]+)(m?)s$", line) or \ + re.search(r"(number of imported bytes|number of imported consts|number of imported entries):\s+(\d+)()$", line): cats[m[1].strip()] += float(m[2]) * (1e-3 if m[3] else 1) sys.stderr.write(line) diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 180ffc370f..6ce6efdce6 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -17,16 +17,18 @@ rusage_properties: ["maxrss"] run_config: <<: *time + cwd: ../../src cmd: | - # build only up to make-stdlib so Lake doesn't repeat its output, then finish the build to get - # the executables for further benchmarks, ignore output - bash -c 'set -eo pipefail; find ${BUILD:-../../build/release}/stage3 -name "*.olean" -delete; make LEAN_OPTS="-Dprofiler=true -Dprofiler.threshold=9999999 --stats" -C ${BUILD:-../../build/release}/stage3 --output-sync -j$(nproc) make_stdlib 2>&1 | ./accumulate_profile.py; make -C ${BUILD:-../../build/release}/stage3 -j$(nproc) 1>&2' + 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 stage2 cmake + warmup build_config: cmd: | - bash -c 'make -C ${BUILD:-../../build/release} stage3 -j$(nproc)' + bash -c 'make -C ${BUILD:-../build/release} stage3 -j$(nproc)' - attributes: description: stdlib size tags: [deterministic, fast]