test: modernize scripts

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

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

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"

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
 

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

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