From bf2315b4743b4cec1b10f0b5a31e3decebab27e8 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 23 Mar 2023 15:14:05 +0100 Subject: [PATCH 1/4] 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"] From 7992cffa265bef90332cb3d9c3a51d81515c7819 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 23 Mar 2023 15:23:12 +0100 Subject: [PATCH 2/4] add minimal NNG dummy --- server/nng/.gitignore | 1 + server/nng/NNG.lean | 9 +++++++++ server/nng/lake-manifest.json | 3 +++ server/nng/lakefile.lean | 11 +++++++++++ server/nng/lean-toolchain | 1 + 5 files changed, 25 insertions(+) create mode 100644 server/nng/.gitignore create mode 100644 server/nng/NNG.lean create mode 100644 server/nng/lake-manifest.json create mode 100644 server/nng/lakefile.lean create mode 100644 server/nng/lean-toolchain diff --git a/server/nng/.gitignore b/server/nng/.gitignore new file mode 100644 index 0000000..c795b05 --- /dev/null +++ b/server/nng/.gitignore @@ -0,0 +1 @@ +build \ No newline at end of file diff --git a/server/nng/NNG.lean b/server/nng/NNG.lean new file mode 100644 index 0000000..88032ba --- /dev/null +++ b/server/nng/NNG.lean @@ -0,0 +1,9 @@ +import GameServer.Commands + +Game "NNG" +World "HelloWorld" +Level 1 + +Statement : 1 + 1 = 2 := rfl + +MakeGame \ No newline at end of file diff --git a/server/nng/lake-manifest.json b/server/nng/lake-manifest.json new file mode 100644 index 0000000..fee354b --- /dev/null +++ b/server/nng/lake-manifest.json @@ -0,0 +1,3 @@ +{"version": 4, + "packagesDir": "lake-packages", + "packages": [{"path": {"name": "GameServer", "dir": "./../leanserver"}}]} diff --git a/server/nng/lakefile.lean b/server/nng/lakefile.lean new file mode 100644 index 0000000..9ff2130 --- /dev/null +++ b/server/nng/lakefile.lean @@ -0,0 +1,11 @@ +import Lake +open Lake DSL + +require GameServer from ".."/"leanserver" + +package NNG + +@[default_target] +lean_lib NNG { + moreLeanArgs := #["-DautoImplicit=false"] +} diff --git a/server/nng/lean-toolchain b/server/nng/lean-toolchain new file mode 100644 index 0000000..7f0fd43 --- /dev/null +++ b/server/nng/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2023-03-09 From dac15d84b5500c5005f0a4fe40039c4e001b89b0 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 23 Mar 2023 15:54:47 +0100 Subject: [PATCH 3/4] add build mechanism for nng --- UPDATE_LEAN.sh | 4 ++++ package.json | 2 +- server/build.sh | 12 +++++++++++- server/index.mjs | 3 ++- server/server.Dockerfile | 4 ++-- 5 files changed, 20 insertions(+), 5 deletions(-) diff --git a/UPDATE_LEAN.sh b/UPDATE_LEAN.sh index 3ea0fe4..899dbbc 100755 --- a/UPDATE_LEAN.sh +++ b/UPDATE_LEAN.sh @@ -10,6 +10,10 @@ lake update cp lake-packages/mathlib/lean-toolchain lean-toolchain cp lake-packages/mathlib/lean-toolchain ../leanserver/lean-toolchain +cp lake-packages/mathlib/lean-toolchain ../nng/lean-toolchain cd ../leanserver lake update + +cd ../nng +lake update diff --git a/package.json b/package.json index a230586..ebe5cdc 100644 --- a/package.json +++ b/package.json @@ -56,7 +56,7 @@ }, "scripts": { "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"", - "start_server": "cd server && (cd leanserver && lake build) && (cd testgame && lake exe cache get && lake build) && NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"", + "start_server": "cd server && (cd leanserver && lake build) && (cd testgame && lake exe cache get && lake build) && (cd nng && 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/build.sh b/server/build.sh index bc3f11a..3b85690 100755 --- a/server/build.sh +++ b/server/build.sh @@ -6,6 +6,16 @@ cd $(dirname $0) # Build elan image if not already present docker build --pull --rm -f elan.Dockerfile -t elan:latest . +# Build testgame (cd testgame && lake exe cache get && lake build) docker rmi testgame:latest || true -docker build --rm -f server.Dockerfile -t testgame:latest . +docker build \ + --build-arg GAME_DIR=testgame \ + --rm -f server.Dockerfile -t testgame:latest . + +# Build NNG +(cd nng && lake build) +docker rmi nng:latest || true +docker build \ + --build-arg GAME_DIR=nng \ + --rm -f server.Dockerfile -t nng:latest . diff --git a/server/index.mjs b/server/index.mjs index 4e80f8a..756987c 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -45,7 +45,8 @@ function startServerProcess(gameId) { ["--server", gameId, games[gameId].module, games[gameId].name], { cwd: "./leanserver/build/bin/" }) : cp.spawn("docker", - ["run", "--runtime=runsc", "--network=none", "--rm", "-i", `${gameId}:latest`], + ["run", "--runtime=runsc", "--network=none", "--rm", "-i", `${gameId}:latest`, + "./gameserver", "--server", gameId, games[gameId].module, games[gameId].name], { cwd: "." }) serverProcess.on('error', error => console.error(`Launching Lean Server failed: ${error}`) diff --git a/server/server.Dockerfile b/server/server.Dockerfile index a054176..304b16b 100644 --- a/server/server.Dockerfile +++ b/server/server.Dockerfile @@ -1,10 +1,11 @@ +ARG GAME_DIR FROM elan:latest WORKDIR / # Copy lean files COPY leanserver ./leanserver -COPY testgame ./testgame +COPY $GAME_DIR ./$GAME_DIR # TODO: make `testgame` a build argument WORKDIR /leanserver @@ -12,4 +13,3 @@ RUN rm -f ./build/bin/gameserver RUN lake build WORKDIR /leanserver/build/bin/ -CMD ["./gameserver", "--server", "testgame", "TestGame", "TestGame"] From cbc9576f98372645ecdd371805aa146a1e443a6c Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 23 Mar 2023 16:21:57 +0100 Subject: [PATCH 4/4] add support for multiple games in redux state --- client/src/components/Level.tsx | 14 +++---- client/src/components/Welcome.tsx | 2 +- client/src/components/infoview/main.tsx | 6 ++- client/src/state/localStorage.ts | 2 +- client/src/state/progress.ts | 50 +++++++++++++------------ 5 files changed, 40 insertions(+), 34 deletions(-) diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 9e44489..513a8ed 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -76,8 +76,9 @@ function PlayableLevel({worldId, levelId}) { const codeviewRef = useRef(null) const introductionPanelRef = useRef(null) - const initialCode = useAppSelector(selectCode(worldId, levelId)) - const initialSelections = useAppSelector(selectSelections(worldId, levelId)) + const gameId = React.useContext(GameIdContext) + const initialCode = useAppSelector(selectCode(gameId, worldId, levelId)) + const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId)) const [commandLineMode, setCommandLineMode] = useState(true) const [commandLineInput, setCommandLineInput] = useState("") @@ -126,14 +127,13 @@ function PlayableLevel({worldId, levelId}) { }]); } - const gameId = React.useContext(GameIdContext) const gameInfo = useGetGameInfoQuery({game: gameId}) const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) const dispatch = useAppDispatch() const onDidChangeContent = (code) => { - dispatch(codeEdited({world: worldId, level: levelId, code})) + dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code})) setCanUndo(code.trim() !== "") } @@ -142,10 +142,10 @@ function PlayableLevel({worldId, levelId}) { const selections = monacoSelections.map( ({selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}) => {return {selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}}) - dispatch(changedSelection({world: worldId, level: levelId, selections})) + dispatch(changedSelection({game: gameId, world: worldId, level: levelId, selections})) } - const completed = useAppSelector(selectCompleted(worldId, levelId)) + const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) const {editor, infoProvider, editorConnection} = useLevelEditor(worldId, levelId, codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) @@ -408,7 +408,7 @@ function useLoadWorldFiles(worldId) { if (model) { models.push(model) } else { - const code = selectCode(worldId, levelId)(store.getState()) + const code = selectCode(gameId, worldId, levelId)(store.getState()) models.push(monaco.editor.createModel(code, 'lean4', uri)) } } diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx index c5fce54..5fb36f3 100644 --- a/client/src/components/Welcome.tsx +++ b/client/src/components/Welcome.tsx @@ -19,7 +19,7 @@ import { GameIdContext } from '../App'; function LevelIcon({ worldId, levelId, position }) { const gameId = React.useContext(GameIdContext) - const completed = useSelector(selectCompleted(worldId,levelId)) + const completed = useSelector(selectCompleted(gameId, worldId,levelId)) // TODO: relative positioning? return ( diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 369bdf7..39075bd 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -19,10 +19,12 @@ import { WithRpcSessions } from '../../../../node_modules/lean4-infoview/src/inf import { ServerVersion } from '../../../../node_modules/lean4-infoview/src/infoview/serverVersion'; import { useAppDispatch, useAppSelector } from '../../hooks'; import { levelCompleted, selectCompleted } from '../../state/progress'; +import { GameIdContext } from '../../App'; export function Main(props: {world: string, level: number}) { const ec = React.useContext(EditorContext); + const gameId = React.useContext(GameIdContext) const dispatch = useAppDispatch() @@ -33,13 +35,13 @@ export function Main(props: {world: string, level: number}) { if (ec.events.changedCursorLocation.current && ec.events.changedCursorLocation.current.uri === params.uri) { - dispatch(levelCompleted({world: props.world, level: props.level})) + dispatch(levelCompleted({game: gameId, world: props.world, level: props.level})) } }, [] ); - const completed = useAppSelector(selectCompleted(props.world, props.level)) + const completed = useAppSelector(selectCompleted(gameId, props.world, props.level)) /* Set up updates to the global infoview state on editor events. */ const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig; diff --git a/client/src/state/localStorage.ts b/client/src/state/localStorage.ts index a290d75..729d84d 100644 --- a/client/src/state/localStorage.ts +++ b/client/src/state/localStorage.ts @@ -1,4 +1,4 @@ -const KEY = "progress"; +const KEY = "game_progress"; export function loadState() { try { const serializedState = localStorage.getItem(KEY); diff --git a/client/src/state/progress.ts b/client/src/state/progress.ts index 6005d4f..3d0a29c 100644 --- a/client/src/state/progress.ts +++ b/client/src/state/progress.ts @@ -3,7 +3,7 @@ import type { PayloadAction } from '@reduxjs/toolkit' import { loadState } from "./localStorage"; interface ProgressState { - level: {[world: string]: {[level: number]: LevelProgressState}} + level: {[game: string]: {[world: string]: {[level: number]: LevelProgressState}}} } interface Selection { selectionStartLineNumber: number, @@ -20,12 +20,15 @@ interface LevelProgressState { const initialProgressState = loadState() ?? { level: {} } as ProgressState const initalLevelProgressState = {code: "", completed: false} as LevelProgressState -function addLevelProgress(state, action: PayloadAction<{world: string, level: number}>) { - if (!state.level[action.payload.world]) { - state.level[action.payload.world] = {} +function addLevelProgress(state, action: PayloadAction<{game: string, world: string, level: number}>) { + if (!state.level[action.payload.game]) { + state.level[action.payload.game] = {} } - if (!state.level[action.payload.world][action.payload.level]) { - state.level[action.payload.world][action.payload.level] = {...initalLevelProgressState} + if (!state.level[action.payload.game][action.payload.world]) { + state.level[action.payload.game][action.payload.world] = {} + } + if (!state.level[action.payload.game][action.payload.world][action.payload.level]) { + state.level[action.payload.game][action.payload.world][action.payload.level] = {...initalLevelProgressState} } } @@ -33,45 +36,46 @@ export const progressSlice = createSlice({ name: 'progress', initialState: initialProgressState, reducers: { - codeEdited(state, action: PayloadAction<{world: string, level: number, code: string}>) { + codeEdited(state, action: PayloadAction<{game: string, world: string, level: number, code: string}>) { addLevelProgress(state, action) - state.level[action.payload.world][action.payload.level].code = action.payload.code - state.level[action.payload.world][action.payload.level].completed = false + state.level[action.payload.game][action.payload.world][action.payload.level].code = action.payload.code + state.level[action.payload.game][action.payload.world][action.payload.level].completed = false }, - changedSelection(state, action: PayloadAction<{world: string, level: number, selections: Selection[]}>) { + changedSelection(state, action: PayloadAction<{game: string, world: string, level: number, selections: Selection[]}>) { addLevelProgress(state, action) - state.level[action.payload.world][action.payload.level].selections = action.payload.selections + state.level[action.payload.game][action.payload.world][action.payload.level].selections = action.payload.selections }, - levelCompleted(state, action: PayloadAction<{world: string, level: number}>) { + levelCompleted(state, action: PayloadAction<{game: string, world: string, level: number}>) { addLevelProgress(state, action) - state.level[action.payload.world][action.payload.level].completed = true + state.level[action.payload.game][action.payload.world][action.payload.level].completed = true }, } }) -export function selectLevel(world: string, level: number) { +export function selectLevel(game: string, world: string, level: number) { return (state) =>{ - if (!state.progress.level[world]) { return initalLevelProgressState } - if (!state.progress.level[world][level]) { return initalLevelProgressState } - return state.progress.level[world][level] + if (!state.progress.level[game]) { return initalLevelProgressState } + if (!state.progress.level[game][world]) { return initalLevelProgressState } + if (!state.progress.level[game][world][level]) { return initalLevelProgressState } + return state.progress.level[game][world][level] } } -export function selectCode(world: string, level: number) { +export function selectCode(game: string, world: string, level: number) { return (state) => { - return selectLevel(world, level)(state).code + return selectLevel(game, world, level)(state).code } } -export function selectSelections(world: string, level: number) { +export function selectSelections(game: string, world: string, level: number) { return (state) => { - return selectLevel(world, level)(state).selections + return selectLevel(game, world, level)(state).selections } } -export function selectCompleted(world: string, level: number) { +export function selectCompleted(game: string, world: string, level: number) { return (state) => { - return selectLevel(world, level)(state).completed + return selectLevel(game, world, level)(state).completed } }