diff --git a/package.json b/package.json index 2b6994f..218a1ce 100644 --- a/package.json +++ b/package.json @@ -60,7 +60,7 @@ }, "scripts": { "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"", - "start_server": "cd server && lake build && (cd adam && lake exe cache get && lake build) && (cd nng && lake build) && NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"", + "start_server": "cd server && lake build && NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"", "start_client": "NODE_ENV=development webpack-dev-server --hot", "build": "npm run build_server && npm run build_client", "build_server": "server/build.sh", diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index bdacdf6..3ce7328 100644 --- a/server/GameServer/FileWorker.lean +++ b/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 diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean index 61f3d46..7ec447c 100644 --- a/server/GameServer/Game.lean +++ b/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 diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index 8903a3d..ed6286d 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/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 diff --git a/server/GameServer/Watchdog.lean b/server/GameServer/Watchdog.lean index 790cd56..45548cc 100644 --- a/server/GameServer/Watchdog.lean +++ b/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 diff --git a/server/build.sh b/server/build.sh index b1a2afd..308f555 100755 --- a/server/build.sh +++ b/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 . diff --git a/server/index.mjs b/server/index.mjs index 8dbec7a..a996681 100644 --- a/server/index.mjs +++ b/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}`)