diff --git a/tests/bench_build.sh b/tests/bench_build.sh new file mode 100755 index 0000000000..c91fb109ac --- /dev/null +++ b/tests/bench_build.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +# This script must be called from the repo root. +# The radar environment variables must be provided. +# See also the https://github.com/leanprover/radar readme. + +cmake --preset release -DWFAIL=OFF +make -C build/release -j"$(nproc)" bench-part1 +mv tests/part1.measurements.jsonl "$RADAR_OUT" + +tests/bench/build/lakeprof_report_upload.py diff --git a/tests/bench_other.sh b/tests/bench_other.sh new file mode 100755 index 0000000000..18d23d0019 --- /dev/null +++ b/tests/bench_other.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +# This script must be called from the repo root. +# The radar environment variables must be provided. +# See also the https://github.com/leanprover/radar readme. + +cmake --preset release -DWFAIL=OFF +make -C build/release -j"$(nproc)" bench-part2 +mv tests/part2.measurements.jsonl "$RADAR_OUT"