From 6b55c0c083df69588c4273314274664eaecf9c84 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 4 May 2026 18:51:30 +0000
Subject: [PATCH 01/19] chore: use the lean-llvm LLVM for benchmarking

---
 tests/bench_build.sh | 19 ++++++++++++++++++-
 tests/bench_other.sh | 19 ++++++++++++++++++-
 2 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index c91fb109acd8..bf0286450c0c 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -4,7 +4,24 @@
 # The radar environment variables must be provided.
 # See also the https://github.com/leanprover/radar readme.
 
-cmake --preset release -DWFAIL=OFF
+LLVM_RELEASE=19.1.2
+LLVM_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
+LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
+
+if [ ! -f "$LLVM_TARBALL" ]; then
+    mkdir -p "$RADAR_CACHE/llvm"
+    wget -O "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
+    mkdir -p "$LLVM_DIR"
+    tar -I zstd -xf "$LLVM_TARBALL" -C "$LLVM_DIR"
+fi
+
+export LD_LIBRARY_PATH="$LLVM_DIR/lib/x86_64-unknown-linux-gnu:$LD_LIBRARY_PATH"
+export PATH="$LLVM_DIR/bin:$PATH"
+
+cmake --preset release -DWFAIL=OFF \
+  -DCMAKE_C_COMPILER="$LLVM_DIR/bin/clang" \
+  -DCMAKE_CXX_COMPILER="$LLVM_DIR/bin/clang++" \
+  -DLLVM_CONFIG="$LLVM_DIR/bin/llvm-config"
 make -C build/release -j"$(nproc)" bench-part1
 mv tests/part1.measurements.jsonl "$RADAR_OUT"
 
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index 18d23d0019a2..7241eb09812b 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -4,6 +4,23 @@
 # The radar environment variables must be provided.
 # See also the https://github.com/leanprover/radar readme.
 
-cmake --preset release -DWFAIL=OFF
+LLVM_RELEASE=19.1.2
+LLVM_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
+LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
+
+if [ ! -f "$LLVM_TARBALL" ]; then
+    mkdir -p "$RADAR_CACHE/llvm"
+    wget -O "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
+    mkdir -p "$LLVM_DIR"
+    tar -I zstd -xf "$LLVM_TARBALL" -C "$LLVM_DIR"
+fi
+
+export LD_LIBRARY_PATH="$LLVM_DIR/lib/x86_64-unknown-linux-gnu:$LD_LIBRARY_PATH"
+export PATH="$LLVM_DIR/bin:$PATH"
+
+cmake --preset release -DWFAIL=OFF \
+  -DCMAKE_C_COMPILER="$LLVM_DIR/bin/clang" \
+  -DCMAKE_CXX_COMPILER="$LLVM_DIR/bin/clang++" \
+  -DLLVM_CONFIG="$LLVM_DIR/bin/llvm-config"
 make -C build/release -j"$(nproc)" bench-part2
 mv tests/part2.measurements.jsonl "$RADAR_OUT"

From d05a736a7ca329146f06a6a67de514b441d47aec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 4 May 2026 19:01:30 +0000
Subject: [PATCH 02/19] curl?

---
 tests/bench_build.sh | 2 +-
 tests/bench_other.sh | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index bf0286450c0c..e38015a0c0bb 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -10,7 +10,7 @@ LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
 if [ ! -f "$LLVM_TARBALL" ]; then
     mkdir -p "$RADAR_CACHE/llvm"
-    wget -O "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
+    curl -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
     mkdir -p "$LLVM_DIR"
     tar -I zstd -xf "$LLVM_TARBALL" -C "$LLVM_DIR"
 fi
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index 7241eb09812b..842d5b186b46 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -10,7 +10,7 @@ LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
 if [ ! -f "$LLVM_TARBALL" ]; then
     mkdir -p "$RADAR_CACHE/llvm"
-    wget -O "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
+    curl -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
     mkdir -p "$LLVM_DIR"
     tar -I zstd -xf "$LLVM_TARBALL" -C "$LLVM_DIR"
 fi

From 1064980f695deed35c98be08a6057f8792e24b93 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 4 May 2026 19:09:31 +0000
Subject: [PATCH 03/19] curl follow?

---
 tests/bench_build.sh | 9 +++++----
 tests/bench_other.sh | 9 +++++----
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index e38015a0c0bb..3df9d6176d8e 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -5,14 +5,15 @@
 # See also the https://github.com/leanprover/radar readme.
 
 LLVM_RELEASE=19.1.2
