fixes for v4.6.0-rc1

server/GameServer/FileWorker.lean

@@ -299,7 +299,7 @@ where
   private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream)
       (snaps : Array Snapshot) : IO Unit := do
     let trees := snaps.map fun snap => snap.infoTree
-    let references := findModuleRefs m.text trees (localVars := true)
+    let references ← findModuleRefs m.text trees (localVars := true) |>.toLspModuleRefs
     let param := { version := m.version, references : LeanIleanInfoParams }
     hOut.writeLspNotification { method, param }
 
@@ -503,6 +503,12 @@ def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
   fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
   fileMap  := default
 
+/-- `gameDir` and `module` were added.
+
+TODO: In general this resembles little similarity with the
+original code, and I don't know why...
+-/
+-- @[inherit_doc Lean.Server.FileWorker.compileHeader]
 def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
     (gameDir : String) (module : Name):
     IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
@@ -538,7 +544,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
     let cmdState := Elab.Command.mkState headerEnv {} opts
     let cmdState := { cmdState with infoState := {
       enabled := true
-      trees := #[Elab.InfoTree.context ({
+      trees := #[Elab.InfoTree.context (.commandCtx {
         env     := headerEnv
         fileMap := m.text
         ngen    := { namePrefix := `_worker }
@@ -555,7 +561,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
     let headerSnap := {
       beginPos := 0
       stx := headerStx
-      mpState := {}
+      mpState := {} -- was `headerParserState`
       cmdState := cmdState
       interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
       tacticCache := (← IO.mkRef {})

server/GameServer/InteractiveGoal.lean

@@ -146,7 +146,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
     return {
       hyps
       type := goalFmt
-      ctx := ⟨← Elab.ContextInfo.save⟩
+      ctx := ⟨{← Elab.CommandContextInfo.save with }⟩
       userName?
       goalPrefix := getGoalPrefix mvarDecl
       mvarId

server/lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
+   "rev": "276953b13323ca151939eafaaec9129bf7970306",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.5.0",
+   "inputRev": "v4.6.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "GameServer",

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.6.0-rc1