Merge pull request #12 from tydeu/quiet-lake

chore: use `lake -q` in test to request no extra output

test.sh

@@ -23,19 +23,19 @@ check_command() {
     fi
 }
 
-check_command "lake exe lean4checker Lean4CheckerTests.AddFalse" "uncaught exception: (kernel) declaration type mismatch, 'false' has type
+check_command "lake -q exe lean4checker Lean4CheckerTests.AddFalse" "uncaught exception: (kernel) declaration type mismatch, 'false' has type
   Prop
 but it is expected to have type
   False"
 
-check_command "lake exe lean4checker Lean4CheckerTests.AddFalseConstructor" "uncaught exception: No such constructor False.intro"
+check_command "lake -q exe lean4checker Lean4CheckerTests.AddFalseConstructor" "uncaught exception: No such constructor False.intro"
 
-check_command "lake exe lean4checker --fresh Lean4CheckerTests.UseFalseConstructor" "uncaught exception: (kernel) unknown constant 'False.intro'"
+check_command "lake -q exe lean4checker --fresh Lean4CheckerTests.UseFalseConstructor" "uncaught exception: (kernel) unknown constant 'False.intro'"
 
 # The 'ReduceBool' test writes to a temporary file.
 # We clean up before and afterwards for consistency, although neither should be required.
 rm -f .lean4checker.tmp
-check_command "lake exe lean4checker Lean4CheckerTests.ReduceBool" "uncaught exception: (kernel) unknown declaration 'foo'"
+check_command "lake -q exe lean4checker Lean4CheckerTests.ReduceBool" "uncaught exception: (kernel) unknown declaration 'foo'"
 rm -f .lean4checker.tmp
 
 echo "All commands produced the expected errors."