From c404564a2b25f1ee4a0cb611904f944b0321f998 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 6 Jul 2024 19:53:50 -0700
Subject: [PATCH] chore: Bump Lean version to 4.10.0-rc1

---
 Pantograph/Compile/Frontend.lean | 2 +-
 Pantograph/Environment.lean      | 2 +-
 Pantograph/Goal.lean             | 9 ++-------
 Pantograph/Version.lean          | 2 +-
 flake.nix                        | 2 +-
 lean-toolchain                   | 2 +-
 6 files changed, 7 insertions(+), 12 deletions(-)

diff --git a/Pantograph/Compile/Frontend.lean b/Pantograph/Compile/Frontend.lean
index 5cb3e63..3dbad85 100644
--- a/Pantograph/Compile/Frontend.lean
+++ b/Pantograph/Compile/Frontend.lean
@@ -52,7 +52,7 @@ def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do
   let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
   let s' := (← get).commandState
   let after := s'.env
-  let msgs := s'.messages.msgs.drop s.messages.msgs.size
+  let msgs := s'.messages.toList.drop s.messages.toList.length
   let trees := s'.infoState.trees.drop s.infoState.trees.size
   let ⟨_, fileName, fileMap⟩  := (← read).inputCtx
   return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index d5cdc3d..6d91abb 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -132,7 +132,7 @@ def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) :
     (hints := Lean.mkReducibilityHintsRegularEx 1)
     (safety := Lean.DefinitionSafety.safe)
     (all := [])
-  let env' ← match env.addDecl constant with
+  let env' ← match env.addDecl (← getOptions) constant with
     | .error e => do
       let options ← Lean.MonadOptions.getOptions
       let desc ← (e.toMessageData options).toString
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 46888e7..8c2324d 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -7,11 +7,6 @@ import Pantograph.Protocol
 import Pantograph.Tactic
 import Lean
 
-def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
-  {
-    msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
-  }
-
 
 namespace Pantograph
 open Lean
@@ -178,7 +173,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.
   try
     let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
     if (← getThe Core.State).messages.hasErrors then
-      let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
+      let messages := (← getThe Core.State).messages.toArray
       let errors ← (messages.map (·.data)).mapM fun md => md.toString
       return .failure errors
     let nextElabState ← MonadBacktrack.saveState
@@ -223,7 +218,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
     goal.checkNotAssigned `GoalState.assign
     goal.assign expr
     if (← getThe Core.State).messages.hasErrors then
-      let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
+      let messages := (← getThe Core.State).messages.toArray
       let errors ← (messages.map (·.data)).mapM fun md => md.toString
       return .failure errors
     let prevMCtx := state.savedState.term.meta.meta.mctx
diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean
index 207b597..f3bcf93 100644
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.2.16"
+def version := "0.2.17"
 
 end Pantograph
diff --git a/flake.nix b/flake.nix
index ad40a3f..b96d5e2 100644
--- a/flake.nix
+++ b/flake.nix
@@ -6,7 +6,7 @@
     flake-parts.url = "github:hercules-ci/flake-parts";
     lean = {
       # Do not follow input's nixpkgs since it could cause build failures
-      url = "github:leanprover/lean4?ref=v4.8.0-rc1";
+      url = "github:leanprover/lean4?ref=v4.10.0-rc1";
     };
     lspec = {
       url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
diff --git a/lean-toolchain b/lean-toolchain
index d8a6d7e..d69d1ed 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc1
+leanprover/lean4:v4.10.0-rc1