Merge branch 'main' of github.com:leanprover-community/lean4game

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

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<string>(undefined);
+
 function App() {
+  const params = useParams();
   return (
     <div className="app">
+      <GameIdContext.Provider value={params.gameId}>
         <Outlet />
+      </GameIdContext.Provider>
     </div>
   )
 }

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 gameId = React.useContext(GameIdContext)
-  const doc = useLoadDocQuery({type: type, name: name})
+  const doc = useLoadDocQuery({game: gameId, type: type, name: name})
 
   return <>
     <h2 className="doc">{doc.data?.displayName}</h2>

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<monaco.editor.IStandaloneCodeEditor>(null as any);
 
@@ -75,8 +76,9 @@ function PlayableLevel({worldId, levelId}) {
   const codeviewRef = useRef<HTMLDivElement>(null)
   const introductionPanelRef = useRef<HTMLDivElement>(null)
 
-  const initialCode = useAppSelector(selectCode(worldId, levelId))
+  const gameId = React.useContext(GameIdContext)
-  const initialSelections = useAppSelector(selectSelections(worldId, levelId))
+  const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
+  const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
 
   const [commandLineMode, setCommandLineMode] = useState(true)
   const [commandLineInput, setCommandLineInput] = useState("")
@@ -125,14 +127,13 @@ function PlayableLevel({worldId, levelId}) {
     }]);
   }
 
-  const gameInfo = useGetGameInfoQuery()
+  const gameInfo = useGetGameInfoQuery({game: gameId})
-
+  const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
-  const level = useLoadLevelQuery({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() !== "")
   }
