From d305918bb944fef285864ab8df3d863c13f3d287 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 24 Mar 2025 17:57:34 -0700
Subject: [PATCH] chore: Update Lean to v4.17.0

---
 Pantograph/Delate.lean      |  3 ++-
 Pantograph/Environment.lean | 11 ++---------
 Pantograph/Version.lean     |  2 +-
 Test/Serial.lean            |  8 ++------
 lean-toolchain              |  2 +-
 5 files changed, 8 insertions(+), 18 deletions(-)

diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index efb1008..b6e016c 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -122,7 +122,8 @@ partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
         return .visit (mkAppN assign args)
       else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
         if ← isTracingEnabledFor `Pantograph.Delate then
-          let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
+          let substTableStr := ",".intercalate $
+            Array.zipWith (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") fvars args |>.toList
           trace[Pantograph.Delate]"MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
 
         if args.size < fvars.size then
diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index aa4dd03..8e552a3 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -91,7 +91,6 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
     isUnsafe := info.isUnsafe,
     value? := ← value?.mapM (λ v => serializeExpression options v |>.run'),
     publicName? := Lean.privateToUserName? name |>.map (·.toString),
-    -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
     typeDependency? := if args.dependency?.getD false
       then .some <| type.getUsedConstants.map (λ n => serializeName n)
       else .none,
@@ -169,7 +168,7 @@ def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) :
   let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
     | .ok t => pure t
     | .error e => return .error $ Protocol.errorExpr e
-  let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
+  let decl := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
     (name := args.name.toName)
     (levelParams := [])
     (type := type)
@@ -177,13 +176,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 (← getOptions) constant with
-    | .error e => do
-      let options ← Lean.MonadOptions.getOptions
-      let desc ← (e.toMessageData options).toString
-      return .error $ { error := "kernel", desc }
-    | .ok env' => pure env'
-  Lean.MonadEnv.modifyEnv (λ _ => env')
+  Lean.addDecl decl
   return .ok {}
 
 end Pantograph.Environment
diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean
index a65274d..845d83f 100644
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.3.0-rc.1"
+def version := "0.3.0"
 
 end Pantograph
diff --git a/Test/Serial.lean b/Test/Serial.lean
index fcdc155..bd22d72 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -47,12 +47,8 @@ def test_environment_pickling : TestM Unit := do
       (hints := Lean.mkReducibilityHintsRegularEx 1)
       (safety := Lean.DefinitionSafety.safe)
       (all := [])
-    let env' ← match (← getEnv).addDecl (← getOptions) c with
-      | .error e => do
-        let error ← (e.toMessageData (← getOptions)).toString
-        throwError error
-      | .ok env' => pure env'
-    environmentPickle env' envPicklePath
+    addDecl c
+    environmentPickle (← getEnv) envPicklePath
 
   let _ ← runCoreM coreDst do
     let (env', _) ← environmentUnpickle envPicklePath
diff --git a/lean-toolchain b/lean-toolchain
index 2586f88..5499a24 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0
+leanprover/lean4:v4.17.0