From 64817f49d9bc3a8bfef447e60b9424b8468aaa10 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Mon, 18 Mar 2024 14:40:25 +1100
Subject: [PATCH 1/4] chore: adaptations for nightly-2024-03-16

---
 Lean4CheckerTests/OpenPrivate.lean | 2 +-
 lean-toolchain                     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Lean4CheckerTests/OpenPrivate.lean b/Lean4CheckerTests/OpenPrivate.lean
index 0d3686a..7ade0b9 100644
--- a/Lean4CheckerTests/OpenPrivate.lean
+++ b/Lean4CheckerTests/OpenPrivate.lean
@@ -49,7 +49,7 @@ def elabOpenPrivateLike (ids : Array Ident) (tgts mods : Option (Array Ident))
   (f : (priv full user : Name) → CommandElabM Name) : CommandElabM Unit := do
   let mut names := NameSet.empty
   for tgt in tgts.getD #[] do
-    let n ← resolveGlobalConstNoOverloadWithInfo tgt
+    let n ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo tgt
     names ← Meta.collectPrivateIn n names
   for mod in mods.getD #[] do
     let some modIdx := (← getEnv).moduleIdxForModule? mod.getId
diff --git a/lean-toolchain b/lean-toolchain
index 6b26dd5..539e2b1 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0-rc1
+leanprover/lean4:nightly-2024-03-16

From 4d2ed60a5b7b22a7c7c3ccde0159e51c91df5aa9 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Mon, 18 Mar 2024 15:05:27 +1100
Subject: [PATCH 2/4] adaptations for v4.8.0

---
 Lean4CheckerTests/OpenPrivate.lean | 2 +-
 lean-toolchain                     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Lean4CheckerTests/OpenPrivate.lean b/Lean4CheckerTests/OpenPrivate.lean
index 0d3686a..7ade0b9 100644
--- a/Lean4CheckerTests/OpenPrivate.lean
+++ b/Lean4CheckerTests/OpenPrivate.lean
@@ -49,7 +49,7 @@ def elabOpenPrivateLike (ids : Array Ident) (tgts mods : Option (Array Ident))
   (f : (priv full user : Name) → CommandElabM Name) : CommandElabM Unit := do
   let mut names := NameSet.empty
   for tgt in tgts.getD #[] do
-    let n ← resolveGlobalConstNoOverloadWithInfo tgt
+    let n ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo tgt
     names ← Meta.collectPrivateIn n names
   for mod in mods.getD #[] do
     let some modIdx := (← getEnv).moduleIdxForModule? mod.getId
diff --git a/lean-toolchain b/lean-toolchain
index 6b26dd5..539e2b1 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0-rc1
+leanprover/lean4:nightly-2024-03-16

From b68e32ce1f1c83c309c4e6bee898ad811ea7035f Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 2 May 2024 22:12:35 +1000
Subject: [PATCH 3/4] move to v4.8.0-rc1

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index df30ca3..d8a6d7e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-04-30
+leanprover/lean4:v4.8.0-rc1

From 76da07e11f6a97a80ca5d420bfac218a849f39d1 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 2 May 2024 22:14:17 +1000
Subject: [PATCH 4/4] no need for trim

---
 test.sh | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/test.sh b/test.sh
index dcfc341..0629d35 100755
--- a/test.sh
+++ b/test.sh
@@ -2,19 +2,6 @@
 
 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"
@@ -26,10 +13,6 @@ 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:"