diff --git a/tests/bench/build/run_bench.sh b/tests/bench/build/run_bench.sh index 4388163a91..5c3045e107 100644 --- a/tests/bench/build/run_bench.sh +++ b/tests/bench/build/run_bench.sh @@ -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"