From bf2315b4743b4cec1b10f0b5a31e3decebab27e8 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 23 Mar 2023 15:14:05 +0100 Subject: [PATCH] remove references to `testgame` on the server, add gameId to router --- client/src/App.tsx | 9 ++- client/src/components/Inventory.tsx | 5 +- client/src/components/Level.tsx | 35 +++++----- client/src/components/Welcome.tsx | 9 ++- client/src/connection.ts | 23 ++++--- client/src/index.tsx | 9 ++- client/src/state/api.ts | 16 ++--- server/index.mjs | 65 ++++++++++++------- server/leanserver/GameServer/FileWorker.lean | 21 +++--- server/leanserver/GameServer/Game.lean | 4 +- server/leanserver/GameServer/RpcHandlers.lean | 28 +++++--- server/leanserver/GameServer/Watchdog.lean | 20 ++++-- server/leanserver/Main.lean | 2 +- server/server.Dockerfile | 2 +- 14 files changed, 157 insertions(+), 91 deletions(-) diff --git a/client/src/App.tsx b/client/src/App.tsx index c1eb545..3c06cb9 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -1,6 +1,6 @@ import * as React from 'react'; import { useState, useEffect } from 'react'; -import { Outlet } from "react-router-dom"; +import { Outlet, useParams } from "react-router-dom"; import '@fontsource/roboto/300.css'; import '@fontsource/roboto/400.css'; @@ -10,10 +10,15 @@ import '@fontsource/roboto/700.css'; import './reset.css'; import './app.css'; +export const GameIdContext = React.createContext(undefined); + function App() { + const params = useParams(); return (
- + + +
) } diff --git a/client/src/components/Inventory.tsx b/client/src/components/Inventory.tsx index df5410c..2135760 100644 --- a/client/src/components/Inventory.tsx +++ b/client/src/components/Inventory.tsx @@ -5,6 +5,7 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-solid-svg-icons' import Markdown from './Markdown'; import { useLoadDocQuery, ComputedInventoryItem } from '../state/api'; +import { GameIdContext } from '../App'; export function Inventory({ tactics, lemmas, definitions, setInventoryDoc } : {lemmas: ComputedInventoryItem[], @@ -77,8 +78,8 @@ function InventoryItem({name, displayName, locked, disabled, showDoc}) { } export function Documentation({name, type}) { - - const doc = useLoadDocQuery({type: type, name: name}) + const gameId = React.useContext(GameIdContext) + const doc = useLoadDocQuery({game: gameId, type: type, name: name}) return <>