-LLVM_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
+LLVM_BASE_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
+LLVM_DIR = "$LLVM_DIR/lean-llvm"
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
 if [ ! -f "$LLVM_TARBALL" ]; then
     mkdir -p "$RADAR_CACHE/llvm"
-    curl -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
-    mkdir -p "$LLVM_DIR"
-    tar -I zstd -xf "$LLVM_TARBALL" -C "$LLVM_DIR"
+    curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
+    mkdir -p "$LLVM_BASE_DIR"
+    tar -I zstd -xf "$LLVM_TARBALL" -C "$LLVM_BASE_DIR"
 fi
 
 export LD_LIBRARY_PATH="$LLVM_DIR/lib/x86_64-unknown-linux-gnu:$LD_LIBRARY_PATH"
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index 842d5b186b46..0bba617dd195 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -5,14 +5,15 @@
 # See also the https://github.com/leanprover/radar readme.
 
 LLVM_RELEASE=19.1.2
-LLVM_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
+LLVM_BASE_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
+LLVM_DIR = "$LLVM_DIR/lean-llvm"
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
 if [ ! -f "$LLVM_TARBALL" ]; then
     mkdir -p "$RADAR_CACHE/llvm"
-    curl -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
-    mkdir -p "$LLVM_DIR"
-    tar -I zstd -xf "$LLVM_TARBALL" -C "$LLVM_DIR"
+    curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
+    mkdir -p "$LLVM_BASE_DIR"
+    tar -I zstd -xf "$LLVM_TARBALL" -C "$LLVM_BASE_DIR"
 fi
 
 export LD_LIBRARY_PATH="$LLVM_DIR/lib/x86_64-unknown-linux-gnu:$LD_LIBRARY_PATH"

From e3c7028da7a154e6e2838e0736af00480a24f3f9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 4 May 2026 19:13:09 +0000
Subject: [PATCH 04/19] aahhh

---
 tests/bench_build.sh | 2 +-
 tests/bench_other.sh | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index 3df9d6176d8e..4f8f7be270b8 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -6,7 +6,7 @@
 
 LLVM_RELEASE=19.1.2
 LLVM_BASE_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
-LLVM_DIR = "$LLVM_DIR/lean-llvm"
+LLVM_DIR = "$LLVM_BASE_DIR/lean-llvm"
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
 if [ ! -f "$LLVM_TARBALL" ]; then
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index 0bba617dd195..ee0842d03b53 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -6,7 +6,7 @@
 
 LLVM_RELEASE=19.1.2
 LLVM_BASE_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
-LLVM_DIR = "$LLVM_DIR/lean-llvm"
+LLVM_DIR = "$LLVM_BASE_DIR/lean-llvm"
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
 if [ ! -f "$LLVM_TARBALL" ]; then

From e00dfb7eb38be46b0acb911babb1619f27b7dfc6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 4 May 2026 19:14:24 +0000
Subject: [PATCH 05/19] ahhhhhhh

---
 tests/bench_other.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index ee0842d03b53..d444805d5111 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -6,7 +6,7 @@
 
 LLVM_RELEASE=19.1.2
 LLVM_BASE_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
-LLVM_DIR = "$LLVM_BASE_DIR/lean-llvm"
+LLVM_DIR="$LLVM_BASE_DIR/lean-llvm"
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
 if [ ! -f "$LLVM_TARBALL" ]; then

From 598542156732b183995105f0a159d026c091fc89 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 4 May 2026 19:16:17 +0000
Subject: [PATCH 06/19] ahhhhhhhhhhhhhhhhh

---
 tests/bench_build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index 4f8f7be270b8..fdbb3b4d95a4 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -6,7 +6,7 @@
 
 LLVM_RELEASE=19.1.2
 LLVM_BASE_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
-LLVM_DIR = "$LLVM_BASE_DIR/lean-llvm"
+LLVM_DIR="$LLVM_BASE_DIR/lean-llvm"
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
 if [ ! -f "$LLVM_TARBALL" ]; then

From 3cdbd3ec02b577f063ca75381a0130cbe8560800 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 4 May 2026 19:26:28 +0000
Subject: [PATCH 07/19] test

---
 tests/bench_build.sh | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index fdbb3b4d95a4..a752329cd6b9 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -19,6 +19,9 @@ fi
 export LD_LIBRARY_PATH="$LLVM_DIR/lib/x86_64-unknown-linux-gnu:$LD_LIBRARY_PATH"
 export PATH="$LLVM_DIR/bin:$PATH"
 
