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

chore: move more radar bench logic to this repo (#13633)

Browse source 
These commands were previously executed in the radar-bench-lean4
repository, but are now moved here for additional control.
This commit is contained in:
Garmelon 2026-05-04 20:21:22 +02:00 • committed by GitHub
parent c8191c5e2c
commit 9e5c86eac9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 20 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
tests/bench_build.sh Executable file
View file

@ -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

9
tests/bench_other.sh Executable file
View file

@ -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"