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

chore: build bench: replace warmup with selective build (#13432)

Browse source
This commit is contained in:
Sebastian Ullrich 2026-04-17 10:01:17 +02:00 • committed by GitHub
parent 348ed9b3b0
commit b09d39a766
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
tests/bench/build/run_bench.sh
View file

@ -18,17 +18,6 @@ make -C "$BUILD_ROOT" -j"$(nproc)" "$STAGE_NEXT-configure"
echo
echo ">"
echo "> Warming up $STAGE_NEXT..."
echo ">"
make -C "$BUILD_NEXT" -j"$(nproc)"
find "$BUILD_NEXT/lib" -name "*.olean" -delete
rm -f measurements.jsonl
echo
echo ">"
echo "> Building $STAGE_NEXT..."
@ -38,7 +27,7 @@ LAKE_OVERRIDE_LEAN=true LEAN="$(realpath fake_root/bin/lean)" \
WRAPPER_PREFIX="$(realpath fake_root)" WRAPPER_OUT="$OUT" \
lakeprof record -- \
"$TEST_DIR/measure.py" -t build -d -a -- \
make -C "$BUILD_NEXT" -j"$(nproc)"
make -C "$BUILD_NEXT" -j"$(nproc)" make_stdlib LAKE_EXTRA_ARGS="+Init:olean +Std:olean +Lean:olean +Lake:olean +LakeMain:olean +LeanIR:olean +Leanc:olean +LeanChecker:olean"