diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index 55bf9aa..65b8a33 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -9,6 +9,14 @@ defined in this file. open Lean +-- Note: When changing these, one also needs to change them in `index.mjs` + +/-! The default game name if `Game "MyGame"` is not used. -/ +def defaultGameName: String := "MyGame" + +/-! The default game module name. -/ +def defaultGameModule: String := "Game" + /-! ## Hints -/ /-- @@ -123,15 +131,15 @@ def setCurLevelIdx (level : Nat) : m Unit := def getCurLayer [MonadError m] : m Layer := do match curGameExt.getState (← getEnv), curWorldExt.getState (← getEnv), curLevelExt.getState (← getEnv) with - | some _, some _, some _ => return Layer.Level - | some _, some _, none => return Layer.World - | some _, none, none => return Layer.Game + | _, some _, some _ => return Layer.Level + | _, some _, none => return Layer.World + | _, none, none => return Layer.Game | _, _, _ => throwError "Invalid Layer" -def getCurGameId [MonadError m] : m Name := do +def getCurGameId [Monad m] : m Name := do match curGameExt.getState (← getEnv) with | some game => return game - | none => throwError "Current game not set" + | none => return defaultGameName def getCurWorldId [MonadError m] : m Name := do match curWorldExt.getState (← getEnv) with @@ -296,9 +304,11 @@ def getLevel? (levelId : LevelId) : m (Option GameLevel) := do | return none return level -def getCurGame [MonadError m] : m Game := do +def getCurGame [Monad m] : m Game := do let some game ← getGame? (← getCurGameId) - | throwError m!"Game {← getCurGameId} does not exist" + | let game := {name := defaultGameName} + insertGame defaultGameName game + return game return game def modifyCurGame (fn : Game → m Game) [MonadError m] : m Unit := do diff --git a/server/GameServer/Watchdog.lean b/server/GameServer/Watchdog.lean index 45548cc..4d92376 100644 --- a/server/GameServer/Watchdog.lean +++ b/server/GameServer/Watchdog.lean @@ -95,12 +95,12 @@ def createEnv (gameDir : String) (module : String) : IO Environment := do return env 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" + if args.length < 2 then + throwServerError s!"Expected 1-3 command line arguments in addition to `--server`: + game directory, the name of the main module (optional), and the name of the game (optional)." let gameDir := args[1]! - let module := args[2]! - let gameName := args[3]! + let module := if args.length < 3 then defaultGameModule else args[2]! + let gameName := if args.length < 4 then defaultGameName else args[3]! let workerPath := "./gameserver" -- TODO: Do the following commands slow us down? let srcSearchPath ← initSrcSearchPath (← getBuildDir) diff --git a/server/index.mjs b/server/index.mjs index 35164b1..acdf9f0 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -17,18 +17,20 @@ import { importTrigger, importStatus } from './import.mjs' */ const games = { "g/hhu-adam/robo": { - name: "Adam", - module: "Game", + // module: "Game", // The lean module's name. Defaults to "Game" + // name: "Adam", // For the `Game "Adam"` tag in the games. Defaults to "MyGame" dir: "../../../../Robo", queueLength: 5 }, "g/hhu-adam/nng4": { - name: "NNG", - module: "Game", + // module: "Game", + // name: "NNG", dir: "../../../../NNG4", queueLength: 5 } } +// Note: If `module` and `name` are uncommented, one also needs to add them as arguments to +// the `--server` call below. const __filename = url.fileURLToPath(import.meta.url); const __dirname = url.fileURLToPath(new URL('.', import.meta.url)); @@ -61,7 +63,7 @@ function startServerProcess(tag) { let serverProcess if (isDevelopment && games[tag]?.dir) { serverProcess = cp.spawn("./gameserver", - ["--server", games[tag].dir, games[tag].module, games[tag].name], + ["--server", games[tag].dir], // games[tag].module, games[tag].name { cwd: "./build/bin/" }) } else { serverProcess = cp.spawn("docker",