From 9e5c86eac9ef4c50ca487106942f61298549aec5 Mon Sep 17 00:00:00 2001
From: Garmelon <joscha@plugh.de>
Date: Mon, 4 May 2026 20:21:22 +0200
Subject: [PATCH] chore: move more radar bench logic to this repo (#13633)

These commands were previously executed in the radar-bench-lean4
repository, but are now moved here for additional control.
---
 tests/bench_build.sh | 11 +++++++++++
 tests/bench_other.sh |  9 +++++++++
 2 files changed, 20 insertions(+)
 create mode 100755 tests/bench_build.sh
 create mode 100755 tests/bench_other.sh

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"