Skip to content

Commit 38fbc41

Browse files
fix: use lake test if test.sh is missing from lean4checker (#160)
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 Co-authored-by: Austin Letson <austin.letson@axiomatic-ai.com>
1 parent 1831970 commit 38fbc41

1 file changed

Lines changed: 5 additions & 1 deletion

File tree

scripts/run_leanchecker.sh

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,11 @@ git checkout "$toolchain_version"
3232
cp ../lean-toolchain .
3333

3434
lake build
35-
./test.sh
35+
if [ -f ./test.sh ]; then
36+
./test.sh
37+
else
38+
lake test
39+
fi
3640
)
3741

3842
echo "Running external lean4checker"

0 commit comments

Comments
 (0)