@@ -141,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)
@@ -209,8 +210,8 @@ function PlayableLevel({worldId, levelId}) {
             <Markdown>{level?.data?.conclusion}</Markdown>
           </div>
           {levelId >= gameInfo.data?.worldSize[worldId] ?
-          <Button to={`/`}><FontAwesomeIcon icon={faHome} /></Button> :
+          <Button to={`/game/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
-          <Button to={`/world/${worldId}/level/${levelId + 1}`}>
+          <Button to={`/game/${gameId}/world/${worldId}/level/${levelId + 1}`}>
             Next&nbsp;<FontAwesomeIcon icon={faArrowRight} /></Button>}
 
         </div>}
@@ -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 <>
     <div style={gameInfo.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
@@ -245,8 +247,8 @@ function Introduction({worldId}) {
       </div>
       <div className="conclusion">
         {0 == gameInfo.data?.worldSize[worldId] ?
-        <Button to={`/`}><FontAwesomeIcon icon={faHome} /></Button> :
+        <Button to={`/game/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
-        <Button to={`/world/${worldId}/level/1`}>
+        <Button to={`/game/${gameId}/world/${worldId}/level/1`}>
           Start&nbsp;<FontAwesomeIcon icon={faArrowRight} />
         </Button>}
       </div>
@@ -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 <div className="app-bar" style={isLoading ? {display: "none"} : null} >
     <div>
-    <Button to={`/`}><FontAwesomeIcon icon={faHome} /></Button>
+    <Button to={`/game/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button>
       <span className="app-bar-title">
         {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
       </span>
@@ -269,10 +272,10 @@ function LevelAppBar({isLoading, levelId, worldId, levelTitle}) {
         {levelTitle}
       </span>
       <Button disabled={levelId <= 0} inverted={true}
-        to={`/world/${worldId}/level/${levelId - 1}`}
+        to={`/game/${gameId}/world/${worldId}/level/${levelId - 1}`}
         ><FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous</Button>
       <Button disabled={levelId >= gameInfo.data?.worldSize[worldId]} inverted={true}
-        to={`/world/${worldId}/level/${levelId + 1}`}
+        to={`/game/${gameId}/world/${worldId}/level/${levelId + 1}`}
         >Next&nbsp;<FontAwesomeIcon icon={faArrowRight} /></Button>
     </div>
 
@@ -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<monaco.editor.IStandaloneCodeEditor|null>(null)
   const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(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(() => {
@@ -403,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))
         }
       }

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 completed = useSelector(selectCompleted(worldId,levelId))
+  const gameId = React.useContext(GameIdContext)
+  const completed = useSelector(selectCompleted(gameId, worldId,levelId))
   // TODO: relative positioning?
   return (
-    <Link to={`/world/${worldId}/level/${levelId}`} key={`/world/${worldId}/level/${levelId}`}>
+    <Link to={`/game/${gameId}/${worldId}/level/${levelId}`} key={`/game/${gameId}/world/${worldId}/level/${levelId}`}>
       <circle fill={completed ? "green" :"#aaa"} cx={position.x + Math.sin(levelId/5) * 9} cy={position.y - Math.cos(levelId/5) * 9} r="0.8" />
     </Link>
   )
@@ -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(
-        <Link key={`world${id}`} to={`/world/${id}/level/0`}>
+        <Link key={`world${id}`} to={`/game/${gameId}/world/${id}/level/0`}>
           <circle className="world-circle" cx={position.x} cy={position.y} r="8" />
           <text className="world-name"
             x={position.x} y={position.y}>{nodes[id].data.title ? nodes[id].data.title : id}</text>

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;

client/src/connection.ts

@@ -6,12 +6,17 @@ import { useState } from 'react';
 
 
 export class Connection {
-  private leanClient = null
+  private game: string = undefined // We only keep a connection to a single game at a time
-
+  private leanClient: LeanClient = null
-  getLeanClient(): LeanClient {
-    if (this.leanClient === null) {
-      const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/'
 
+  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<LeanClient>((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 = () => {
+export const useLeanClient = (gameId) => {
-  const leanClient = connection.getLeanClient()
+  const leanClient = connection.getLeanClient(gameId)
   const [leanClientStarted, setLeanClientStarted] = useState(leanClient.isStarted())
 
   React.useEffect(() => {

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: <App />,
     errorElement: <ErrorPage />,
     children: [
       {
-        path: "/",
+        path: "/game/:gameId",
         element: <Welcome />,
       },
       {
-        path: "/world/:worldId/level/:levelId",
+        path: "/game/:gameId/world/:worldId/level/:levelId",
         element: <Level />,
       },
     ],

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<GameInfo, void>({
+    getGameInfo: builder.query<GameInfo, {game: string}>({
-      query: () => {return {method: 'info', params: {}}},
+      query: ({game}) => {return {game, method: 'info', params: {}}},
     }),
-    loadLevel: builder.query<LevelInfo, {world: string, level: number}>({
+    loadLevel: builder.query<LevelInfo, {game: string, world: string, level: number}>({
-      query: ({world, level}) => {return {method: "loadLevel", params: {world, level}}},
+      query: ({game, world, level}) => {return {game, method: "loadLevel", params: {world, level}}},
     }),
-    loadDoc: builder.query<Doc, {name: string, type: "lemma"|"tactic"}>({
+    loadDoc: builder.query<Doc, {game: string, name: string, type: "lemma"|"tactic"}>({
-      query: ({name, type}) => {return {method: "loadDoc", params: {name, type}}},
+      query: ({game, name, type}) => {return {game, method: "loadDoc", params: {name, type}}},
     }),
   }),
 })

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);

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}>) {
+function addLevelProgress(state, action: PayloadAction<{game: string, world: string, level: number}>) {
-  if (!state.level[action.payload.world]) {
+  if (!state.level[action.payload.game]) {
-    state.level[action.payload.world] = {}
+    state.level[action.payload.game] = {}
   }
-  if (!state.level[action.payload.world][action.payload.level]) {
+  if (!state.level[action.payload.game][action.payload.world]) {
-    state.level[action.payload.world][action.payload.level] = {...initalLevelProgressState}
+    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.game][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].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[game]) { return initalLevelProgressState }
-    if (!state.progress.level[world][level]) { return initalLevelProgressState }
+    if (!state.progress.level[game][world]) { return initalLevelProgressState }
-    return state.progress.level[world][level]
+    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
   }
 }
 

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",

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 .

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,19 @@ const wss = new WebSocketServer({ server })
 const environment = process.env.NODE_ENV
 const isDevelopment = environment === 'development'
 
-let cmd, cmdArgs, cwd;
+/** We keep queues of started Lean Server processes to be ready when a user arrives */
-if (isDevelopment) {
+const queue = {}
-    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 = []
 const queueLength = 5
 
-function startServerProcess() {
+function startServerProcess(gameId) {
-    const serverProcess = cp.spawn(cmd, cmdArgs, { cwd })
+    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`,
+              "./gameserver", "--server", gameId, games[gameId].module, games[gameId].name],
+            { cwd: "." })
     serverProcess.on('error', error =>
         console.error(`Launching Lean Server failed: ${error}`)
     );
@@ -52,22 +60,32 @@ function startServerProcess() {
 }
 
 /** start Lean Server processes to refill the queue */
-function fillQueue() {
+function fillQueue(gameId) {
-    while (queue.length < queueLength) {
+    while (queue[gameId].length < games[gameId].queueLength) {
-        const serverProcess = startServerProcess()
+        const serverProcess = startServerProcess(gameId)
-        queue.push(serverProcess)
+        queue[gameId].push(serverProcess)
+    }
 }
+
+for (let gameId in games) {
+    queue[gameId] = []
+    fillQueue(gameId)
 }
 
-fillQueue()
+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
+        ps = queue[gameId].shift() // Pick the first Lean process; it's likely to be ready immediately
-        fillQueue()
+        fillQueue(gameId)
     }
 
     const socket = {

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
+    (levelModule : Name) (initParams : InitializeParams): IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
-    let gameDir := "../../../testgame"
+    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 =>

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 {

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
+    if let (some level, some game) := (fileParts[2]!.toNat?, splitRootUri initParams 2) then
-      return some {game := `TestGame, world := fileParts[1]!, level := level}
+      return some {game, world := fileParts[1]!, level := level}
   return none
 
-def getLevelByFileName? [Monad m] [MonadEnv m] (fileName : String) : m (Option GameLevel) := do
+def gameDirFromInitParams (initParams : Lsp.InitializeParams) : Option String :=
-  let some levelId := levelIdFromFileName? fileName
+  (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

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
+def createEnv (gameDir : String) (module : String) : IO Environment := do
-  let gameDir := "../../../testgame"
-
   -- 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 := module : Import }] {} 0
-  let env ← importModules [{ module := `Init : Import }, { module := gameName : 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 := {

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

server/nng/.gitignore

@@ -0,0 +1 @@
+build

server/nng/NNG.lean

@@ -0,0 +1,9 @@
+import GameServer.Commands
+
+Game "NNG"
+World "HelloWorld"
+Level 1
+
+Statement : 1 + 1 = 2 := rfl
+
+MakeGame

server/nng/lake-manifest.json

@@ -0,0 +1,3 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages": [{"path": {"name": "GameServer", "dir": "./../leanserver"}}]}

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"]
+}

server/nng/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-03-09

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"]