From a712058ff5ca47f670f6d25ea2b2a7385d9523ae Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Mon, 22 Jul 2024 13:10:09 -0400
Subject: [PATCH] test: modernize scripts

---
 examples/S/test.sh                | 7 ++++---
 examples/my_add/test.sh           | 7 ++++---
 test.sh                           | 8 ++++----
 tests/compile/Test/RawStruct.lean | 2 --
 tests/compile/lakefile.lean       | 6 +++---
 tests/compile/test.sh             | 9 +++++----
 6 files changed, 20 insertions(+), 19 deletions(-)

diff --git a/examples/S/test.sh b/examples/S/test.sh
index 1d6b89a..ee4bac6 100755
--- a/examples/S/test.sh
+++ b/examples/S/test.sh
@@ -1,6 +1,7 @@
 set -ex
 rm -rf .lake
 LAKE=${LAKE:-lake}
-$LAKE build -U
-$LAKE build Test -v
-.lake/build/bin/s
+$LAKE update
+$LAKE build
+$LAKE lean Test.lean
+$LAKE exe s
diff --git a/examples/my_add/test.sh b/examples/my_add/test.sh
index aec6483..a58742b 100755
--- a/examples/my_add/test.sh
+++ b/examples/my_add/test.sh
@@ -1,6 +1,7 @@
 set -ex
 rm -rf .lake
 LAKE=${LAKE:-lake}
-$LAKE build -U
-$LAKE build Test -v
-.lake/build/bin/my_add
+$LAKE update
+$LAKE build
+$LAKE lean Test.lean
+$LAKE exe my_add
diff --git a/test.sh b/test.sh
index afe5345..dbd492b 100755
--- a/test.sh
+++ b/test.sh
@@ -18,11 +18,11 @@ pushd tests/compile
 ./test.sh
 popd
 
-find tests/run -type f -name "*.lean" | xargs -n1 $LAKE env lean
+find tests/run -type f -name "*.lean" | xargs -n1 $LAKE lean
 
 # https://github.com/tydeu/lean4-alloy/issues/6
-$LAKE env lean tests/envIncludePath.lean && false || true
-CPATH=$SCRIPT_DIR/tests $LAKE env lean tests/envIncludePath.lean
-C_INCLUDE_PATH=$SCRIPT_DIR/tests $LAKE env lean tests/envIncludePath.lean
+$LAKE lean tests/envIncludePath.lean && false || true
+CPATH=$SCRIPT_DIR/tests $LAKE lean tests/envIncludePath.lean
+C_INCLUDE_PATH=$SCRIPT_DIR/tests $LAKE lean tests/envIncludePath.lean
 
 echo "all done"
diff --git a/tests/compile/Test/RawStruct.lean b/tests/compile/Test/RawStruct.lean
index 63859b6..b127f3b 100644
--- a/tests/compile/Test/RawStruct.lean
+++ b/tests/compile/Test/RawStruct.lean
@@ -50,11 +50,9 @@ theorem RawY.dataImpl_eq_data (y : RawY) : y.dataImpl = y.data := rfl
 
 attribute [implemented_by RawY.dataImpl] RawY.data
 
-set_option trace.compiler.ir.result true in
 def addRawY (y : RawY) :=
   y.n + y.m
 
-set_option trace.compiler.ir.result true in
 def addPureY (y : PureY) :=
   addRawY <| .mk y () -- due to lean4#2292, will optimize away `mk` w/o Unit
 
diff --git a/tests/compile/lakefile.lean b/tests/compile/lakefile.lean
index ec1ecd9..61a9452 100644
--- a/tests/compile/lakefile.lean
+++ b/tests/compile/lakefile.lean
@@ -1,7 +1,7 @@
 import Lake
 open System Lake DSL
 
-package my_add
+package test
 
 require alloy from ".."/".."
 module_data alloy.c.o : BuildJob FilePath
@@ -19,6 +19,6 @@ lean_lib Test where
 
 lean_lib Eval
 
-@[default_target]
-lean_exe run where
+@[default_target, test_driver]
+lean_exe test where
   root := `Main
diff --git a/tests/compile/test.sh b/tests/compile/test.sh
index ffc925b..2af453c 100755
--- a/tests/compile/test.sh
+++ b/tests/compile/test.sh
@@ -1,6 +1,7 @@
 set -ex
-rm -rf build
+rm -rf .lake
 LAKE=${LAKE:-lake}
-$LAKE build -U
-$LAKE build Eval -v
-.lake/build/bin/run
+$LAKE update
+$LAKE build
+$LAKE lean Eval.lean
+$LAKE exe test