+$LLVM_DIR/clang --help
+$LLVM_DIR/clang++ --help
+
 cmake --preset release -DWFAIL=OFF \
   -DCMAKE_C_COMPILER="$LLVM_DIR/bin/clang" \
   -DCMAKE_CXX_COMPILER="$LLVM_DIR/bin/clang++" \

From e9338c93e00fe73429638b56fbb0c0e9b616b3be Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 4 May 2026 19:27:32 +0000
Subject: [PATCH 08/19] more test

---
 tests/bench_build.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index a752329cd6b9..7038cdac25ce 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -19,8 +19,8 @@ fi
 export LD_LIBRARY_PATH="$LLVM_DIR/lib/x86_64-unknown-linux-gnu:$LD_LIBRARY_PATH"
 export PATH="$LLVM_DIR/bin:$PATH"
 
-$LLVM_DIR/clang --help
-$LLVM_DIR/clang++ --help
+$LLVM_DIR/bin/clang --help
+$LLVM_DIR/bin/clang++ --help
 
 cmake --preset release -DWFAIL=OFF \
   -DCMAKE_C_COMPILER="$LLVM_DIR/bin/clang" \

From cef138932f6859dcd74ccd94ec39827f3fae1dc2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 4 May 2026 19:28:48 +0000
Subject: [PATCH 09/19] clean cache?

---
 tests/bench_build.sh | 2 ++
 tests/bench_other.sh | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index 7038cdac25ce..8c53a3d770b8 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -9,6 +9,8 @@ LLVM_BASE_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
 LLVM_DIR="$LLVM_BASE_DIR/lean-llvm"
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
+rm -rf "$RADAR_CACHE/llvm"
+
 if [ ! -f "$LLVM_TARBALL" ]; then
     mkdir -p "$RADAR_CACHE/llvm"
     curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index d444805d5111..2563c7705280 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -9,6 +9,8 @@ LLVM_BASE_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
 LLVM_DIR="$LLVM_BASE_DIR/lean-llvm"
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
+rm -rf "$RADAR_CACHE/llvm"
+
 if [ ! -f "$LLVM_TARBALL" ]; then
     mkdir -p "$RADAR_CACHE/llvm"
     curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"

From 624e8d3377e6d3c1b4628a87729bc99ddec4e287 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 5 May 2026 09:19:45 +0000
Subject: [PATCH 10/19] build

---
 CMakeLists.txt       | 3 ++-
 src/CMakeLists.txt   | 1 +
 src/lakefile.toml.in | 2 ++
 3 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 2af38729071b..6aa7bf15479d 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -52,7 +52,8 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
       # Use same platform flags as for Lean executables, in particular from `prepare-llvm-linux.sh`,
       # but not Lean-specific `LEAN_EXTRA_CXX_FLAGS` such as fsanitize.
       set(CADICAL_CXXFLAGS "${CMAKE_CXX_FLAGS}")
-      set(CADICAL_LDFLAGS "-Wl,-rpath=\\$$ORIGIN/../lib")
+      string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}/stage1" CADICAL_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
+      set(CADICAL_LDFLAGS "${CADICAL_INTERNAL_LINKER_FLAGS} -Wl,-rpath=\\$$ORIGIN/../lib")
     endif()
     find_program(CCACHE ccache)
     if(CCACHE)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 372be2b36bc0..b764dc260eaa 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1075,6 +1075,7 @@ string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERN
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
 
 toml_escape("${LEAN_EXTRA_OPTS}" LEAN_EXTRA_OPTS_TOML)
