make game directory more configurable

server/GameServer/FileWorker.lean

@@ -359,25 +359,22 @@ section Initialization
     fileMap  := default
 
   def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-    (levelModule : Name) (initParams : InitializeParams): IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
-    let some gameDir := GameServer.gameDirFromInitParams initParams
-      | throwServerError s!"Invalid rootUri: {initParams.rootUri?}"
-
+    (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams): IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
     -- 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"] }
+      { cwd := levelParams.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
+    let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p
 
     -- Set the search path
     Lean.searchPathRef.set paths
 
-    let env ← importModules [{ module := `Init : Import }, { module := levelModule : Import }] {} 0
+    let env ← importModules [{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
     -- return (env, paths)
 
     -- use empty header
@@ -425,7 +422,7 @@ section Initialization
        (levelParams : Game.DidOpenLevelParams) : IO (WorkerContext × WorkerState) := do
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
     let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-      levelParams.levelModule initParams
+      levelParams initParams
     let cancelTk ← CancelToken.new
     let ctx :=
       { hIn  := i

server/GameServer/Game.lean

@@ -5,6 +5,7 @@ open Lean
 structure GameServerState :=
 (env : Lean.Environment)
 (game : Name)
+(gameDir : String)
 
 abbrev GameServerM := StateT GameServerState Server.Watchdog.ServerM
 
@@ -57,6 +58,7 @@ structure LoadLevelParams where
 
 structure DidOpenLevelParams where
   uri : String
+  gameDir : String
   levelModule : Name
   tactics : Array ComputedInventoryItem
   lemmas : Array ComputedInventoryItem
@@ -90,7 +92,8 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
   fw.stdin.writeLspNotification {
     method := "$/game/didOpenLevel"
     param  := {
-      uri       := m.uri
+      uri := m.uri
+      gameDir := (← get).gameDir
       levelModule := lvl.module
       tactics := lvl.tactics.computed
       lemmas := lvl.lemmas.computed

server/GameServer/RpcHandlers.lean

@@ -12,24 +12,13 @@ open Meta
 
 namespace GameServer
 
-def splitRootUri (initParams : Lsp.InitializeParams) (i : Nat): Option String := Id.run do
-  let some rootUri := initParams.rootUri?
-    | return none
-  let rootUriParts := rootUri.splitOn "/"
-  if rootUriParts.length == 3 then
-    return rootUriParts[i]?
-  return none
-
 def levelIdFromFileName? (initParams : Lsp.InitializeParams) (fileName : String) : Option LevelId := Id.run do
   let fileParts := fileName.splitOn "/"
   if fileParts.length == 3 then
-    if let (some level, some game) := (fileParts[2]!.toNat?, splitRootUri initParams 2) then
+    if let (some level, some game) := (fileParts[2]!.toNat?, initParams.rootUri?) then
       return some {game, world := fileParts[1]!, level := level}
   return none
 
-def gameDirFromInitParams (initParams : Lsp.InitializeParams) : Option String :=
-  (splitRootUri initParams 0).map (s!"../../{·}")
-
 def getLevelByFileName? [Monad m] [MonadEnv m] (initParams : Lsp.InitializeParams) (fileName : String) : m (Option GameLevel) := do
   let some levelId := levelIdFromFileName? initParams fileName
     | return none

server/GameServer/Watchdog.lean

@@ -98,8 +98,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
   if args.length < 4 then
     throwServerError s!"Expected 3 command line arguments in addition to `--server`:
       game directory, the name of the main module, and the name of the game"
-  let gameId := args[1]!
-  let gameDir := s!"../../{gameId}"
+  let gameDir := args[1]!
   let module := args[2]!
   let gameName := args[3]!
   let workerPath := "./gameserver"
@@ -110,10 +109,10 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
   let i ← maybeTee "wdIn.txt" false i
   let o ← maybeTee "wdOut.txt" true o
   let e ← maybeTee "wdErr.txt" true e
-  let state := {env := ← createEnv gameDir module, game := gameName}
+  let state := {env := ← createEnv gameDir module, game := gameName, gameDir := gameDir}
   let initRequest ← i.readLspRequestAs "initialize" InitializeParams
-  -- We misuse the `rootUri` field to store gameId, module, and gameName
-  let rootUri? := s!"{gameId}/{module}/{gameName}"
+  -- We misuse the `rootUri` field to the gameName
+  let rootUri? := gameName
   let initRequest := {initRequest with param := {initRequest.param with rootUri?}}
   o.writeLspResponse {
     id     := initRequest.id

server/build.sh

@@ -3,6 +3,8 @@
 # Operate in the directory where this file is located
 cd $(dirname $0)
 
+# TODO: Pull prebuilt docker images from GitHub
+
 # Build elan image if not already present
 docker build --pull --rm -f elan.Dockerfile -t elan:latest .
 

server/index.mjs

@@ -10,11 +10,13 @@ const games = {
     adam: {
         name: "Adam",
         module: "Adam",
+        dir: "../../../../Robo",
         queueLength: 5
     },
     nng: {
         name: "NNG",
         module: "NNG",
+        dir: "../../../../NNG4",
         queueLength: 5
     }
 }
@@ -42,11 +44,11 @@ const queueLength = 5
 function startServerProcess(gameId) {
     const serverProcess = isDevelopment
         ? cp.spawn("./gameserver",
-            ["--server", gameId, games[gameId].module, games[gameId].name],
+            ["--server", games[gameId].dir, games[gameId].module, games[gameId].name],
             { cwd: "./build/bin/" })
         : cp.spawn("docker",
             ["run", "--runtime=runsc", "--network=none", "--rm", "-i", `${gameId}:latest`,
-              "./gameserver", "--server", gameId, games[gameId].module, games[gameId].name],
+              "./gameserver", "--server", "/game/", games[gameId].module, games[gameId].name],
             { cwd: "." })
     serverProcess.on('error', error =>
         console.error(`Launching Lean Server failed: ${error}`)