Import only specific Level file

Fixes #35

server/leanserver/GameServer/Commands.lean

@@ -80,9 +80,11 @@ elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : comma
   -- | some name => `(lemma $name $sig $val)
 
   let scope ← getScope
+  let env ← getEnv
 
   elabCommand thmStatement
   modifyCurLevel fun level => pure {level with
+    module := env.header.mainModule
     goal := sig,
     scope := scope,
     descrText := descr.getString,

server/leanserver/GameServer/EnvExtensions.lean

@@ -199,6 +199,8 @@ structure GameLevel where
   scope : Elab.Command.Scope := default
   descrText: String := default
   descrFormat : String := default
+  -- The module to be imported when playing this level:
+  module : Name := default
   deriving Inhabited, Repr
 
 /-! ## World -/

server/leanserver/GameServer/FileWorker.lean

@@ -3,6 +3,7 @@
 import Lean
 import GameServer.EnvExtensions
 import GameServer.RpcHandlers
+import GameServer.Game
 
 import Lean.Server.FileWorker
 
@@ -132,7 +133,8 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
   let (output, _) ← IO.FS.withIsolatedStreams (isolateStderr := server.stderrAsMessages.get snap.cmdState.scopes.head!.opts) <| liftM (m := BaseIO) do
     Elab.Command.catchExceptions
       (getResetInfoTrees *> do
-        let level ← GameServer.getLevelByFileName inputCtx.fileName
+        let some level ← GameServer.getLevelByFileName? inputCtx.fileName
+          | throwError "Level not found: {inputCtx.fileName}"
         let scope := level.scope
 
         -- use open namespaces and options as in the level file
@@ -344,67 +346,13 @@ end Updates
 
 section Initialization
 
-
   def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
     input    := "" -- No header!
     fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
     fileMap  := default
 
-  -- TODO: Duplicate in Watchdog?
-  def createEnv : IO (Environment × SearchPath) := do
-    let gameDir := "../../../testgame"
-
-    -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
-    let out ← IO.Process.output
-      { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
-    if out.exitCode != 0 then
-      throwServerError s!"Error while running Lake: {out.stderr}"
-
-    -- Make the paths relative to the current directory
-    let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
-    let currentDir ← IO.currentDir
-    let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
-
-    -- Set the search path
-    Lean.searchPathRef.set paths
-
-    let gameName := `TestGame
-    let env ← importModules [{ module := `Init : Import }, { module := gameName : Import }] {} 0
-    return (env, paths)
-
-  -- def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-  --     : IO (Snapshot × SearchPath) := do
-  --   let mut (headerEnv, paths) ← createEnv
-  --   try
-  --     if let some path := System.Uri.fileUriToPath? m.uri then
-  --       headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
-  --   catch _ => pure ()
-  --   let cmdState := Elab.Command.mkState headerEnv {} opts
-  --   let cmdState := { cmdState with infoState := {
-  --     enabled := true
-  --     trees := #[Elab.InfoTree.context ({
-  --       env     := headerEnv
-  --       fileMap := m.text
-  --       ngen    := { namePrefix := `_worker }
-  --     }) (Elab.InfoTree.node
-  --         (Elab.Info.ofCommandInfo { elaborator := `header, stx := Syntax.missing })
-  --         #[].toPArray'
-  --     )].toPArray'
-  --   }}
-  --   let headerSnap := {
-  --     beginPos := 0
-  --     stx := Syntax.missing
-  --     mpState := {}
-  --     cmdState := cmdState
-  --     interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
-  --     tacticCache := (← IO.mkRef {})
-  --   }
-  --   publishDiagnostics m headerSnap.diagnostics.toArray hOut
-  --   return (headerSnap, paths)
-
-
   def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-      : IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
+    (levelModule : Name) : IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
     let gameDir := "../../../testgame"
 
     -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
@@ -421,8 +369,7 @@ section Initialization
     -- Set the search path
     Lean.searchPathRef.set paths
 
-    let gameName := `TestGame
-    let env ← importModules [{ module := `Init : Import }, { module := gameName : Import }] {} 0
+    let env ← importModules [{ module := `Init : Import }, { module := levelModule : Import }] {} 0
     -- return (env, paths)
 
     -- use empty header
@@ -467,9 +414,9 @@ section Initialization
       return (headerSnap, srcSearchPath)
 
   def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
-      : IO (WorkerContext × WorkerState) := do
+      (levelModule : Name) : IO (WorkerContext × WorkerState) := do
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
-    let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
+    let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets) levelModule
     let cancelTk ← CancelToken.new
     let ctx :=
       { hIn  := i
@@ -566,6 +513,8 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let o ← maybeTee "fwOut.txt" true o
   let initParams ← i.readLspRequestAs "initialize" InitializeParams
   let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
+  let ⟨_, levelParam⟩ ← i.readLspNotificationAs "$/game/didOpenLevel" Game.DidOpenLevelParams
+
   let doc := param.textDocument
   /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
     "\n", which should be enough to handle both LF and CRLF correctly.
@@ -576,7 +525,7 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
-    let (ctx, st) ← initializeWorker meta i o e initParams.param opts
+    let (ctx, st) ← initializeWorker meta i o e initParams.param opts levelParam.levelModule
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) mainLoop
     return (0 : UInt32)
   catch e =>

server/leanserver/GameServer/Game.lean

@@ -1,5 +1,6 @@
 import Lean
 import GameServer.EnvExtensions
+import GameServer.RpcHandlers
 
 
 open Lean
@@ -46,13 +47,18 @@ structure LevelInfo where
   introduction : String
   descrText : String := ""
   descrFormat : String := ""
-deriving ToJson
+deriving ToJson, FromJson
 
 structure LoadLevelParams where
   world : Name
   level : Nat
   deriving ToJson, FromJson
 
+structure DidOpenLevelParams where
+  uri : String
+  levelModule : Name
+  deriving ToJson, FromJson
+
 structure Doc where
   name: String
   text: String
@@ -79,6 +85,29 @@ def mkDoc (name : Name) (type : TacOrLem) : GameServerM (Option Doc) := do
       { name := doc.name.toString
         text := doc.content }
 
+def handleDidOpenLevel (params : Json) : GameServerM Unit := do
+  let p ← parseParams _ params
+  let m := p.textDocument
+  -- Execute the regular handling of the `didOpen` event
+  handleDidOpen p
+  let fw ← findFileWorker! m.uri
+  let s ← get
+  let c ← read
+  let some lvl ← GameServer.getLevelByFileName? ((System.Uri.fileUriToPath? m.uri).getD m.uri |>.toString)
+    | do
+      c.hLog.putStr s!"Level not found: {m.uri}"
+      c.hLog.flush
+  -- Send an extra notification to the file worker to inform it about the level data
+  fw.stdin.writeLspNotification {
+    method := "$/game/didOpenLevel"
+    param  := {
+      uri       := m.uri
+      levelModule := lvl.module
+      : DidOpenLevelParams
+    }
+  }
+
+
 partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
   match ev with
   | ServerEvent.clientMsg msg =>

server/leanserver/GameServer/RpcHandlers.lean

@@ -13,20 +13,17 @@ open Meta
 
 namespace GameServer
 
--- TODO: Find a better way to pass on the file name?
-def levelIdFromFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String) : m LevelId := do
+def levelIdFromFileName? (fileName : String) : Option LevelId := Id.run do
   let fileParts := fileName.splitOn "/"
   if fileParts.length == 3 then
     if let some level := fileParts[2]!.toNat? then
-      return {game := `TestGame, world := fileParts[1]!, level := level}
-  throwError s!"Could not find level ID in file name: {fileName}"
+      return some {game := `TestGame, world := fileParts[1]!, level := level}
+  return none
 
-def getLevelByFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String) : m GameLevel := do
-  let levelId ← levelIdFromFileName fileName
-  -- TODO: make world and game configurable
-  let some level ← getLevel? levelId
-    | throwError "Level not found"
-  return level
+def getLevelByFileName? [Monad m] [MonadEnv m] (fileName : String) : m (Option GameLevel) := do
+  let some levelId := levelIdFromFileName? fileName
+    | return none
+  return ← getLevel? levelId
 
 /-- Check if each meta variable in `declMvars` has a matching fvar in `declFvars` -/
 def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool := do
