aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 16 Pull Requests 3 Packages Projects Releases Wiki Activity

chore: Update Lean to v4.20.1

This commit is contained in:
Leni Aniva 2025-06-17 08:38:03 -07:00
parent 3d65f6a69e
commit 3ce335ebfe
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
4 changed files with 18 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
Pantograph/Environment.lean
View File

@ -4,6 +4,7 @@ import Pantograph.Protocol
import Pantograph.Serial import Pantograph.Serial
import Lean.Environment import Lean.Environment
import Lean.Replay import Lean.Replay
import Lean.Util.Path
open Lean open Lean
open Pantograph open Pantograph
@ -130,17 +131,20 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
} } } }
| _ => pure core | _ => pure core
let result ← if args.source?.getD false then let result ← if args.source?.getD false then
let srcSearchPath ← initSrcSearchPath let srcSearchPath ← getSrcSearchPath
let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·) try
let declRange? ← findDeclarationRanges? name let sourceUri? ← module?.mapM (findLean srcSearchPath ·)
let sourceStart? := declRange?.map (·.range.pos) let declRange? ← findDeclarationRanges? name
let sourceEnd? := declRange?.map (·.range.endPos) let sourceStart? := declRange?.map (·.range.pos)
.pure { let sourceEnd? := declRange?.map (·.range.endPos)
result with .pure {
sourceUri?, result with
sourceStart?, sourceUri? := sourceUri?.map (toString ·),
sourceEnd?, sourceStart?,
} sourceEnd?,
}
catch _ =>
.pure result
else else
.pure result .pure result
return result return result

2
Pantograph/Library.lean
View File

@ -69,7 +69,7 @@ def createCoreContext (options: Array String): IO Core.Context := do
@[export pantograph_create_core_state] @[export pantograph_create_core_state]
def createCoreState (imports: Array String): IO Core.State := do def createCoreState (imports: Array String): IO Core.State := do
let env ← Lean.importModules let env ← Lean.importModules
(imports := imports.map (λ str => { module := str.toName, runtimeOnly := false })) (imports := imports.map (λ str => { module := str.toName }))
(opts := {}) (opts := {})
(trustLevel := 1) (trustLevel := 1)
(loadExts := true) (loadExts := true)

2
Pantograph/Version.lean
View File

@ -1,6 +1,6 @@
namespace Pantograph namespace Pantograph
@[export pantograph_version] @[export pantograph_version]
def version := "0.3.1" def version := "0.3.2"
end Pantograph end Pantograph

2
lean-toolchain
View File

@ -1 +1 @@
leanprover/lean4:v4.19.0 leanprover/lean4:v4.20.1