From 3ce335ebfe8465b213e4256cf892115f94e5af80 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 17 Jun 2025 08:38:03 -0700
Subject: [PATCH] chore: Update Lean to v4.20.1

---
 Pantograph/Environment.lean | 26 +++++++++++++++-----------
 Pantograph/Library.lean     |  2 +-
 Pantograph/Version.lean     |  2 +-
 lean-toolchain              |  2 +-
 4 files changed, 18 insertions(+), 14 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index 4f0a678..dce74c8 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -4,6 +4,7 @@ import Pantograph.Protocol
 import Pantograph.Serial
 import Lean.Environment
 import Lean.Replay
+import Lean.Util.Path
 
 open Lean
 open Pantograph
@@ -130,17 +131,20 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
       } }
     | _ => pure core
   let result ← if args.source?.getD false then
-      let srcSearchPath ← initSrcSearchPath
-      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
-      let declRange? ← findDeclarationRanges? name
-      let sourceStart? := declRange?.map (·.range.pos)
-      let sourceEnd? := declRange?.map (·.range.endPos)
-      .pure {
-        result with
-        sourceUri?,
-        sourceStart?,
-        sourceEnd?,
-      }
+      let srcSearchPath ← getSrcSearchPath
+      try
+        let sourceUri? ← module?.mapM (findLean srcSearchPath ·)
+        let declRange? ← findDeclarationRanges? name
+        let sourceStart? := declRange?.map (·.range.pos)
+        let sourceEnd? := declRange?.map (·.range.endPos)
+        .pure {
+          result with
+          sourceUri? := sourceUri?.map (toString ·),
+          sourceStart?,
+          sourceEnd?,
+        }
+      catch _ =>
+        .pure result
     else
       .pure result
   return result
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 14e7b67..97e3d82 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -69,7 +69,7 @@ def createCoreContext (options: Array String): IO Core.Context := do
 @[export pantograph_create_core_state]
 def createCoreState (imports: Array String): IO Core.State := do
   let env ← Lean.importModules
-    (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
+    (imports := imports.map (λ str => { module := str.toName }))
     (opts := {})
     (trustLevel := 1)
     (loadExts := true)
diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean
index 6853517..4d937cd 100644
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.3.1"
+def version := "0.3.2"
 
 end Pantograph
diff --git a/lean-toolchain b/lean-toolchain
index 7aca1d8..78adacd 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.19.0
+leanprover/lean4:v4.20.1