{doc.data?.displayName}

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 89a9de4..9e44489 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -40,6 +40,7 @@ import Markdown from './Markdown'; import Split from 'react-split' import { Alert } from '@mui/material'; +import { GameIdContext } from '../App'; export const MonacoEditorContext = React.createContext(null as any); @@ -125,9 +126,9 @@ function PlayableLevel({worldId, levelId}) { }]); } - const gameInfo = useGetGameInfoQuery() - - const level = useLoadLevelQuery({world: worldId, level: levelId}) + const gameId = React.useContext(GameIdContext) + const gameInfo = useGetGameInfoQuery({game: gameId}) + const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) const dispatch = useAppDispatch() @@ -209,8 +210,8 @@ function PlayableLevel({worldId, levelId}) { {level?.data?.conclusion} {levelId >= gameInfo.data?.worldSize[worldId] ? - : - : + } } @@ -230,7 +231,8 @@ function PlayableLevel({worldId, levelId}) { export default Level function Introduction({worldId}) { - const gameInfo = useGetGameInfoQuery() + const gameId = React.useContext(GameIdContext) + const gameInfo = useGetGameInfoQuery({game: gameId}) return <>
@@ -245,8 +247,8 @@ function Introduction({worldId}) {
{0 == gameInfo.data?.worldSize[worldId] ? - : - : + }
@@ -255,11 +257,12 @@ function Introduction({worldId}) { } function LevelAppBar({isLoading, levelId, worldId, levelTitle}) { - const gameInfo = useGetGameInfoQuery() + const gameId = React.useContext(GameIdContext) + const gameInfo = useGetGameInfoQuery({game: gameId}) return
- + {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`} @@ -269,10 +272,10 @@ function LevelAppBar({isLoading, levelId, worldId, levelTitle}) { {levelTitle}
@@ -282,6 +285,7 @@ function LevelAppBar({isLoading, levelId, worldId, levelTitle}) { function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) { const connection = React.useContext(ConnectionContext) + const gameId = React.useContext(GameIdContext) const [editor, setEditor] = useState(null) const [infoProvider, setInfoProvider] = useState(null) @@ -308,7 +312,7 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCo theme: 'vs-code-theme-converted' }) - const infoProvider = new InfoProvider(connection.getLeanClient()) + const infoProvider = new InfoProvider(connection.getLeanClient(gameId)) const editorApi = infoProvider.getApi() @@ -358,7 +362,7 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCo return () => { infoProvider.dispose(); editor.dispose() } }, []) - const {leanClient, leanClientStarted} = useLeanClient() + const {leanClient, leanClientStarted} = useLeanClient(gameId) // Create model when level changes useEffect(() => { @@ -391,7 +395,8 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCo /** Open all files in this world on the server so that they will load faster when accessed */ function useLoadWorldFiles(worldId) { - const gameInfo = useGetGameInfoQuery() + const gameId = React.useContext(GameIdContext) + const gameInfo = useGetGameInfoQuery({game: gameId}) const store = useStore() useEffect(() => { diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx index 1c97932..c5fce54 100644 --- a/client/src/components/Welcome.tsx +++ b/client/src/components/Welcome.tsx @@ -14,13 +14,15 @@ import { useGetGameInfoQuery } from '../state/api'; import { Link } from 'react-router-dom'; import Markdown from './Markdown'; import { selectCompleted } from '../state/progress'; +import { GameIdContext } from '../App'; function LevelIcon({ worldId, levelId, position }) { + const gameId = React.useContext(GameIdContext) const completed = useSelector(selectCompleted(worldId,levelId)) // TODO: relative positioning? return ( - + ) @@ -29,7 +31,8 @@ function LevelIcon({ worldId, levelId, position }) { function Welcome() { const navigate = useNavigate(); - const gameInfo = useGetGameInfoQuery() + const gameId = React.useContext(GameIdContext) + const gameInfo = useGetGameInfoQuery({game: gameId}) const { nodes, bounds }: any = gameInfo.data ? computeWorldLayout(gameInfo.data?.worlds) : {nodes: []} @@ -55,7 +58,7 @@ function Welcome() { let position: cytoscape.Position = nodes[id].position svgElements.push( - + {nodes[id].data.title ? nodes[id].data.title : id} diff --git a/client/src/connection.ts b/client/src/connection.ts index f25b4ca..2d630ac 100644 --- a/client/src/connection.ts +++ b/client/src/connection.ts @@ -6,12 +6,17 @@ import { useState } from 'react'; export class Connection { - private leanClient = null - - getLeanClient(): LeanClient { - if (this.leanClient === null) { - const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + private game: string = undefined // We only keep a connection to a single game at a time + private leanClient: LeanClient = null + getLeanClient(game): LeanClient { + if (this.game !== game) { + if (this.leanClient) { + this.leanClient.stop() // Stop previous Lean client + } + this.game = game + // Start a new Lean client for the new `gameId`. + const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + game const uri = monaco.Uri.parse('file:///') this.leanClient = new LeanClient(socketUrl, undefined, uri, () => {}) } @@ -22,9 +27,9 @@ export class Connection { /** If not already started, starts the Lean client. resolves the returned promise as soon as a * Lean client is running. */ - startLeanClient = () => { + startLeanClient = (game) => { return new Promise((resolve) => { - const leanClient = this.getLeanClient() + const leanClient = this.getLeanClient(game) if (leanClient.isRunning()) { resolve(leanClient) } else { @@ -47,8 +52,8 @@ export const connection = new Connection() export const ConnectionContext = React.createContext(null); -export const useLeanClient = () => { - const leanClient = connection.getLeanClient() +export const useLeanClient = (gameId) => { + const leanClient = connection.getLeanClient(gameId) const [leanClientStarted, setLeanClientStarted] = useState(leanClient.isStarted()) React.useEffect(() => { diff --git a/client/src/index.tsx b/client/src/index.tsx index d13b276..eedeb12 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -13,21 +13,26 @@ import ErrorPage from './ErrorPage'; import Welcome from './components/Welcome'; import Level from './components/Level'; import { monacoSetup } from 'lean4web/client/src/monacoSetup'; +import { redirect } from 'react-router-dom'; monacoSetup() const router = createHashRouter([ { path: "/", + loader: () => redirect("/game/testgame") + }, + { + path: "/game/:gameId", element: , errorElement: , children: [ { - path: "/", + path: "/game/:gameId", element: , }, { - path: "/world/:worldId/level/:levelId", + path: "/game/:gameId/world/:worldId/level/:levelId", element: , }, ], diff --git a/client/src/state/api.ts b/client/src/state/api.ts index 581823c..6d93733 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -38,13 +38,13 @@ interface Doc { const customBaseQuery = async ( - args : {method: string, params?: any}, + args : {game: string, method: string, params?: any}, { signal, dispatch, getState, extra }, extraOptions ) => { try { const connection : Connection = extra.connection - let leanClient = await connection.startLeanClient() + let leanClient = await connection.startLeanClient(args.game) console.log(`Sending request ${args.method}`) let res = await leanClient.sendRequest(args.method, args.params) console.log('Received response', res) @@ -59,14 +59,14 @@ export const apiSlice = createApi({ reducerPath: 'gameApi', baseQuery: customBaseQuery, endpoints: (builder) => ({ - getGameInfo: builder.query({ - query: () => {return {method: 'info', params: {}}}, + getGameInfo: builder.query({ + query: ({game}) => {return {game, method: 'info', params: {}}}, }), - loadLevel: builder.query({ - query: ({world, level}) => {return {method: "loadLevel", params: {world, level}}}, + loadLevel: builder.query({ + query: ({game, world, level}) => {return {game, method: "loadLevel", params: {world, level}}}, }), - loadDoc: builder.query({ - query: ({name, type}) => {return {method: "loadDoc", params: {name, type}}}, + loadDoc: builder.query({ + query: ({game, name, type}) => {return {game, method: "loadDoc", params: {name, type}}}, }), }), }) diff --git a/server/index.mjs b/server/index.mjs index a07dab6..4e80f8a 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -6,6 +6,18 @@ import * as url from 'url'; import * as rpc from 'vscode-ws-jsonrpc'; import * as jsonrpcserver from 'vscode-ws-jsonrpc/server'; +const games = { + testgame: { + name: "TestGame", + module: "TestGame", + queueLength: 5 + }, + nng: { + name: "NNG", + module: "NNG", + queueLength: 5 + } +} const __filename = url.fileURLToPath(import.meta.url); const __dirname = url.fileURLToPath(new URL('.', import.meta.url)); @@ -23,23 +35,18 @@ const wss = new WebSocketServer({ server }) const environment = process.env.NODE_ENV const isDevelopment = environment === 'development' -let cmd, cmdArgs, cwd; -if (isDevelopment) { - cmd = "./gameserver"; - cmdArgs = ["--server"]; - cwd = "./leanserver/build/bin/" -} else{ - cmd = "docker"; - cmdArgs = ["run", "--runtime=runsc", "--network=none", "--rm", "-i", "testgame:latest"]; - cwd = "." -} - -/** We keep a queue of started Lean Server processes to be ready when a user arrives */ -const queue = [] +/** We keep queues of started Lean Server processes to be ready when a user arrives */ +const queue = {} const queueLength = 5 -function startServerProcess() { - const serverProcess = cp.spawn(cmd, cmdArgs, { cwd }) +function startServerProcess(gameId) { + const serverProcess = isDevelopment + ? cp.spawn("./gameserver", + ["--server", gameId, games[gameId].module, games[gameId].name], + { cwd: "./leanserver/build/bin/" }) + : cp.spawn("docker", + ["run", "--runtime=runsc", "--network=none", "--rm", "-i", `${gameId}:latest`], + { cwd: "." }) serverProcess.on('error', error => console.error(`Launching Lean Server failed: ${error}`) ); @@ -52,22 +59,32 @@ function startServerProcess() { } /** start Lean Server processes to refill the queue */ -function fillQueue() { - while (queue.length < queueLength) { - const serverProcess = startServerProcess() - queue.push(serverProcess) +function fillQueue(gameId) { + while (queue[gameId].length < games[gameId].queueLength) { + const serverProcess = startServerProcess(gameId) + queue[gameId].push(serverProcess) } } -fillQueue() +for (let gameId in games) { + queue[gameId] = [] + fillQueue(gameId) +} + +const urlRegEx = new RegExp("^/websocket/(.*)$") + +wss.addListener("connection", function(ws, req) { + const reRes = urlRegEx.exec(req.url) + if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; } + const gameId = reRes[1] + if (!games[gameId]) { console.error(`Unknown game: ${gameId}`); return; } -wss.addListener("connection", function(ws) { let ps; if (isDevelopment) { // Don't use queue in development - ps = startServerProcess() + ps = startServerProcess(gameId) } else { - ps = queue.shift() // Pick the first Lean process; it's likely to be ready immediately - fillQueue() + ps = queue[gameId].shift() // Pick the first Lean process; it's likely to be ready immediately + fillQueue(gameId) } const socket = { diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean index 3326fa8..9075307 100644 --- a/server/leanserver/GameServer/FileWorker.lean +++ b/server/leanserver/GameServer/FileWorker.lean @@ -113,7 +113,7 @@ where addErrorMessage (info : SourceInfo) (s : MessageData) := open Elab Meta Expr in def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool) - (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams) : IO Snapshot := do + (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams): IO Snapshot := do -- Recognize end snap if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then let endSnap : Snapshot := { @@ -142,7 +142,7 @@ 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 some level ← GameServer.getLevelByFileName? inputCtx.fileName + let some level ← GameServer.getLevelByFileName? initParams inputCtx.fileName | throwError "Level not found: {inputCtx.fileName}" let scope := level.scope @@ -244,7 +244,8 @@ where hOut.writeLspNotification { method := "$/game/completed", param } /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/ - private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken) (levelParams : Game.DidOpenLevelParams) + private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken) + (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams) : AsyncElabM (Option Snapshot) := do cancelTk.check let s ← get @@ -261,7 +262,8 @@ where -- Make sure that there is at least one snap after the head snap, so that -- we can see the current goal even on an empty document let couldBeEndSnap := s.snaps.size > 1 - let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap levelParams + let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap + levelParams initParams set { s with snaps := s.snaps.push snap } -- TODO(MH): check for interrupt with increased precision cancelTk.check @@ -299,7 +301,7 @@ where publishIleanInfoUpdate m ctx.hOut snaps return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do IO.sleep startAfterMs - AsyncList.unfoldAsync (nextSnap ctx m cancelTk levelParams) { snaps }) + AsyncList.unfoldAsync (nextSnap ctx m cancelTk levelParams ctx.initParams) { snaps }) end Elab @@ -362,8 +364,9 @@ section Initialization fileMap := default def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool) - (levelModule : Name) : IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do - let gameDir := "../../../testgame" + (levelModule : Name) (initParams : InitializeParams): IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do + let some gameDir := GameServer.gameDirFromInitParams initParams + | throwServerError s!"Invalid rootUri: {initParams.rootUri?}" -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`. let out ← IO.Process.output @@ -426,7 +429,8 @@ section Initialization def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options) (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 + let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets) + levelParams.levelModule initParams let cancelTk ← CancelToken.new let ctx := { hIn := i @@ -506,6 +510,7 @@ section MainLoop set st match msg with | Message.request id method (some params) => + if method == "Game.getInteractiveGoals" then throwServerError "HELLO" handleRequest id method (toJson params) mainLoop levelParams | Message.notification "exit" none => diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean index 95942e3..4e3681b 100644 --- a/server/leanserver/GameServer/Game.lean +++ b/server/leanserver/GameServer/Game.lean @@ -83,9 +83,9 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do 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) + let some lvl ← GameServer.getLevelByFileName? c.initParams ((System.Uri.fileUriToPath? m.uri).getD m.uri |>.toString) | do - c.hLog.putStr s!"Level not found: {m.uri}" + c.hLog.putStr s!"Level not found: {m.uri} {c.initParams.rootUri?}" c.hLog.flush -- Send an extra notification to the file worker to inform it about the level data fw.stdin.writeLspNotification { diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean index 32f3931..78304a5 100644 --- a/server/leanserver/GameServer/RpcHandlers.lean +++ b/server/leanserver/GameServer/RpcHandlers.lean @@ -13,15 +13,26 @@ open Meta namespace GameServer -def levelIdFromFileName? (fileName : String) : Option LevelId := Id.run do +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 := fileParts[2]!.toNat? then - return some {game := `TestGame, world := fileParts[1]!, level := level} + if let (some level, some game) := (fileParts[2]!.toNat?, splitRootUri initParams 2) then + return some {game, world := fileParts[1]!, level := level} return none -def getLevelByFileName? [Monad m] [MonadEnv m] (fileName : String) : m (Option GameLevel) := do - let some levelId := levelIdFromFileName? fileName +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 return ← getLevel? levelId @@ -114,9 +125,9 @@ def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pu open Meta in /-- Find all hints whose trigger matches the current goal -/ -def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array GameHint) := do +def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do goal.withContext do - let some level ← getLevelByFileName? doc.meta.mkInputContext.fileName + let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName | throwError "Level not found: {doc.meta.mkInputContext.fileName}" let hints ← level.hints.filterMapM fun hint => do openAbstractCtxResult hint.goal fun hintFVars hintGoal => do @@ -137,6 +148,7 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array open RequestM in def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do let doc ← readDoc + let rc ← readThe RequestContext let text := doc.meta.text let hoverPos := text.lspPosToUtf8Pos p.position -- TODO: I couldn't find a good condition to find the correct snap. So we are looking @@ -152,7 +164,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio return List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore let goals ← ci.runMetaM {} do goals.mapM fun goal => do - let hints ← findHints goal doc + let hints ← findHints goal doc rc.initParams return ← goalToInteractive goal hints -- compute the goal diff -- let goals ← ciAfter.runMetaM {} (do diff --git a/server/leanserver/GameServer/Watchdog.lean b/server/leanserver/GameServer/Watchdog.lean index 039a730..8b6cfca 100644 --- a/server/leanserver/GameServer/Watchdog.lean +++ b/server/leanserver/GameServer/Watchdog.lean @@ -1,6 +1,7 @@ /- This file is mostly copied from `Lean/Server/Watchdog.lean`. -/ import Lean import GameServer.Game +import Lean.Server.Watchdog namespace MyServer.Watchdog open Lean @@ -76,9 +77,7 @@ def initAndRunWatchdogAux : GameServerM Unit := do catch _ => pure (Message.notification "exit" none) | throwServerError "Got `shutdown` request, expected an `exit` notification" -def createEnv : IO Environment := do - let gameDir := "../../../testgame" - +def createEnv (gameDir : String) (module : String) : IO Environment := 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"] } @@ -93,11 +92,17 @@ def createEnv : IO Environment := do -- 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 := module : Import }] {} 0 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" + let gameId := args[1]! + let gameDir := s!"../../../{gameId}" + let module := args[2]! + let gameName := args[3]! let workerPath := "./gameserver" -- TODO: Do the following commands slow us down? let srcSearchPath ← initSrcSearchPath (← getBuildDir) @@ -106,8 +111,11 @@ 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, game := `TestGame} + let state := {env := ← createEnv gameDir module, game := gameName} let initRequest ← i.readLspRequestAs "initialize" InitializeParams + -- We misuse the `rootUri` field to store gameId, module, and gameName + let rootUri? := s!"{gameId}/{module}/{gameName}" + let initRequest := {initRequest with param := {initRequest.param with rootUri?}} o.writeLspResponse { id := initRequest.id result := { diff --git a/server/leanserver/Main.lean b/server/leanserver/Main.lean index 993172c..39964b7 100644 --- a/server/leanserver/Main.lean +++ b/server/leanserver/Main.lean @@ -8,7 +8,7 @@ unsafe def main : List String → IO UInt32 := fun args => do Lean.enableInitializersExecution if args[0]? == some "--server" then - MyServer.Watchdog.watchdogMain [] + MyServer.Watchdog.watchdogMain args else if args[0]? == some "--worker" then MyServer.FileWorker.workerMain {} else diff --git a/server/server.Dockerfile b/server/server.Dockerfile index e056a94..a054176 100644 --- a/server/server.Dockerfile +++ b/server/server.Dockerfile @@ -12,4 +12,4 @@ RUN rm -f ./build/bin/gameserver RUN lake build WORKDIR /leanserver/build/bin/ -CMD ["./gameserver", "--server"] +CMD ["./gameserver", "--server", "testgame", "TestGame", "TestGame"]