From 9322808685e706fcd135d99d1c2be3670536c169 Mon Sep 17 00:00:00 2001
From: Austin Letson <austin.letson@axiomatic-ai.com>
Date: Mon, 20 Apr 2026 12:10:58 +0200
Subject: [PATCH] fix: use `lake test` if `test.sh` is missing from
 lean4checker

test.sh was removed in lean4check 4.27.0

note, Lean version >= 4.28.x will use the built in leanchecker so this
only affects 4.27.0
---
 scripts/run_leanchecker.sh | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/scripts/run_leanchecker.sh b/scripts/run_leanchecker.sh
index f201c1d..04006f6 100755
--- a/scripts/run_leanchecker.sh
+++ b/scripts/run_leanchecker.sh
@@ -32,7 +32,11 @@ git checkout "$toolchain_version"
 cp ../lean-toolchain .
 
 lake build
-./test.sh
+if [ -f ./test.sh ]; then
+  ./test.sh
+else
+  lake test
+fi
 )
 
 echo "Running external lean4checker"