merge nightly-testing

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-03-16
+leanprover/lean4:nightly-2024-04-30

test.sh

@@ -2,6 +2,19 @@
 
 lake build
 
+trim() {
+    local var="$*"
+    # Remove all leading whitespace and newline characters
+    while [[ $var =~ ^[[:space:]] ]]; do
+        var="${var#?}"  # Remove the first character repeatedly if it's whitespace
+    done
+    # Remove all trailing whitespace and newline characters
+    while [[ $var =~ [[:space:]]$ ]]; do
+        var="${var%?}"  # Remove the last character repeatedly if it's whitespace
+    done
+    printf '%s' "$var"
+}
+
 check_command() {
     local cmd="$1"
     local expected="$2"
@@ -13,6 +26,10 @@ check_command() {
         exit 1
     fi
 
+    # Account for weird whitespace from lake
+    # https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/Mathlib.20status.20updates/near/436249454
+    output=$(trim "$output")
+
     if [[ "$output" != "$expected" ]]; then
         echo "Error: The command '$cmd' did not produce the expected error."
         echo "Expected:"
@@ -23,19 +40,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."