From e165e41efa8a65628501f6b8390b14040eb0ac62 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 17 May 2024 20:31:45 -0700
Subject: [PATCH] chore: Version bump to v4.8.0-rc1

---
 Pantograph/Goal.lean | 4 ++--
 flake.lock           | 8 ++++----
 flake.nix            | 2 +-
 lean-toolchain       | 2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 484ff51..e6a59d0 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -90,7 +90,7 @@ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax
       Elab.Tactic.evalTactic stx
       if (← getThe Core.State).messages.hasErrors then
         let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
-        let errors ← (messages.map Message.data).mapM fun md => md.toString
+        let errors ← (messages.map (·.data)).mapM fun md => md.toString
         return .error errors
       else
         return .ok (← MonadBacktrack.saveState)
@@ -161,7 +161,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
     goal.assign expr
     if (← getThe Core.State).messages.hasErrors then
       let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
-      let errors ← (messages.map Message.data).mapM fun md => md.toString
+      let errors ← (messages.map (·.data)).mapM fun md => md.toString
       return .failure errors
     let prevMCtx := state.savedState.term.meta.meta.mctx
     let nextMCtx ← getMCtx
diff --git a/flake.lock b/flake.lock
index 39888a8..1a50363 100644
--- a/flake.lock
+++ b/flake.lock
@@ -42,16 +42,16 @@
         "nixpkgs-old": "nixpkgs-old"
       },
       "locked": {
-        "lastModified": 1711508550,
-        "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=",
+        "lastModified": 1714704934,
+        "narHash": "sha256-q0kLyIahUXolkSrBZSegPF+R99WAH1YC96JfKoFntDE=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
+        "rev": "dcccfb73cb247e9478220375ab7de03f7c67e505",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
+        "ref": "v4.8.0-rc1",
         "repo": "lean4",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 2458805..ad40a3f 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,8 +5,8 @@
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
     lean = {
-      url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
       # Do not follow input's nixpkgs since it could cause build failures
+      url = "github:leanprover/lean4?ref=v4.8.0-rc1";
     };
     lspec = {
       url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
diff --git a/lean-toolchain b/lean-toolchain
index c630636..d8a6d7e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-03-27
+leanprover/lean4:v4.8.0-rc1