@@ -54,7 +51,8 @@ open Meta in
 /-- Find all hints whose trigger matches the current goal -/
 def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array GameHint) := do
   goal.withContext do
-    let level ← getLevelByFileName doc.meta.mkInputContext.fileName
+    let some level ← getLevelByFileName? doc.meta.mkInputContext.fileName
+      | throwError "Level not found: {doc.meta.mkInputContext.fileName}"
     let hints ← level.hints.filterMapM fun hint => do
       let (declMvars, binderInfo, hintGoal) ← forallMetaBoundedTelescope hint.goal hint.intros
       -- TODO: Protext mvars in the type of `goal` to be instantiated?

server/leanserver/GameServer/Watchdog.lean

@@ -39,7 +39,11 @@ open System.Uri
         | Message.responseError _ _ e .. =>
           throwServerError s!"Unhandled response error: {e}"
         | Message.notification method (some params) =>
-          handleNotification method (toJson params)
+          if method == "textDocument/didOpen" then
+            -- for lean4game, we need to pass in extra information when a level is opened:
+            Game.handleDidOpenLevel (← parseParams _ (toJson params))
+          else
+            handleNotification method (toJson params)
           mainLoop (←runClientTask)
         | _ => throwServerError "Got invalid JSON-RPC message"
       | ServerEvent.clientError e => throw e