From 7b9d4ee060e088b3a37c96c94c0c610b303c2201 Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 18 Apr 2024 20:17:33 -0400 Subject: [PATCH] chore: use `lake -q` in test to request no extra output --- test.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/test.sh b/test.sh index a1f6049..0629d35 100755 --- a/test.sh +++ b/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."