+toml_escape("${LEANC_INTERNAL_FLAGS} ${LEANC_INTERNAL_LINKER_FLAGS}" LEAN_MORE_LEANC_ARGS_TOML)
 
 if(CMAKE_BUILD_TYPE MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
   set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")
diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in
index c0faf4fa46d2..21e59a9e4a14 100644
--- a/src/lakefile.toml.in
+++ b/src/lakefile.toml.in
@@ -46,6 +46,8 @@ moreLeanArgs = [${LEAN_EXTRA_OPTS_TOML}]
 # Uncomment to limit number of reported errors further in case of overwhelming cmdline output
 #weakLeanArgs = ["-DmaxErrors=1"]
 
+moreLeancArgs = [${LEAN_MORE_LEANC_ARGS_TOML}]
+
 ${LEAN_EXTRA_LAKEFILE_TOML}
 
 [[lean_lib]]

From ca66d58e0f1fc2d64e48187ee3081afdac7efb5e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 5 May 2026 09:21:37 +0000
Subject: [PATCH 11/19] fixup scripts

---
 tests/bench_build.sh | 20 ++++++--------------
 tests/bench_other.sh | 17 ++++++-----------
 2 files changed, 12 insertions(+), 25 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index 8c53a3d770b8..7603966309f4 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -5,8 +5,6 @@
 # See also the https://github.com/leanprover/radar readme.
 
 LLVM_RELEASE=19.1.2
-LLVM_BASE_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
-LLVM_DIR="$LLVM_BASE_DIR/lean-llvm"
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
 rm -rf "$RADAR_CACHE/llvm"
@@ -14,20 +12,14 @@ rm -rf "$RADAR_CACHE/llvm"
 if [ ! -f "$LLVM_TARBALL" ]; then
     mkdir -p "$RADAR_CACHE/llvm"
     curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
-    mkdir -p "$LLVM_BASE_DIR"
-    tar -I zstd -xf "$LLVM_TARBALL" -C "$LLVM_BASE_DIR"
 fi
 
-export LD_LIBRARY_PATH="$LLVM_DIR/lib/x86_64-unknown-linux-gnu:$LD_LIBRARY_PATH"
-export PATH="$LLVM_DIR/bin:$PATH"
-
-$LLVM_DIR/bin/clang --help
-$LLVM_DIR/bin/clang++ --help
-
-cmake --preset release -DWFAIL=OFF \
-  -DCMAKE_C_COMPILER="$LLVM_DIR/bin/clang" \
-  -DCMAKE_CXX_COMPILER="$LLVM_DIR/bin/clang++" \
-  -DLLVM_CONFIG="$LLVM_DIR/bin/llvm-config"
+mkdir -p build/release
+cd build/release
+eval cmake ../.. \
+    --preset release $(../.././script/prepare-llvm-linux.sh /tmp/llvm/19.1.2.tar.zst) \
+    -DWFAIL=OFF
+cd ../..
 make -C build/release -j"$(nproc)" bench-part1
 mv tests/part1.measurements.jsonl "$RADAR_OUT"
 
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index 2563c7705280..17bb990a606e 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -5,8 +5,6 @@
 # See also the https://github.com/leanprover/radar readme.
 
 LLVM_RELEASE=19.1.2
-LLVM_BASE_DIR="$RADAR_CACHE/llvm/$LLVM_RELEASE"
-LLVM_DIR="$LLVM_BASE_DIR/lean-llvm"
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
 rm -rf "$RADAR_CACHE/llvm"
@@ -14,16 +12,13 @@ rm -rf "$RADAR_CACHE/llvm"
 if [ ! -f "$LLVM_TARBALL" ]; then
     mkdir -p "$RADAR_CACHE/llvm"
     curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
-    mkdir -p "$LLVM_BASE_DIR"
-    tar -I zstd -xf "$LLVM_TARBALL" -C "$LLVM_BASE_DIR"
 fi
 
-export LD_LIBRARY_PATH="$LLVM_DIR/lib/x86_64-unknown-linux-gnu:$LD_LIBRARY_PATH"
-export PATH="$LLVM_DIR/bin:$PATH"
-
-cmake --preset release -DWFAIL=OFF \
-  -DCMAKE_C_COMPILER="$LLVM_DIR/bin/clang" \
-  -DCMAKE_CXX_COMPILER="$LLVM_DIR/bin/clang++" \
-  -DLLVM_CONFIG="$LLVM_DIR/bin/llvm-config"
+mkdir -p build/release
+cd build/release
+eval cmake ../.. \
+    --preset release $(../.././script/prepare-llvm-linux.sh /tmp/llvm/19.1.2.tar.zst) \
+    -DWFAIL=OFF
+cd ../..
 make -C build/release -j"$(nproc)" bench-part2
 mv tests/part2.measurements.jsonl "$RADAR_OUT"

From 10464c516977981a4bf44051016cfc46371cb8ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 5 May 2026 09:35:17 +0000
Subject: [PATCH 12/19] ahhahhhh

---
 tests/bench_build.sh | 2 +-
 tests/bench_other.sh | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index 7603966309f4..b59d6426c657 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -17,7 +17,7 @@ fi
 mkdir -p build/release
 cd build/release
 eval cmake ../.. \
-    --preset release $(../.././script/prepare-llvm-linux.sh /tmp/llvm/19.1.2.tar.zst) \
+    --preset release $(../.././script/prepare-llvm-linux.sh $LLVM_TARBALL) \
     -DWFAIL=OFF
 cd ../..
 make -C build/release -j"$(nproc)" bench-part1
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index 17bb990a606e..92577b398ae8 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -17,7 +17,7 @@ fi
 mkdir -p build/release
 cd build/release
 eval cmake ../.. \
-    --preset release $(../.././script/prepare-llvm-linux.sh /tmp/llvm/19.1.2.tar.zst) \
+    --preset release $(../.././script/prepare-llvm-linux.sh $LLVM_TARBALL) \
     -DWFAIL=OFF
 cd ../..
 make -C build/release -j"$(nproc)" bench-part2

From ef761cd2ef351ffda2d6f79993790f3f33e0b997 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 5 May 2026 09:43:07 +0000
Subject: [PATCH 13/19] nix shell

---
 tests/bench_build.sh | 2 ++
 tests/bench_other.sh | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index b59d6426c657..c1f99cf236fd 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -14,6 +14,8 @@ if [ ! -f "$LLVM_TARBALL" ]; then
     curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
 fi
 
+nix develop .#oldGlibc
+
 mkdir -p build/release
 cd build/release
 eval cmake ../.. \
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index 92577b398ae8..f75f4ffe65a3 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -14,6 +14,8 @@ if [ ! -f "$LLVM_TARBALL" ]; then
     curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
 fi
 
+nix develop .#oldGlibc
+
 mkdir -p build/release
 cd build/release
 eval cmake ../.. \

From 22338004f2ec7e59207831dcb881dd76cb386bfe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 5 May 2026 12:09:00 +0000
Subject: [PATCH 14/19] nix shell the second

---
 tests/bench_build.sh | 5 ++---
 tests/bench_other.sh | 5 ++---
 2 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index c1f99cf236fd..2e1259e74d03 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -1,4 +1,5 @@
-#!/usr/bin/env bash
+#!/usr/bin/env nix
+#! nix shell .#oldGlibc --command /usr/bin/env bash
 
 # This script must be called from the repo root.
 # The radar environment variables must be provided.
@@ -14,8 +15,6 @@ if [ ! -f "$LLVM_TARBALL" ]; then
     curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
 fi
 
-nix develop .#oldGlibc
-
 mkdir -p build/release
 cd build/release
 eval cmake ../.. \
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index f75f4ffe65a3..a30fa24d8a86 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -1,4 +1,5 @@
-#!/usr/bin/env bash
+#!/usr/bin/env nix
+#! nix shell .#oldGlibc --command /usr/bin/env bash
 
 # This script must be called from the repo root.
 # The radar environment variables must be provided.
@@ -14,8 +15,6 @@ if [ ! -f "$LLVM_TARBALL" ]; then
     curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
 fi
 
-nix develop .#oldGlibc
-
 mkdir -p build/release
 cd build/release
 eval cmake ../.. \

From 11e567728d463b7131a0707daaae02928057742b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 5 May 2026 12:09:56 +0000
Subject: [PATCH 15/19] develop

---
 tests/bench_build.sh | 2 +-
 tests/bench_other.sh | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index 2e1259e74d03..65534d0c4956 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -1,5 +1,5 @@
 #!/usr/bin/env nix
-#! nix shell .#oldGlibc --command /usr/bin/env bash
+#! nix develop .#oldGlibc --command /usr/bin/env bash
 
 # This script must be called from the repo root.
 # The radar environment variables must be provided.
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index a30fa24d8a86..f8f28285b688 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -1,5 +1,5 @@
 #!/usr/bin/env nix
-#! nix shell .#oldGlibc --command /usr/bin/env bash
+#! nix develop .#oldGlibc --command /usr/bin/env bash
 
 # This script must be called from the repo root.
 # The radar environment variables must be provided.

From c2da7b22ff3f755860e0935d30ce4ccf9a96f04d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 5 May 2026 13:12:09 +0000
Subject: [PATCH 16/19] punkt

---
 tests/bench_build.sh | 2 +-
 tests/bench_other.sh | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index 65534d0c4956..3ae81daaeb86 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -1,5 +1,5 @@
 #!/usr/bin/env nix
-#! nix develop .#oldGlibc --command /usr/bin/env bash
+#! nix develop ..#oldGlibc --command /usr/bin/env bash
 
 # This script must be called from the repo root.
 # The radar environment variables must be provided.
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index f8f28285b688..050139478e71 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -1,5 +1,5 @@
 #!/usr/bin/env nix
-#! nix develop .#oldGlibc --command /usr/bin/env bash
+#! nix develop ..#oldGlibc --command /usr/bin/env bash
 
 # This script must be called from the repo root.
 # The radar environment variables must be provided.

From 5f3abf08f5eef5ee1f005721faac9753852b5691 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 5 May 2026 13:32:57 +0000
Subject: [PATCH 17/19] copy copy copy

---
 tests/bench_build.sh | 2 ++
 tests/bench_other.sh | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index 3ae81daaeb86..e514b8f1897b 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -20,6 +20,8 @@ cd build/release
 eval cmake ../.. \
     --preset release $(../.././script/prepare-llvm-linux.sh $LLVM_TARBALL) \
     -DWFAIL=OFF
+cp -r stage1 stage2
+cp -r stage1 stage3
 cd ../..
 make -C build/release -j"$(nproc)" bench-part1
 mv tests/part1.measurements.jsonl "$RADAR_OUT"
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index 050139478e71..f6646538c756 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -20,6 +20,8 @@ cd build/release
 eval cmake ../.. \
     --preset release $(../.././script/prepare-llvm-linux.sh $LLVM_TARBALL) \
     -DWFAIL=OFF
+cp -r stage1 stage2
+cp -r stage1 stage3
 cd ../..
 make -C build/release -j"$(nproc)" bench-part2
 mv tests/part2.measurements.jsonl "$RADAR_OUT"

From 84acdcf6a82818b2b9c7a83ffcb1f57dbd090b75 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 5 May 2026 13:41:20 +0000
Subject: [PATCH 18/19] help

---
 tests/bench_build.sh | 4 +++-
 tests/bench_other.sh | 4 +++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index e514b8f1897b..a5b455007094 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -18,9 +18,11 @@ fi
 mkdir -p build/release
 cd build/release
 eval cmake ../.. \
-    --preset release $(../.././script/prepare-llvm-linux.sh $LLVM_TARBALL) \
+    --preset release $(../../script/prepare-llvm-linux.sh $LLVM_TARBALL) \
     -DWFAIL=OFF
+rm -rf stage2
 cp -r stage1 stage2
+rm -rf stage3
 cp -r stage1 stage3
 cd ../..
 make -C build/release -j"$(nproc)" bench-part1
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index f6646538c756..811001fc7d4c 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -18,9 +18,11 @@ fi
 mkdir -p build/release
 cd build/release
 eval cmake ../.. \
-    --preset release $(../.././script/prepare-llvm-linux.sh $LLVM_TARBALL) \
+    --preset release $(../../script/prepare-llvm-linux.sh $LLVM_TARBALL) \
     -DWFAIL=OFF
+rm -rf stage2
 cp -r stage1 stage2
+rm -rf stage3
 cp -r stage1 stage3
 cd ../..
 make -C build/release -j"$(nproc)" bench-part2

From f8849c8af18b691ab1c54f156dce0d1cd5f4e1b0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 5 May 2026 14:17:33 +0000
Subject: [PATCH 19/19] do not delete the cache every time

---
 tests/bench_build.sh | 2 --
 tests/bench_other.sh | 2 --
 2 files changed, 4 deletions(-)

diff --git a/tests/bench_build.sh b/tests/bench_build.sh
index a5b455007094..749cc9682ceb 100755
--- a/tests/bench_build.sh
+++ b/tests/bench_build.sh
@@ -8,8 +8,6 @@
 LLVM_RELEASE=19.1.2
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
-rm -rf "$RADAR_CACHE/llvm"
-
 if [ ! -f "$LLVM_TARBALL" ]; then
     mkdir -p "$RADAR_CACHE/llvm"
     curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"
diff --git a/tests/bench_other.sh b/tests/bench_other.sh
index 811001fc7d4c..98bae3ff685a 100755
--- a/tests/bench_other.sh
+++ b/tests/bench_other.sh
@@ -8,8 +8,6 @@
 LLVM_RELEASE=19.1.2
 LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst"
 
-rm -rf "$RADAR_CACHE/llvm"
-
 if [ ! -f "$LLVM_TARBALL" ]; then
     mkdir -p "$RADAR_CACHE/llvm"
     curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst"