$/game/setInventory no longer needed

Mobile option (template)

client/src/app.tsx

@@ -12,8 +12,6 @@ import { MobileContext } from './components/infoview/context';
 import { useMobile } from './hooks';
 import { AUTO_SWITCH_THRESHOLD, getWindowDimensions} from './state/preferences';
 
-import { connection } from './connection';
-
 export const GameIdContext = React.createContext<string>(undefined);
 
 function App() {
@@ -38,10 +36,6 @@ function App() {
     }
   }, [lockMobile])
 
-  React.useEffect(() => {
-    connection.startLeanClient(gameId);
-  }, [gameId])
-
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>

client/src/components/infoview/main.tsx

@@ -493,18 +493,20 @@ export function TypewriterInterface({props}) {
                       <Markdown>{props.data?.introduction}</Markdown>
                     </div>
                   }
-                  {mobile && <>
+                  {mobile &&
                     <Hints key={`hints-${i}`}
                       hints={step.hints} showHidden={showHelp.has(i)} step={i}
                       selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
-                    {i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-                      <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
-                        Show more help!
-                      </Button>
-                    }
-                  </>
                   }
                   <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/>
+
+                  {mobile && i == proof.length - 1 &&
+                    hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
+                    <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
+                      Show more help!
+                    </Button>
+                  }
+
                   {/* Show a message that there are no goals left */}
                   {!step.goals.length && (
                     <div className="message information">
@@ -521,7 +523,7 @@ export function TypewriterInterface({props}) {
               }
             })}
             {mobile && completed &&
-              <div className="button-row">
+              <div className="button-row mobile">
                 {props.level >= props.worldSize ?
                   <Button to={`/${gameId}`}>
                     <FontAwesomeIcon icon={faHome} />&nbsp;Leave World

client/src/components/inventory.tsx

@@ -2,7 +2,8 @@ import * as React from 'react';
 import { useState, useEffect } from 'react';
 import '../css/inventory.css'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faLock, faBan } from '@fortawesome/free-solid-svg-icons'
+import { faLock, faBan, faCheck } from '@fortawesome/free-solid-svg-icons'
+import { faClipboard } from '@fortawesome/free-regular-svg-icons'
 import { GameIdContext } from '../app';
 import Markdown from './markdown';
 import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
@@ -10,10 +11,12 @@ import { selectDifficulty, selectInventory } from '../state/progress';
 import { store } from '../state/store';
 import { useSelector } from 'react-redux';
 
-export function Inventory({levelInfo, openDoc, enableAll=false} :
+export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=false} :
   {
     levelInfo: LevelInfo|InventoryOverview,
     openDoc: (props: {name: string, type: string}) => void,
+    lemmaTab: any,
+    setLemmaTab: any,
     enableAll?: boolean,
   }) {
 
@@ -31,19 +34,20 @@ export function Inventory({levelInfo, openDoc, enableAll=false} :
       }
       <h2>Theorems</h2>
       {levelInfo?.lemmas &&
-        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} defaultTab={levelInfo?.lemmaTab} level={levelInfo} enableAll={enableAll}/>
+        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} level={levelInfo} enableAll={enableAll} tab={lemmaTab} setTab={setLemmaTab}/>
       }
     </div>
   )
 }
 
-function InventoryList({items, docType, openDoc, defaultTab=null, level=undefined, enableAll=false} :
+function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, level=undefined, enableAll=false} :
   {
     items: InventoryTile[],
     docType: string,
     openDoc(props: {name: string, type: string}): void,
-    defaultTab? : string,
-    level? : LevelInfo|InventoryOverview,
+    tab?: any,
+    setTab?: any,
+    level?: LevelInfo|InventoryOverview,
     enableAll?: boolean,
   }) {
   // TODO: `level` is only used in the `useEffect` below to check if a new level has
@@ -59,8 +63,6 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
   }
   const categories = Array.from(categorySet).sort()
 
-  const [tab, setTab] = useState(defaultTab)
-
   // Add inventory items from local store as unlocked.
   // Items are unlocked if they are in the local store, or if the server says they should be
   // given the dependency graph. (OR-connection) (TODO: maybe add different logic for different
@@ -68,13 +70,6 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
   let inv: string[] = selectInventory(gameId)(store.getState())
   let modifiedItems : InventoryTile[] = items.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile)
 
-  useEffect(() => {
-    // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading.
-    // `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch.
-    if (defaultTab) {
-      setTab(defaultTab)
-    }}, [level])
-
   return <>
     {categories.length > 1 &&
       <div className="tab-bar">
@@ -89,21 +84,26 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
           (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
         ).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => {
             return <InventoryItem key={`${item.category}-${item.name}`}
+              item={item}
               showDoc={() => {openDoc({name: item.name, type: docType})}}
               name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false}
-              disabled={item.disabled} newly={item.new} enableAll={enableAll}/>
+              disabled={item.disabled} newly={item.new} enableAll={enableAll} />
         })
       }
     </div>
     </>
 }
 
-function InventoryItem({name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
+function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
   const icon = locked ? <FontAwesomeIcon icon={faLock} /> :
-               disabled ? <FontAwesomeIcon icon={faBan} /> : ""
+               disabled ? <FontAwesomeIcon icon={faBan} /> : item.st
   const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : ""
+  // Note: This is somewhat a hack as the statement of lemmas comes currently in the form
+  // `Namespace.statement_name (x y : Nat) : some type`
   const title = locked ? "Not unlocked yet" :
-                disabled ? "Not available in this level" : ""
+                disabled ? "Not available in this level" : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
+
+  const [copied, setCopied] = useState(false)
 
   const handleClick = () => {
     if (enableAll || !locked) {
@@ -111,7 +111,21 @@ function InventoryItem({name, displayName, locked, disabled, newly, showDoc, ena
     }
   }
 
-  return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>{icon} {displayName}</div>
+  const copyItemName = (ev) => {
+    navigator.clipboard.writeText(displayName)
+    setCopied(true)
+    setInterval(() => {
+      setCopied(false)
+    }, 3000);
+    ev.stopPropagation()
+  }
+
+return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>
+    {icon} {displayName}
+    <div className="copy-button" onClick={copyItemName}>
+      {copied ? <FontAwesomeIcon icon={faCheck} /> : <FontAwesomeIcon icon={faClipboard} />}
+    </div>
+  </div>
 }
 
 export function Documentation({name, type, handleClose}) {
@@ -131,16 +145,25 @@ export function Documentation({name, type, handleClose}) {
 export function InventoryPanel({levelInfo, visible = true}) {
   const gameId = React.useContext(GameIdContext)
 
+  const [lemmaTab, setLemmaTab] = useState(levelInfo?.lemmaTab)
+
   // The inventory is overlayed by the doc entry of a clicked item
   const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
   // Set `inventoryDoc` to `null` to close the doc
   function closeInventoryDoc() {setInventoryDoc(null)}
 
+    useEffect(() => {
+    // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading.
+    // `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch.
+    if (levelInfo?.lemmaTab) {
+      setLemmaTab(levelInfo?.lemmaTab)
+    }}, [levelInfo])
+
   return <div className={`column inventory-panel ${visible ? '' : 'hidden'}`}>
     {inventoryDoc ?
       <Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
       :
-      <Inventory levelInfo={levelInfo} openDoc={setInventoryDoc} enableAll={true}/>
+      <Inventory levelInfo={levelInfo} openDoc={setInventoryDoc} enableAll={true} lemmaTab={lemmaTab} setLemmaTab={setLemmaTab}/>
     }
   </div>
 }

client/src/components/level.tsx

@@ -18,7 +18,6 @@ import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-info
 import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event'
 
 import { GameIdContext } from '../app'
-import { ConnectionContext, connection, useLeanClient } from '../connection'
 import { useAppDispatch, useAppSelector } from '../hooks'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'
 import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited,
@@ -44,6 +43,15 @@ import 'lean4web/client/src/editor/infoview.css'
 import 'lean4web/client/src/editor/vscode.css'
 import '../css/level.css'
 import { LevelAppBar } from './app_bar'
+import { LeanClient } from 'lean4web/client/src/editor/leanclient'
+import { DisposingWebSocketMessageReader } from 'lean4web/client/src/reader'
+import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc'
+import { IConnectionProvider } from 'monaco-languageclient'
+import { monacoSetup } from 'lean4web/client/src/monacoSetup'
+import { onigasmH } from 'onigasm/lib/onigasmH'
+
+
+monacoSetup()
 
 function Level() {
   const params = useParams()
@@ -211,10 +219,8 @@ function PlayableLevel({impressum, setImpressum}) {
 
   const dispatch = useAppDispatch()
 
-  const difficulty = useSelector(selectDifficulty(gameId))
   const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
   const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
-  const inventory: Array<String> = useSelector(selectInventory(gameId))
 
   const typewriterMode = useSelector(selectTypewriterMode(gameId))
   const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
@@ -293,12 +299,6 @@ function PlayableLevel({impressum, setImpressum}) {
   // a hint at the beginning of the proof...
   const [selectedStep, setSelectedStep] = useState<number>()
 
-  // if the user inventory changes, notify the server
-  useEffect(() => {
-    let leanClient = connection.getLeanClient(gameId)
-    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty})
-  }, [inventory])
-
   useEffect (() => {
     // Lock editor mode
     if (level?.data?.template) {
@@ -372,7 +372,7 @@ function PlayableLevel({impressum, setImpressum}) {
 
   // Effect when command line mode gets enabled
   useEffect(() => {
-    if (editor && typewriterMode) {
+    if (onigasmH && editor && typewriterMode) {
       let code = editor.getModel().getLinesContent().filter(line => line.trim())
       editor.executeEdits("typewriter", [{
         range: editor.getModel().getFullModelRange(),
@@ -395,7 +395,7 @@ function PlayableLevel({impressum, setImpressum}) {
       //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
       // }
     }
-  }, [editor, typewriterMode])
+  }, [editor, typewriterMode, onigasmH == null])
 
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
@@ -441,6 +441,7 @@ function PlayableLevel({impressum, setImpressum}) {
 function IntroductionPanel({gameInfo}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId} = useContext(WorldLevelIdContext)
+  const {mobile} = React.useContext(MobileContext)
 
   let text: Array<string> = gameInfo.data?.worlds.nodes[worldId].introduction.split(/\n(\s*\n)+/)
 
@@ -451,7 +452,7 @@ function IntroductionPanel({gameInfo}) {
           hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
       ))}
     </div>
-    <div className="button-row">
+    <div className={`button-row${mobile ? ' mobile' : ''}`}>
       {gameInfo.data?.worldSize[worldId] == 0 ?
         <Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
         <Button to={`/${gameId}/world/${worldId}/level/1`}>
@@ -530,21 +531,32 @@ function Introduction({impressum, setImpressum}) {
 
 function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {
 
-  const connection = React.useContext(ConnectionContext)
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
 
-
   const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
   const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
-  const [infoviewApi, setInfoviewApi] = useState<null|InfoviewApi>(null)
   const [editorConnection, setEditorConnection] = useState<null|EditorConnection>(null)
 
-  // Create Editor
+  const uriStr = `file:///${worldId}/${levelId}`
+  const uri = monaco.Uri.parse(uriStr)
+
+  const inventory: Array<String> = useSelector(selectInventory(gameId))
+  const difficulty: number = useSelector(selectDifficulty(gameId))
+
   useEffect(() => {
+    const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri)
+    if (onDidChangeContent) {
+      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
+    }
+
     const editor = monaco.editor.create(codeviewRef.current!, {
+      model,
       glyphMargin: true,
       quickSuggestions: false,
+      lineDecorationsWidth: 5,
+      folding: false,
+      lineNumbers: 'on',
       lightbulb: {
         enabled: true
       },
@@ -556,11 +568,61 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
         enabled: false
       },
       lineNumbersMinChars: 3,
+      tabSize: 2,
       'semanticHighlighting.enabled': true,
       theme: 'vs-code-theme-converted'
     })
+    if (onDidChangeSelection) {
+      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
+    }
+    if (initialSelections) {
+      console.debug("Initial Selection: ", initialSelections)
+      // BUG: Somehow I get an `invalid arguments` bug here
+      // editor.setSelections(initialSelections)
+    }
+    setEditor(editor)
+    const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
 
-    const infoProvider = new InfoProvider(connection.getLeanClient(gameId))
+    const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + gameId
+
+    const connectionProvider : IConnectionProvider = {
+      get: async () => {
+        return await new Promise((resolve, reject) => {
+          console.log(`connecting ${socketUrl}`)
+          const websocket = new WebSocket(socketUrl)
+          websocket.addEventListener('error', (ev) => {
+            reject(ev)
+          })
+          websocket.addEventListener('message', (msg) => {
+            // console.log(msg.data)
+          })
+          websocket.addEventListener('open', () => {
+            const socket = toSocket(websocket)
+            const reader = new DisposingWebSocketMessageReader(socket)
+            const writer = new WebSocketMessageWriter(socket)
+            resolve({
+              reader,
+              writer
+            })
+          })
+        })
+      }
+    }
+
+    // Following `vscode-lean4/webview/index.ts`
+    const client = new LeanClient(connectionProvider, showRestartMessage, {inventory, difficulty})
+    const infoProvider = new InfoProvider(client)
+    // const div: HTMLElement = infoviewRef.current!
+    const imports = {
+      '@leanprover/infoview': `${window.location.origin}/index.production.min.js`,
+      'react': `${window.location.origin}/react.production.min.js`,
+      'react/jsx-runtime': `${window.location.origin}/react-jsx-runtime.production.min.js`,
+      'react-dom': `${window.location.origin}/react-dom.production.min.js`,
+      'react-popper': `${window.location.origin}/react-popper.production.min.js`
+    }
+    // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi)
+    setInfoProvider(infoProvider)
+    client.restart()
 
     const editorApi = infoProvider.getApi()
 
@@ -605,54 +667,27 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
 
     setEditor(editor)
     setInfoProvider(infoProvider)
-    setInfoviewApi(infoviewApi)
 
-    return () => { infoProvider.dispose(); editor.dispose() }
-  }, [])
+    infoProvider.openPreview(editor, infoviewApi)
+    const taskgutter = new LeanTaskGutter(infoProvider.client, editor)
 
-  const {leanClient, leanClientStarted} = useLeanClient(gameId)
-  const uriStr = `file:///${worldId}/${levelId}`
-  const uri = monaco.Uri.parse(uriStr)
+    // TODO:
+    // setRestart(() => restart)
 
-  // Create model when level changes
-  useEffect(() => {
-    if (editor && leanClientStarted) {
-
-      let model = monaco.editor.getModel(uri)
-      if (!model) {
-        model = monaco.editor.createModel(initialCode, 'lean4', uri)
-      }
-      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
-      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
-      editor.setModel(model)
-      if (initialSelections) {
-        console.debug("Initial Selection: ", initialSelections)
-        // BUG: Somehow I get an `invalid arguments` bug here
-        // editor.setSelections(initialSelections)
-      }
-
-      return () => {
-        editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
-        model.dispose();
-      }
+    return () => {
+      editor.dispose();
+      model.dispose();
+      abbrevRewriter.dispose();
+      taskgutter.dispose();
+      infoProvider.dispose();
+      client.dispose();
     }
-  }, [editor, levelId, connection, leanClientStarted])
+  }, [gameId, worldId, levelId])
 
-
-  useEffect(() => {
-    if (editor && leanClientStarted) {
-
-      let model = monaco.editor.getModel(uri)
-      infoviewApi.serverRestarted(leanClient.initializeResult)
-
-      infoProvider.openPreview(editor, infoviewApi)
-
-      const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
-      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
-
-      return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
-    }
-  }, [editor, connection, leanClientStarted])
+  const showRestartMessage = () => {
+    // setRestartMessage(true)
+    console.log("TODO: SHOW RESTART MESSAGE")
+  }
 
   return {editor, infoProvider, editorConnection}
 }

client/src/components/world_tree.tsx

@@ -11,7 +11,7 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
-import { useAppDispatch } from '../hooks'
+import { useAppDispatch, useMobile } from '../hooks'
 import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
 import { store } from '../state/store'
 
@@ -197,13 +197,15 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
   const gameId = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
   const dispatch = useAppDispatch()
+  const { mobile } = useMobile()
+
 
   function label(x : number) {
     return x == 0 ? 'none' : x == 1 ? 'relaxed' : 'regular'
   }
 
 
-  return <nav className="world-selection-menu">
+  return <nav className={`world-selection-menu${mobile ? '' : ' desktop'}`}>
     <div className="slider-wrap">
       <span className="difficulty-label">Rules
         <FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
@@ -213,7 +215,7 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
         title="Game Rules"
         min={0} max={2}
         aria-label="Game Rules"
-        defaultValue={difficulty}
+        value={difficulty}
         marks={[
           {value: 0, label: label(0)},
           {value: 1, label: label(1)},

client/src/connection.ts

@@ -1,68 +0,0 @@
-/**
- *  @fileOverview todo
- */
-
-import * as React from 'react';
-import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
-import { LeanClient } from 'lean4web/client/src/editor/leanclient';
-
-export class Connection {
-  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, () => {})
-    }
-
-    return this.leanClient
-  }
-
-  /** If not already started, starts the Lean client. resolves the returned promise as soon as a
-   * Lean client is running.
-   */
-  startLeanClient = (game) => {
-    return new Promise<LeanClient>((resolve) => {
-      const leanClient = this.getLeanClient(game)
-      if (leanClient.isRunning()) {
-        resolve(leanClient)
-      } else {
-        if (!leanClient.isStarted()) {
-          leanClient.start()
-        }
-        leanClient.restarted(() => {
-          // This keep alive message is not recognized by the server,
-          // but it makes sure that the websocket connection does not
-          // time out after 60 seconds.
-          setInterval(() => {leanClient.sendNotification('$/keepAlive', {}) }, 5000)
-          resolve(leanClient)
-        })
-      }
-    })
-  }
-}
-
-export const connection = new Connection()
-
-export const ConnectionContext = React.createContext(null);
-
-export const useLeanClient = (gameId) => {
-  const leanClient = connection.getLeanClient(gameId)
-  const [leanClientStarted, setLeanClientStarted] = React.useState(leanClient.isStarted())
-
-  React.useEffect(() => {
-    const t1 = leanClient.restarted(() => { console.log("START"); setLeanClientStarted(true) })
-    const t2 = leanClient.stopped(() => { console.log("STOP"); setLeanClientStarted(false) })
-
-    return () => {t1.dispose(); t2.dispose()}
-  }, [leanClient, setLeanClientStarted])
-
-  return {leanClientStarted, leanClient}
-}

client/src/css/inventory.css

@@ -26,7 +26,11 @@
 .inventory .item {
   background: #fff;
   border: solid 1px #777;
-  padding: .1em .5em;
+  padding-left: .5rem;
+  padding-right: 1.0rem;
+  padding-top: .1rem;
+  padding-bottom: .1rem;
+  position: relative;
 }
 
 .inventory .item.locked {
@@ -72,3 +76,21 @@
   color: black;
   border-bottom: 0.3em solid #999;
 }
+
+
+.inventory .item .copy-button {
+	min-width: 3px;
+	min-height: 3px;
+	display: inline-block;
+	color: #ccc;
+	font-size: 0.6em;
+	padding-right: .2rem;
+	vertical-align: top;
+	position: absolute;
+	top: 0;
+	right: 0;
+	height: 100%;
+	width: 1rem;
+	align-items: end;
+	text-align: end;
+}

client/src/css/level.css

@@ -232,6 +232,20 @@ td code  {
   height: 100%;
 } */
 
+.button-row.mobile {
+  margin: .5rem;
+  padding-top: .2rem;
+}
+
+.button-row.mobile .btn {
+  padding: .5em;
+  border-radius: .2em;
+  width: 100%;
+  margin: 0;
+  text-align: center;
+}
+
+
 .typewriter-interface {
   display: flex;
   flex-flow: column;

client/src/css/world_tree.css

@@ -49,7 +49,6 @@ svg .disabled {
 }
 
 .world-selection-menu {
-  position: absolute;
   right: 1em;
   top: 1em;
   /* margin: 1em; */
@@ -60,6 +59,10 @@ svg .disabled {
   filter: drop-shadow(4px 4px 5px rgba(0,0,0,0.5));
 }
 
+.world-selection-menu.desktop {
+  position: absolute;
+}
+
 .world-selection-menu .btn, .welcome .btn {
   min-width: 5em;
   text-align: center;

client/src/index.tsx

@@ -1,7 +1,6 @@
 import * as React from 'react'
 import { createRoot } from 'react-dom/client'
 import App from './app'
-import { ConnectionContext, connection } from './connection'
 import { store } from './state/store'
 import { Provider } from 'react-redux'
 import type { RouteObject } from "react-router"
@@ -10,11 +9,8 @@ import ErrorPage from './components/error_page'
 import Welcome from './components/welcome'
 import LandingPage from './components/landing_page'
 import Level from './components/level'
-import { monacoSetup } from 'lean4web/client/src/monacoSetup'
 
 
-monacoSetup()
-
 
 // If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
 // `/g/local/game`. This is used for the devcontainer setup
@@ -61,9 +57,7 @@ const root = createRoot(container!);
 root.render(
   <React.StrictMode>
     <Provider store={store}>
-      <ConnectionContext.Provider value={connection}>
-        <RouterProvider router={router} />
-      </ConnectionContext.Provider>
+      <RouterProvider router={router} />
     </Provider>
   </React.StrictMode>
 );

client/src/state/api.ts

@@ -35,6 +35,7 @@ export interface InventoryTile {
   locked: boolean,
   new: boolean,
   hidden: boolean
+  altTitle: string,
 }
 
 export interface LevelInfo {

client/src/state/store.ts

@@ -19,11 +19,7 @@ export const store = configureStore({
   },
   // Make connection available in thunks:
   middleware: getDefaultMiddleware =>
-    getDefaultMiddleware({
-      thunk: {
-        extraArgument: { connection }
-      }
-    }).concat(apiSlice.middleware),
+    getDefaultMiddleware().concat(apiSlice.middleware),
 });
 
 /**

package-lock.json

@@ -13,6 +13,10 @@
         "@emotion/styled": "^11.10.5",
         "@fontsource/roboto": "^4.5.8",
         "@fontsource/roboto-mono": "^4.5.8",
+        "@fortawesome/fontawesome-svg-core": "^6.5.1",
+        "@fortawesome/free-regular-svg-icons": "^6.5.1",
+        "@fortawesome/free-solid-svg-icons": "^6.5.1",
+        "@fortawesome/react-fontawesome": "^0.2.0",
         "@leanprover/infoview": "^0.4.3",
         "@mui/icons-material": "^5.11.0",
         "@mui/material": "^5.11.1",
@@ -27,7 +31,7 @@
         "debounce": "^1.2.1",
         "express": "^4.18.2",
         "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-        "lean4web": "github:hhu-adam/lean4web",
+        "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
         "octokit": "^2.0.14",
         "path-browserify": "^1.0.1",
         "react": "^18.2.0",
@@ -2221,231 +2225,6 @@
       "resolved": "https://registry.npmjs.org/@emotion/weak-memoize/-/weak-memoize-0.3.1.tgz",
       "integrity": "sha512-EsBwpc7hBUJWAsNPBmJy4hxWx12v6bshQsldrVmjxJoc3isbxhOrF2IcCpaXxfvq03NwkI7sbsOLXbYuqF/8Ww=="
     },
-    "node_modules/@esbuild/android-arm": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/android-arm/-/android-arm-0.18.20.tgz",
-      "integrity": "sha512-fyi7TDI/ijKKNZTUJAQqiG5T7YjJXgnzkURqmGj13C6dCqckZBLdl4h7bkhHt/t0WP+zO9/zwroDvANaOqO5Sw==",
-      "cpu": [
-        "arm"
-      ],
-      "optional": true,
-      "os": [
-        "android"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/android-arm64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/android-arm64/-/android-arm64-0.18.20.tgz",
-      "integrity": "sha512-Nz4rJcchGDtENV0eMKUNa6L12zz2zBDXuhj/Vjh18zGqB44Bi7MBMSXjgunJgjRhCmKOjnPuZp4Mb6OKqtMHLQ==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "android"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/android-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/android-x64/-/android-x64-0.18.20.tgz",
-      "integrity": "sha512-8GDdlePJA8D6zlZYJV/jnrRAi6rOiNaCC/JclcXpB+KIuvfBN4owLtgzY2bsxnx666XjJx2kDPUmnTtR8qKQUg==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "android"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/darwin-arm64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/darwin-arm64/-/darwin-arm64-0.18.20.tgz",
-      "integrity": "sha512-bxRHW5kHU38zS2lPTPOyuyTm+S+eobPUnTNkdJEfAddYgEcll4xkT8DB9d2008DtTbl7uJag2HuE5NZAZgnNEA==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "darwin"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/darwin-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/darwin-x64/-/darwin-x64-0.18.20.tgz",
-      "integrity": "sha512-pc5gxlMDxzm513qPGbCbDukOdsGtKhfxD1zJKXjCCcU7ju50O7MeAZ8c4krSJcOIJGFR+qx21yMMVYwiQvyTyQ==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "darwin"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/freebsd-arm64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/freebsd-arm64/-/freebsd-arm64-0.18.20.tgz",
-      "integrity": "sha512-yqDQHy4QHevpMAaxhhIwYPMv1NECwOvIpGCZkECn8w2WFHXjEwrBn3CeNIYsibZ/iZEUemj++M26W3cNR5h+Tw==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "freebsd"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/freebsd-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/freebsd-x64/-/freebsd-x64-0.18.20.tgz",
-      "integrity": "sha512-tgWRPPuQsd3RmBZwarGVHZQvtzfEBOreNuxEMKFcd5DaDn2PbBxfwLcj4+aenoh7ctXcbXmOQIn8HI6mCSw5MQ==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "freebsd"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-arm": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-arm/-/linux-arm-0.18.20.tgz",
-      "integrity": "sha512-/5bHkMWnq1EgKr1V+Ybz3s1hWXok7mDFUMQ4cG10AfW3wL02PSZi5kFpYKrptDsgb2WAJIvRcDm+qIvXf/apvg==",
-      "cpu": [
-        "arm"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-arm64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-arm64/-/linux-arm64-0.18.20.tgz",
-      "integrity": "sha512-2YbscF+UL7SQAVIpnWvYwM+3LskyDmPhe31pE7/aoTMFKKzIc9lLbyGUpmmb8a8AixOL61sQ/mFh3jEjHYFvdA==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-ia32": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-ia32/-/linux-ia32-0.18.20.tgz",
-      "integrity": "sha512-P4etWwq6IsReT0E1KHU40bOnzMHoH73aXp96Fs8TIT6z9Hu8G6+0SHSw9i2isWrD2nbx2qo5yUqACgdfVGx7TA==",
-      "cpu": [
-        "ia32"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-loong64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-loong64/-/linux-loong64-0.18.20.tgz",
-      "integrity": "sha512-nXW8nqBTrOpDLPgPY9uV+/1DjxoQ7DoB2N8eocyq8I9XuqJ7BiAMDMf9n1xZM9TgW0J8zrquIb/A7s3BJv7rjg==",
-      "cpu": [
-        "loong64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-mips64el": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-mips64el/-/linux-mips64el-0.18.20.tgz",
-      "integrity": "sha512-d5NeaXZcHp8PzYy5VnXV3VSd2D328Zb+9dEq5HE6bw6+N86JVPExrA6O68OPwobntbNJ0pzCpUFZTo3w0GyetQ==",
-      "cpu": [
-        "mips64el"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-ppc64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-ppc64/-/linux-ppc64-0.18.20.tgz",
-      "integrity": "sha512-WHPyeScRNcmANnLQkq6AfyXRFr5D6N2sKgkFo2FqguP44Nw2eyDlbTdZwd9GYk98DZG9QItIiTlFLHJHjxP3FA==",
-      "cpu": [
-        "ppc64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-riscv64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-riscv64/-/linux-riscv64-0.18.20.tgz",
-      "integrity": "sha512-WSxo6h5ecI5XH34KC7w5veNnKkju3zBRLEQNY7mv5mtBmrP/MjNBCAlsM2u5hDBlS3NGcTQpoBvRzqBcRtpq1A==",
-      "cpu": [
-        "riscv64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-s390x": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-s390x/-/linux-s390x-0.18.20.tgz",
-      "integrity": "sha512-+8231GMs3mAEth6Ja1iK0a1sQ3ohfcpzpRLH8uuc5/KVDFneH6jtAJLFGafpzpMRO6DzJ6AvXKze9LfFMrIHVQ==",
-      "cpu": [
-        "s390x"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
     "node_modules/@esbuild/linux-x64": {
       "version": "0.18.20",
       "resolved": "https://registry.npmjs.org/@esbuild/linux-x64/-/linux-x64-0.18.20.tgz",
@@ -2461,96 +2240,6 @@
         "node": ">=12"
       }
     },
-    "node_modules/@esbuild/netbsd-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/netbsd-x64/-/netbsd-x64-0.18.20.tgz",
-      "integrity": "sha512-iO1c++VP6xUBUmltHZoMtCUdPlnPGdBom6IrO4gyKPFFVBKioIImVooR5I83nTew5UOYrk3gIJhbZh8X44y06A==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "netbsd"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/openbsd-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/openbsd-x64/-/openbsd-x64-0.18.20.tgz",
-      "integrity": "sha512-e5e4YSsuQfX4cxcygw/UCPIEP6wbIL+se3sxPdCiMbFLBWu0eiZOJ7WoD+ptCLrmjZBK1Wk7I6D/I3NglUGOxg==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "openbsd"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/sunos-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/sunos-x64/-/sunos-x64-0.18.20.tgz",
-      "integrity": "sha512-kDbFRFp0YpTQVVrqUd5FTYmWo45zGaXe0X8E1G/LKFC0v8x0vWrhOWSLITcCn63lmZIxfOMXtCfti/RxN/0wnQ==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "sunos"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/win32-arm64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/win32-arm64/-/win32-arm64-0.18.20.tgz",
-      "integrity": "sha512-ddYFR6ItYgoaq4v4JmQQaAI5s7npztfV4Ag6NrhiaW0RrnOXqBkgwZLofVTlq1daVTQNhtI5oieTvkRPfZrePg==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/win32-ia32": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/win32-ia32/-/win32-ia32-0.18.20.tgz",
-      "integrity": "sha512-Wv7QBi3ID/rROT08SABTS7eV4hX26sVduqDOTe1MvGMjNd3EjOz4b7zeexIR62GTIEKrfJXKL9LFxTYgkyeu7g==",
-      "cpu": [
-        "ia32"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/win32-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/win32-x64/-/win32-x64-0.18.20.tgz",
-      "integrity": "sha512-kTdfRcSiDfQca/y9QIkng02avJ+NCaQvrMejlsB3RRv5sE9rRoeBPISaZpKxHELzRxZyLvNts1P27W3wV+8geQ==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
     "node_modules/@floating-ui/core": {
       "version": "1.5.0",
       "resolved": "https://registry.npmjs.org/@floating-ui/core/-/core-1.5.0.tgz",
@@ -2596,33 +2285,45 @@
       "integrity": "sha512-KrJdmkqz6DszT2wV/bbhXef4r0hV3B0vw2mAqei8A2kRnvq+gcJLmmIeQ94vu9VEXrUQzos5M9lH1TAAXpRphw=="
     },
     "node_modules/@fortawesome/fontawesome-common-types": {
-      "version": "6.4.2",
-      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.4.2.tgz",
-      "integrity": "sha512-1DgP7f+XQIJbLFCTX1V2QnxVmpLdKdzzo2k8EmvDOePfchaIGQ9eCHj2up3/jNEbZuBqel5OxiaOJf37TWauRA==",
+      "version": "6.5.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.5.1.tgz",
+      "integrity": "sha512-GkWzv+L6d2bI5f/Vk6ikJ9xtl7dfXtoRu3YGE6nq0p/FFqA1ebMOAWg3XgRyb0I6LYyYkiAo+3/KrwuBp8xG7A==",
       "hasInstallScript": true,
       "engines": {
         "node": ">=6"
       }
     },
     "node_modules/@fortawesome/fontawesome-svg-core": {
-      "version": "6.4.2",
-      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-svg-core/-/fontawesome-svg-core-6.4.2.tgz",
-      "integrity": "sha512-gjYDSKv3TrM2sLTOKBc5rH9ckje8Wrwgx1CxAPbN5N3Fm4prfi7NsJVWd1jklp7i5uSCVwhZS5qlhMXqLrpAIg==",
+      "version": "6.5.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-svg-core/-/fontawesome-svg-core-6.5.1.tgz",
+      "integrity": "sha512-MfRCYlQPXoLlpem+egxjfkEuP9UQswTrlCOsknus/NcMoblTH2g0jPrapbcIb04KGA7E2GZxbAccGZfWoYgsrQ==",
       "hasInstallScript": true,
       "dependencies": {
-        "@fortawesome/fontawesome-common-types": "6.4.2"
+        "@fortawesome/fontawesome-common-types": "6.5.1"
+      },
+      "engines": {
+        "node": ">=6"
+      }
+    },
+    "node_modules/@fortawesome/free-regular-svg-icons": {
+      "version": "6.5.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/free-regular-svg-icons/-/free-regular-svg-icons-6.5.1.tgz",
+      "integrity": "sha512-m6ShXn+wvqEU69wSP84coxLbNl7sGVZb+Ca+XZq6k30SzuP3X4TfPqtycgUh9ASwlNh5OfQCd8pDIWxl+O+LlQ==",
+      "hasInstallScript": true,
+      "dependencies": {
+        "@fortawesome/fontawesome-common-types": "6.5.1"
       },
       "engines": {
         "node": ">=6"
       }
     },
     "node_modules/@fortawesome/free-solid-svg-icons": {
-      "version": "6.4.2",
-      "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.4.2.tgz",
-      "integrity": "sha512-sYwXurXUEQS32fZz9hVCUUv/xu49PEJEyUOsA51l6PU/qVgfbTb2glsTEaJngVVT8VqBATRIdh7XVgV1JF1LkA==",
+      "version": "6.5.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.5.1.tgz",
+      "integrity": "sha512-S1PPfU3mIJa59biTtXJz1oI0+KAXW6bkAb31XKhxdxtuXDiUIFsih4JR1v5BbxY7hVHsD1RKq+jRkVRaf773NQ==",
       "hasInstallScript": true,
       "dependencies": {
-        "@fortawesome/fontawesome-common-types": "6.4.2"
+        "@fortawesome/fontawesome-common-types": "6.5.1"
       },
       "engines": {
         "node": ">=6"
@@ -2838,9 +2539,9 @@
       }
     },
     "node_modules/@leanprover/infoview": {
-      "version": "0.4.3",
-      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.3.tgz",
-      "integrity": "sha512-SufdOr2myHAbZNUmobfQdAhsEC5H9ddi3KS0z1v/8riWSMm+yJk3u4LxVuzCmmSmV2QxFqtFzn5z+HQqj1Vo7g==",
+      "version": "0.4.4",
+      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.4.tgz",
+      "integrity": "sha512-OxHffFaHcEudLyBEWpicOl7TfXuTYxW5Sz1RkHdUINWJpQsQn60YDF5fNRKmSb0d/fm7p+LVeBvM273jvfR5wQ==",
       "dependencies": {
         "@leanprover/infoview-api": "~0.2.1",
         "@vscode/codicons": "^0.0.32",
@@ -5077,81 +4778,6 @@
         }
       }
     },
-    "node_modules/@swc/core-darwin-arm64": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-darwin-arm64/-/core-darwin-arm64-1.3.95.tgz",
-      "integrity": "sha512-VAuBAP3MNetO/yBIBzvorUXq7lUBwhfpJxYViSxyluMwtoQDhE/XWN598TWMwMl1ZuImb56d7eUsuFdjgY7pJw==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "darwin"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-darwin-x64": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-darwin-x64/-/core-darwin-x64-1.3.95.tgz",
-      "integrity": "sha512-20vF2rvUsN98zGLZc+dsEdHvLoCuiYq/1B+TDeE4oolgTFDmI1jKO+m44PzWjYtKGU9QR95sZ6r/uec0QC5O4Q==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "darwin"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-linux-arm-gnueabihf": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-linux-arm-gnueabihf/-/core-linux-arm-gnueabihf-1.3.95.tgz",
-      "integrity": "sha512-oEudEM8PST1MRNGs+zu0cx5i9uP8TsLE4/L9HHrS07Ck0RJ3DCj3O2fU832nmLe2QxnAGPwBpSO9FntLfOiWEQ==",
-      "cpu": [
-        "arm"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-linux-arm64-gnu": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-linux-arm64-gnu/-/core-linux-arm64-gnu-1.3.95.tgz",
-      "integrity": "sha512-pIhFI+cuC1aYg+0NAPxwT/VRb32f2ia8oGxUjQR6aJg65gLkUYQzdwuUmpMtFR2WVf7WVFYxUnjo4UyMuyh3ng==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-linux-arm64-musl": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-linux-arm64-musl/-/core-linux-arm64-musl-1.3.95.tgz",
-      "integrity": "sha512-ZpbTr+QZDT4OPJfjPAmScqdKKaT+wGurvMU5AhxLaf85DuL8HwUwwlL0n1oLieLc47DwIJEMuKQkYhXMqmJHlg==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
     "node_modules/@swc/core-linux-x64-gnu": {
       "version": "1.3.95",
       "resolved": "https://registry.npmjs.org/@swc/core-linux-x64-gnu/-/core-linux-x64-gnu-1.3.95.tgz",
@@ -5182,51 +4808,6 @@
         "node": ">=10"
       }
     },
-    "node_modules/@swc/core-win32-arm64-msvc": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-win32-arm64-msvc/-/core-win32-arm64-msvc-1.3.95.tgz",
-      "integrity": "sha512-YaP4x/aZbUyNdqCBpC2zL8b8n58MEpOUpmOIZK6G1SxGi+2ENht7gs7+iXpWPc0sy7X3YPKmSWMAuui0h8lgAA==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-win32-ia32-msvc": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-win32-ia32-msvc/-/core-win32-ia32-msvc-1.3.95.tgz",
-      "integrity": "sha512-w0u3HI916zT4BC/57gOd+AwAEjXeUlQbGJ9H4p/gzs1zkSHtoDQghVUNy3n/ZKp9KFod/95cA8mbVF9t1+6epQ==",
-      "cpu": [
-        "ia32"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-win32-x64-msvc": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-win32-x64-msvc/-/core-win32-x64-msvc-1.3.95.tgz",
-      "integrity": "sha512-5RGnMt0S6gg4Gc6QtPUJ3Qs9Un4sKqccEzgH/tj7V/DVTJwKdnBKxFZfgQ34OR2Zpz7zGOn889xwsFVXspVWNA==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
     "node_modules/@swc/counter": {
       "version": "0.1.2",
       "resolved": "https://registry.npmjs.org/@swc/counter/-/counter-0.1.2.tgz",
@@ -8535,19 +8116,6 @@
       "resolved": "https://registry.npmjs.org/fs.realpath/-/fs.realpath-1.0.0.tgz",
       "integrity": "sha512-OO0pH2lK6a0hZnAdau5ItzHPI6pUlvI7jMVnxUQRtw4owF2wk8lOSabtGDCTP4Ggrg2MbGnWO9X8K1t4+fGMDw=="
     },
-    "node_modules/fsevents": {
-      "version": "2.3.3",
-      "resolved": "https://registry.npmjs.org/fsevents/-/fsevents-2.3.3.tgz",
-      "integrity": "sha512-5xoDfX+fL7faATnagmWPpbFtwh/R77WmMMqqHGS65C3vvB0YHrgF+B1YmZ3441tMj5n63k0212XNoJwzlhffQw==",
-      "hasInstallScript": true,
-      "optional": true,
-      "os": [
-        "darwin"
-      ],
-      "engines": {
-        "node": "^8.16.0 || ^10.6.0 || >=11.0.0"
-      }
-    },
     "node_modules/function-bind": {
       "version": "1.1.1",
       "resolved": "https://registry.npmjs.org/function-bind/-/function-bind-1.1.1.tgz",
@@ -10513,7 +10081,8 @@
     },
     "node_modules/lean4web": {
       "version": "0.1.0",
-      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#6fc9c11179934cce7ca1f78140c57b6931186b42",
+      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
+      "integrity": "sha512-s9qYeXuMNBGDPKC5IuFTjV/j8tQCRkZr+poYKEWljrM95rsz4JHIvjdEt891fE9JhPDLSN+iXNRXwIOCT6FlMg==",
       "dependencies": {
         "@emotion/react": "^11.11.1",
         "@emotion/styled": "^11.11.0",
@@ -10522,7 +10091,7 @@
         "@fortawesome/fontawesome-svg-core": "^6.2.0",
         "@fortawesome/free-solid-svg-icons": "^6.2.0",
         "@fortawesome/react-fontawesome": "^0.2.0",
-        "@leanprover/infoview": "^0.4.3",
+        "@leanprover/infoview": "^0.4.4",
         "@mui/material": "^5.13.7",
         "@vitejs/plugin-react-swc": "^3.4.0",
         "express": "^4.18.2",

package.json

@@ -10,6 +10,10 @@
     "@emotion/styled": "^11.10.5",
     "@fontsource/roboto": "^4.5.8",
     "@fontsource/roboto-mono": "^4.5.8",
+    "@fortawesome/fontawesome-svg-core": "^6.5.1",
+    "@fortawesome/free-regular-svg-icons": "^6.5.1",
+    "@fortawesome/free-solid-svg-icons": "^6.5.1",
+    "@fortawesome/react-fontawesome": "^0.2.0",
     "@leanprover/infoview": "^0.4.3",
     "@mui/icons-material": "^5.11.0",
     "@mui/material": "^5.11.1",
@@ -24,7 +28,7 @@
     "debounce": "^1.2.1",
     "express": "^4.18.2",
     "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-    "lean4web": "github:hhu-adam/lean4web",
+    "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
     "octokit": "^2.0.14",
     "path-browserify": "^1.0.1",
     "react": "^18.2.0",

server/GameServer.lean

@@ -1,5 +1,4 @@
 import GameServer.FileWorker
-import GameServer.Watchdog
 import GameServer.Commands
 
 -- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`
@@ -10,13 +9,9 @@ unsafe def main : List String → IO UInt32 := fun args => do
 
   Lean.enableInitializersExecution
 
+  -- TODO: remove this argument
   if args[0]? == some "--server" then
-    MyServer.Watchdog.watchdogMain args
-  else if args[0]? == some "--worker" then
-    MyServer.FileWorker.workerMain {}
+    MyServer.FileWorker.workerMain {} args
   else
-    e.putStrLn s!"Expected `--server` or `--worker`"
+    e.putStrLn s!"Expected `--server`"
     return 1
-
-
--- TODO: Potentially it could be useful to pass in the `gameName` via the websocket connection

server/GameServer/Commands.lean

@@ -124,7 +124,7 @@ elab "CoverImage" t:str : command => do
 
 /-! # Inventory
 
-The inventory contains docs for tactics, lemmas, and definitions. These are all locked
+The inventory contains docs for tactics, theorems, and definitions. These are all locked
 in the first level and get enabled during the game.
 -/
 
@@ -147,22 +147,22 @@ elab doc:docComment ? "TacticDoc" name:ident content:str ? : command => do
     displayName := name.getId.toString
     content := doc })
 
-/-- Documentation entry of a lemma. Example:
+/-- Documentation entry of a theorem. Example:
 
 ```
-LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
+TheoremDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 ```
 
-* The first identifier is used in the commands `[New/Only/Disabled]Lemma`.
-  It is preferably the true name of the lemma. However, this is not required.
+* The first identifier is used in the commands `[New/Only/Disabled]Theorem`.
+  It is preferably the true name of the theorem. However, this is not required.
 * The string following `as` is the displayed name (in the Inventory).
-* The identifier after `in` is the category to group lemmas by (in the Inventory).
+* The identifier after `in` is the category to group theorems by (in the Inventory).
 * The description is a string supporting Markdown.
 
 Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
-The lemma/definition to have the same fully qualified name as in mathlib.
+The theorem/definition to have the same fully qualified name as in mathlib.
  -/
-elab doc:docComment ? "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str ? :
+elab doc:docComment ? "TheoremDoc" name:ident "as" displayName:str "in" category:str content:str ? :
     command => do
   let doc ← parseDocCommentLegacy doc content
   modifyEnv (inventoryTemplateExt.addEntry · {
@@ -172,7 +172,7 @@ elab doc:docComment ? "LemmaDoc" name:ident "as" displayName:str "in" category:s
     displayName := displayName.getString
     content := doc })
 -- TODO: Catch the following behaviour.
--- 1. if `LemmaDoc` appears in the same file as `Statement`, it will silently use
+-- 1. if `TheoremDoc` appears in the same file as `Statement`, it will silently use
 -- it but display the info that it wasn't found in `Statement`
 -- 2. if it appears in a later file, however, it will silently not do anything and keep
 -- the first one.
@@ -190,7 +190,7 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
 * The description is a string supporting Markdown.
 
 Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
-The lemma/definition to have the same fully qualified name as in mathlib.
+The theorem/definition to have the same fully qualified name as in mathlib.
  -/
 elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:str ? : command => do
   let doc ← parseDocCommentLegacy doc template
@@ -202,8 +202,13 @@ elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:s
 
 /-! ## Add inventory items -/
 
+def checkCommandNotDuplicated (items : Array Name) (cmd := "Command") : CommandElabM Unit := do
+  if ¬ items.isEmpty then
+    logWarning s!"You should only use one `{cmd}` per level, but it takes multiple arguments: `{cmd} obj₁ obj₂ obj₃`!"
+
 /-- Declare tactics that are introduced by this level. -/
 elab "NewTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.new) "NewTactic"
   for name in ↑args do
     checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]")
   modifyCurLevel fun level => pure {level with
@@ -211,14 +216,16 @@ elab "NewTactic" args:ident* : command => do
 
 /-- Declare tactics that are introduced by this level but do not show up in inventory. -/
 elab "NewHiddenTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.hidden) "NewHiddenTactic"
   for name in ↑args do
     checkInventoryDoc .Tactic name (template := "")
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with new := level.tactics.new ++ args.map (·.getId),
                                    hidden := level.tactics.hidden ++ args.map (·.getId)}}
 
-/-- Declare lemmas that are introduced by this level. -/
-elab "NewLemma" args:ident* : command => do
+/-- Declare theorems that are introduced by this level. -/
+elab "NewTheorem" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewTheorem"
   for name in ↑args do
     try let _decl ← getConstInfo name.getId catch
       | _ => logErrorAt name m!"unknown identifier '{name}'."
@@ -228,6 +235,7 @@ elab "NewLemma" args:ident* : command => do
 
 /-- Declare definitions that are introduced by this level. -/
 elab "NewDefinition" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).definitions.new) "NewDefinition"
   for name in ↑args do checkInventoryDoc .Definition name -- TODO: Add (template := "[mathlib]")
   modifyCurLevel fun level => pure {level with
     definitions := {level.definitions with new := args.map (·.getId)}}
@@ -235,31 +243,36 @@ elab "NewDefinition" args:ident* : command => do
 /-- Declare tactics that are temporarily disabled in this level.
 This is ignored if `OnlyTactic` is set. -/
 elab "DisabledTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.disabled) "DisabledTactic"
   for name in ↑args do checkInventoryDoc .Tactic name
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with disabled := args.map (·.getId)}}
 
-/-- Declare lemmas that are temporarily disabled in this level.
-This is ignored if `OnlyLemma` is set. -/
-elab "DisabledLemma" args:ident* : command => do
+/-- Declare theorems that are temporarily disabled in this level.
+This is ignored if `OnlyTheorem` is set. -/
+elab "DisabledTheorem" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.disabled) "DisabledTheorem"
   for name in ↑args  do checkInventoryDoc .Lemma name
   modifyCurLevel fun level => pure {level with
     lemmas := {level.lemmas with disabled := args.map (·.getId)}}
 
 /-- Declare definitions that are temporarily disabled in this level -/
 elab "DisabledDefinition" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).definitions.disabled) "DisabledDefinition"
   for name in ↑args do checkInventoryDoc .Definition name
   modifyCurLevel fun level => pure {level with
     definitions := {level.definitions with disabled := args.map (·.getId)}}
 
 /-- Temporarily disable all tactics except the ones declared here -/
 elab "OnlyTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.only) "OnlyTactic"
   for name in ↑args do checkInventoryDoc .Tactic name
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with only := args.map (·.getId)}}
 
-/-- Temporarily disable all lemmas except the ones declared here -/
-elab "OnlyLemma" args:ident* : command => do
+/-- Temporarily disable all theorems except the ones declared here -/
+elab "OnlyTheorem" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyTheorem"
   for name in ↑args do checkInventoryDoc .Lemma name
   modifyCurLevel fun level => pure {level with
     lemmas := {level.lemmas with only := args.map (·.getId)}}
@@ -267,13 +280,56 @@ elab "OnlyLemma" args:ident* : command => do
 /-- Temporarily disable all definitions except the ones declared here.
 This is ignored if `OnlyDefinition` is set. -/
 elab "OnlyDefinition" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).definitions.only) "OnlyDefinition"
   for name in ↑args do checkInventoryDoc .Definition name
   modifyCurLevel fun level => pure {level with
     definitions := {level.definitions with only := args.map (·.getId)}}
 
-/-- Define which tab of Lemmas is opened by default. Usage: `LemmaTab "Nat"`.
+/-- Define which tab of Lemmas is opened by default. Usage: `TheoremTab "Nat"`.
 If omitted, the current tab will remain open. -/
-elab "LemmaTab"  category:str : command =>
+elab "TheoremTab"  category:str : command =>
+  modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
+
+
+/-! DEPRECATED -/
+
+elab doc:docComment ? "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str ? :
+    command => do
+  logWarning "Deprecated. Has been renamed to `TheoremDoc`"
+  let doc ← parseDocCommentLegacy doc content
+  modifyEnv (inventoryTemplateExt.addEntry · {
+    type := .Lemma
+    name := name.getId
+    category := category.getString
+    displayName := displayName.getString
+    content := doc })
+
+elab "NewLemma" args:ident* : command => do
+  logWarning "Deprecated. Has been renamed to `NewTheorem`"
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewLemma"
+  for name in ↑args do
+    try let _decl ← getConstInfo name.getId catch
+      | _ => logErrorAt name m!"unknown identifier '{name}'."
+    checkInventoryDoc .Lemma name -- TODO: Add (template := "[mathlib]")
+  modifyCurLevel fun level => pure {level with
+    lemmas := {level.lemmas with new := args.map (·.getId)}}
+
+elab "DisabledLemma" args:ident* : command => do
+  logWarning "Deprecated. Has been renamed to `DisabledTheorem`"
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.disabled) "DisabledLemma"
+  for name in ↑args  do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with
+    lemmas := {level.lemmas with disabled := args.map (·.getId)}}
+
+elab "OnlyLemma" args:ident* : command => do
+  logWarning "Deprecated. Has been renamed to `OnlyTheorem`"
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyLemma"
+  for name in ↑args do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with
+    lemmas := {level.lemmas with only := args.map (·.getId)}}
+
+elab "LemmaTab"  category:str : command => do
+  logWarning "Deprecated. Has been renamed to `TheoremTab`"
   modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
 
 /-! # Exercise Statement -/
@@ -781,6 +837,7 @@ elab "MakeGame" : command => do
               name := item
               displayName := data.displayName
               category := data.category
+              altTitle := data.statement
               hidden := hiddenItems.contains item })
 
 
@@ -800,6 +857,7 @@ elab "MakeGame" : command => do
             displayName := data.displayName
             category := data.category
             locked := false
+            altTitle := data.statement
             hidden := hiddenItems.contains item }
       itemsInWorld := itemsInWorld.insert worldId items
 
@@ -819,7 +877,8 @@ elab "MakeGame" : command => do
             displayName := data.displayName
             category := data.category
             locked := false
-            hidden := levelInfo.hidden.contains item }
+            altTitle := data.statement
+            hidden := hiddenItems.contains item }
 
         -- add the exercise statement from the previous level
         -- if it was named
@@ -832,6 +891,7 @@ elab "MakeGame" : command => do
               name := name
               displayName := data.displayName
               category := data.category
+              altTitle := data.statement
               locked := false }
 
         -- add marks for `disabled` and `new` lemmas here, so that they only apply to
@@ -851,4 +911,16 @@ elab "MakeGame" : command => do
           return level.setComputedInventory inventoryType itemsArray
     allItemsByType := allItemsByType.insert inventoryType allItems
 
-  saveGameData allItemsByType
+  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
+    (allItemsByType.findD type {}).toArray.mapM (fun name => do
+      let some item ← getInventoryItem? name type
+        | throwError "Expected item to exist: {name}"
+      return item.toTile)
+  let inventory : InventoryOverview := {
+    lemmas := (← getTiles .Lemma).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    tactics := (← getTiles .Tactic).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    definitions := (← getTiles .Definition).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    lemmaTab := none
+  }
+
+  saveGameData allItemsByType inventory

server/GameServer/EnvExtensions.lean

@@ -106,6 +106,8 @@ structure InventoryTile where
   new := false
   /-- hide the item in the inventory display -/
   hidden := false
+  /-- hover text -/
+  altTitle : String := default
 deriving ToJson, FromJson, Repr, Inhabited
 
 def InventoryItem.toTile (item : InventoryItem) : InventoryTile := {
@@ -291,6 +293,7 @@ structure LevelInfo where
   descrText : Option String := none
   descrFormat : String := ""
   lemmaTab : Option String
+  module : Name
   displayName : Option String
   statementName : Option String
   template : Option String
@@ -315,6 +318,7 @@ def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
       | some tile => tile.category
       | none => none
     statementName := lvl.statementName.toString
+    module := lvl.module
     displayName := match lvl.statementName with
       | .anonymous => none
       | name => match (inventoryExt.getState env).find?
@@ -379,7 +383,7 @@ structure GameTile where
 
   TODO: What's the format? -/
   image: String := default
-deriving Inhabited, ToJson
+deriving Inhabited, ToJson, FromJson
 
 structure Game where
   /-- Internal name of the game. -/
@@ -399,7 +403,7 @@ structure Game where
   tile : GameTile := default
   /-- The path to the background image of the world. -/
   image : String := default
-deriving Inhabited, ToJson
+deriving Inhabited, ToJson, FromJson
 
 def getGameJson (game : «Game») : Json := Id.run do
   let gameJson : Json := toJson game

server/GameServer/FileWorker.lean

@@ -1,7 +1,8 @@
-/- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/
+/- This file is adapted from `Lean/Server/FileWorker.lean`. -/
 import Lean.Server.FileWorker
 import GameServer.Game
 import GameServer.ImportModules
+import GameServer.SaveData
 
 namespace MyModule
 open Lean
@@ -17,7 +18,7 @@ private def mkEOI (pos : String.Pos) : Syntax :=
   mkNode ``Command.eoi #[atom]
 
 partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
-  (mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) :
+  (mps : ModuleParserState) (messages : MessageLog) :
     Syntax × ModuleParserState × MessageLog × String.Pos := Id.run do
   let mut pos := mps.pos
   let mut recovering := mps.recovering
@@ -56,6 +57,20 @@ open IO
 open Snapshots
 open JsonRpc
 
+structure GameWorkerState :=
+  inventory : Array String
+  /--
+  Check for tactics/theorems that are not unlocked.
+  0: no check
+  1: give warnings
+  2: give errors
+  -/
+  difficulty : Nat
+  levelInfo : LevelInfo
+  deriving ToJson, FromJson
+
+abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
+
 section Elab
 
 def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
@@ -73,29 +88,30 @@ def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : Me
 /-- Find all tactics in syntax object that are forbidden according to a
 set `allowed` of allowed tactics. -/
 partial def findForbiddenTactics (inputCtx : Parser.InputContext)
-    (levelParams : Game.DidOpenLevelParams) (stx : Syntax) :
+    (gameWorkerState : GameWorkerState) (stx : Syntax) :
     Elab.Command.CommandElabM Unit := do
+  let levelInfo := gameWorkerState.levelInfo
   match stx with
   | .missing => return ()
   | .node _info _kind args =>
     for arg in args do
-      findForbiddenTactics inputCtx levelParams arg
+      findForbiddenTactics inputCtx gameWorkerState arg
   | .atom info val =>
     -- ignore syntax elements that do not start with a letter
     -- and ignore "with" keyword
     let allowed := ["with", "fun", "at", "only", "by", "to"]
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      match levelParams.tactics.find? (·.name.toString == val) with
+      match levelInfo.tactics.find? (·.name.toString == val) with
       | none =>
         -- Note: This case means that the tactic will never be introduced in the game.
-        match levelParams.inventory.find? (· == val) with
+        match gameWorkerState.inventory.find? (· == val) with
         | none =>
           addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
         | some _ => pure () -- tactic is in the inventory, allow it.
       | some tac =>
         if tac.locked then
-          match levelParams.inventory.find? (· == val) with
+          match gameWorkerState.inventory.find? (· == val) with
           | none =>
             addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
           | some _ => pure () -- tactic is in the inventory, allow it.
@@ -109,10 +125,10 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
         let some (.thmInfo ..) := (← getEnv).find? n
           | return () -- not a theorem -> ignore
         -- Forbid the theorem we are proving currently
-        if n = levelParams.statementName then
+        if some n = levelInfo.statementName then
           addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
 
-        let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions
+        let lemmasAndDefs := levelInfo.lemmas ++ levelInfo.definitions
         match lemmasAndDefs.find? (fun l => l.name == n) with
         | none => addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
         | some lem =>
@@ -121,7 +137,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
           else if lem.disabled then
             addWarningMessage info s!"The lemma/definition '{n}' is disabled in this level!"
 where addWarningMessage (info : SourceInfo) (s : MessageData) :=
-  let difficulty := levelParams.difficulty
+  let difficulty := gameWorkerState.difficulty
   if difficulty > 0 then
     modify fun st => { st with
       messages := st.messages.add {
@@ -137,7 +153,7 @@ where addWarningMessage (info : SourceInfo) (s : MessageData) :=
 
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
-    (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams)
+    (couldBeEndSnap : Bool) (gameWorkerState : GameWorkerState)
     (initParams : Lsp.InitializeParams) : IO Snapshot := do
   -- Recognize end snap
   if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
@@ -168,7 +184,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
     Elab.Command.catchExceptions
       (getResetInfoTrees *> do
         let some level ← GameServer.getLevelByFileName? initParams inputCtx.fileName
-          | throwError "Level not found: {inputCtx.fileName}"
+          | panic! s!"Level not found: {inputCtx.fileName} / {GameServer.levelIdFromFileName? initParams inputCtx.fileName}"
         let scope := level.scope
 
         -- use open namespaces and options as in the level file
@@ -186,12 +202,12 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
             currNamespace := scope.currNamespace,
             openDecls := scope.openDecls }
           let (tacticStx, cmdParserState, msgLog, endOfWhitespace) :=
-            MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap
+            MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog
           modify (fun s => { s with messages := msgLog })
           parseResultRef.set (tacticStx, cmdParserState)
 
           -- Check for forbidden tactics
-          findForbiddenTactics inputCtx levelParams tacticStx
+          findForbiddenTactics inputCtx gameWorkerState tacticStx
 
           -- Insert invisible `skip` command to make sure we always display the initial goal
           let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]
@@ -219,6 +235,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
     }
 
   let (tacticStx, cmdParserState) ← parseResultRef.get
+  if tacticStx.isMissing then throwServerError "Tactic execution went wrong. No stx found."
 
   let postCmdSnap : Snapshot := {
     beginPos := tacticStx.getPos?.getD 0
@@ -270,7 +287,7 @@ where
 
   /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
   private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-      (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams)
+      (gameWorkerState : GameWorkerState) (initParams : Lsp.InitializeParams)
       : AsyncElabM (Option Snapshot) := do
     cancelTk.check
     let s ← get
@@ -288,7 +305,7 @@ where
     -- 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 initParams
+      gameWorkerState initParams
     set { s with snaps := s.snaps.push snap }
     -- TODO(MH): check for interrupt with increased precision
     cancelTk.check
@@ -310,7 +327,7 @@ where
 
   /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
   def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
-      (startAfterMs : UInt32) (levelParams : Game.DidOpenLevelParams)
+      (startAfterMs : UInt32) (gameWorkerState : GameWorkerState)
       : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
     let ctx ← read
     let some headerSnap := snaps[0]? | panic! "empty snapshots"
@@ -326,21 +343,15 @@ 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 ctx.initParams) { snaps })
+        AsyncList.unfoldAsync (nextSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
 
 end Elab
 
-structure GameWorkerState :=
-(levelParams : Game.DidOpenLevelParams)
-
-abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
-
 section Updates
 
 /-- Given the new document, updates editable doc state. -/
   def updateDocument (newMeta : DocumentMeta) : GameWorkerM Unit := do
     let s ← get
-    let levelParams := s.levelParams
     let ctx ← read
     let oldDoc := (← StateT.lift get).doc
     oldDoc.cancelTk.set
@@ -382,7 +393,7 @@ section Updates
           validSnaps := validSnaps.dropLast
       -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
       -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
-      unfoldSnaps newMeta validSnaps.toArray cancelTk levelParams ctx
+      unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx
         (startAfterMs := ctx.initParams.editDelay.toUInt32)
     StateT.lift <| modify fun st => { st with
       doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
@@ -397,24 +408,23 @@ section Initialization
     fileMap  := default
 
   def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-      (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) :
+      (gameDir : String) (module : Name):
       IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
     -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
     let out ← IO.Process.output
-      { cwd := levelParams.gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
+      { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
     if out.exitCode != 0 then
       throwServerError s!"Error while running Lake: {out.stderr}"
 
     -- Make the paths relative to the current directory
     let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
     let currentDir ← IO.currentDir
-    let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p
+    let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
 
     -- Set the search path
     Lean.searchPathRef.set paths
 
-    let env ← importModules' #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }]
-    -- return (env, paths)
+    let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }]
 
     -- use empty header
     let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
@@ -458,10 +468,11 @@ section Initialization
       return (headerSnap, srcSearchPath)
 
   def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
-       (levelParams : Game.DidOpenLevelParams) : IO (WorkerContext × WorkerState) := do
+      (gameDir : String) (gameWorkerState : GameWorkerState) : IO (WorkerContext × WorkerState) := do
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
+
     let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-      levelParams initParams
+      gameDir gameWorkerState.levelInfo.module
     let cancelTk ← CancelToken.new
     let ctx :=
       { hIn  := i
@@ -472,7 +483,7 @@ section Initialization
         clientHasWidgets
       }
     let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk levelParams ctx (startAfterMs := 0)
+      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
       | Except.error e   => throw (e : ElabTaskError))
     let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
     return (ctx,
@@ -509,6 +520,7 @@ section MessageHandling
     match method with
     | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
     | "$/cancelRequest"        => handle CancelParams (handleCancelRequest ·)
+    | "$/setTrace"        => pure ()
     | "$/lean/rpc/release"     => handle RpcReleaseParams (handleRpcRelease ·)
     | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
     | _                        => throwServerError s!"Got unsupported notification method: {method}"
@@ -547,26 +559,32 @@ section MainLoop
       let doc := st.doc
       doc.cancelTk.set
       return ()
-    | Message.notification "$/game/setInventory" params =>
-      let p := (← parseParams Game.SetInventoryParams (toJson params))
-      let s ← get
-
-      set {s with levelParams := {s.levelParams with
-        inventory := p.inventory,
-        difficulty := p.difficulty}}
+    | Message.request id "shutdown" none =>
+      ctx.hOut.writeLspResponse ⟨id, Json.null⟩
       mainLoop
     | Message.notification method (some params) =>
       handleNotification method (toJson params)
       mainLoop
-    | _ => throwServerError "Got invalid JSON-RPC message"
+    | _ => throwServerError s!"Got invalid JSON-RPC message: {toJson msg}"
 end MainLoop
 
-def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
+def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
-  let initParams ← i.readLspRequestAs "initialize" InitializeParams
+  let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
+  o.writeLspResponse {
+    id     := initRequest.id
+    result := {
+      capabilities := Watchdog.mkLeanServerCapabilities
+      serverInfo?  := some {
+        name     := "Lean 4 Game Server"
+        version? := "0.1.1"
+      }
+      : InitializeResult
+    }
+  }
+  discard $ i.readLspNotificationAs "initialized" InitializedParams
   let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
-  let ⟨_, levelParams⟩ ← i.readLspNotificationAs "$/game/didOpenLevel" Game.DidOpenLevelParams
 
   let doc := param.textDocument
   /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
@@ -578,9 +596,24 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
-    let (ctx, st) ← initializeWorker meta i o e initParams.param opts levelParams
+    let game ← loadGameData gameDir
+    -- TODO: We misuse the `rootUri` field to the gameName
+    let rootUri? : Option String := some (toString game.name)
+    let initParams := {initRequest.param.toLeanInternal with rootUri?}
+    let some (levelId : LevelId) := GameServer.levelIdFromFileName?
+        initParams meta.mkInputContext.fileName
+      | throwServerError s!"Could not determine level ID: {meta.mkInputContext.fileName}"
+    let levelInfo ← loadLevelData gameDir levelId.world levelId.level
+    let some initializationOptions := initRequest.param.initializationOptions?
+      | throwServerError "no initialization options found"
+    let gameWorkerState : GameWorkerState:= {
+      inventory := initializationOptions.inventory
+      difficulty := initializationOptions.difficulty
+      levelInfo
+    }
+    let (ctx, st) ← initializeWorker meta i o e initParams opts gameDir gameWorkerState
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
-      StateT.run (s := {levelParams := levelParams}) <| (mainLoop)
+      StateT.run (s := gameWorkerState) <| (mainLoop)
     return (0 : UInt32)
   catch e =>
     IO.eprintln e
@@ -590,12 +623,13 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
       message := e.toString }] o
     return (1 : UInt32)
 
-def workerMain (opts : Options) : IO UInt32 := do
+def workerMain (opts : Options) (args : List String): IO UInt32 := do
   let i ← IO.getStdin
   let o ← IO.getStdout
   let e ← IO.getStderr
   try
-    let exitCode ← initAndRunWorker i o e opts
+    let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
+    let exitCode ← initAndRunWorker i o e opts gameDir
     -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't
     -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code
     o.flush

server/GameServer/Game.lean

@@ -25,75 +25,56 @@ open Lsp
 open JsonRpc
 open IO
 
-structure DidOpenLevelParams where
-  uri : String
-  gameDir : String
-  levelModule : Name
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  inventory : Array String
-  /--
-  Check for tactics/theorems that are not unlocked.
-  0: no check
-  1: give warnings
-  2: give errors
-  -/
+/- Game-specific version of `InitializeParams` that allows for extra options: -/
+
+structure InitializationOptions extends Lean.Lsp.InitializationOptions :=
   difficulty : Nat
-  /-- The name of the theorem to be proven in this level. -/
-  statementName : Name
+  inventory : Array String
   deriving ToJson, FromJson
 
-structure SetInventoryParams where
-  inventory : Array String
-  difficulty : Nat
-deriving ToJson, FromJson
+structure InitializeParams where
+  processId? : Option Int := none
+  clientInfo? : Option ClientInfo := none
+  /- We don't support the deprecated rootPath
+  (rootPath? : Option String) -/
+  rootUri? : Option String := none
+  initializationOptions? : Option InitializationOptions := none
+  capabilities : ClientCapabilities
+  /-- If omitted, we default to off. -/
+  trace : Trace := Trace.off
+  workspaceFolders? : Option (Array WorkspaceFolder) := none
+  deriving ToJson
 
-def handleDidOpenLevel (params : Json) : GameServerM Unit := do
-  let p ← parseParams _ params
-  let m := p.textDocument
-  -- Execute the regular handling of the `didOpen` event
-  handleDidOpen p
-  let fw ← findFileWorker! m.uri
-  -- let s ← get
-  let c ← read
-  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.initParams.rootUri?}"
-      c.hLog.flush
-  -- Send an extra notification to the file worker to inform it about the level data
-  let s ← get
-  fw.stdin.writeLspNotification {
-    method := "$/game/didOpenLevel"
-    param  := {
-      uri := m.uri
-      gameDir := s.gameDir
-      levelModule := lvl.module
-      tactics := lvl.tactics.tiles
-      lemmas := lvl.lemmas.tiles
-      definitions := lvl.definitions.tiles
-      inventory := s.inventory
-      difficulty := s.difficulty
-      statementName := lvl.statementName
-      : DidOpenLevelParams
-    }
+instance : FromJson InitializeParams where
+  fromJson? j := do
+    let processId? := j.getObjValAs? Int "processId"
+    let clientInfo? := j.getObjValAs? ClientInfo "clientInfo"
+    let rootUri? := j.getObjValAs? String "rootUri"
+    let initializationOptions? := j.getObjValAs? InitializationOptions "initializationOptions"
+    let capabilities ← j.getObjValAs? ClientCapabilities "capabilities"
+    let trace := (j.getObjValAs? Trace "trace").toOption.getD Trace.off
+    let workspaceFolders? := j.getObjValAs? (Array WorkspaceFolder) "workspaceFolders"
+    return ⟨
+      processId?.toOption,
+      clientInfo?.toOption,
+      rootUri?.toOption,
+      initializationOptions?.toOption,
+      capabilities,
+      trace,
+      workspaceFolders?.toOption⟩
+
+def InitializeParams.toLeanInternal (p : InitializeParams) : Lean.Lsp.InitializeParams :=
+{
+  processId? := p.processId?
+  clientInfo? := p.clientInfo?
+  rootUri? := p.rootUri?
+  initializationOptions? := p.initializationOptions?.map fun o => {
+    editDelay? := o.editDelay?
+    hasWidgets? := o.hasWidgets?
   }
-
-partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
-  match ev with
-  | ServerEvent.clientMsg msg =>
-    match msg with
-    | Message.notification "$/game/setInventory" params =>
-      let p := (← parseParams SetInventoryParams (toJson params))
-      let s ← get
-      set {s with inventory := p.inventory, difficulty := p.difficulty}
-      let st ← read
-      let workers ← st.fileWorkersRef.get
-      for (_, fw) in workers do
-        fw.stdin.writeLspMessage msg
-
-      return true
-    | _ => return false
-  | _ => return false
+  capabilities := p.capabilities
+  trace := p.trace
+  workspaceFolders? := p.workspaceFolders?
+}
 
 end Game

server/GameServer/Graph.lean

@@ -18,6 +18,14 @@ instance [ToJson β] : ToJson (Graph Name β) := {
   ]
 }
 
+-- Just a dummy implementation for now:
+instance : FromJson (Graph Name β) := {
+  fromJson? := fun _ => .ok {
+    nodes := {}
+    edges := {}
+  }
+}
+
 instance  : EmptyCollection (Graph α β) := ⟨default⟩
 
 def Graph.insertNode (g : Graph α β) (a : α) (b : β) :=

server/GameServer/RpcHandlers.lean

@@ -46,8 +46,8 @@ partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) :
   | .bvar i1, .bvar i2 => if i1 == i2 then bij else none
   | .fvar i1, .fvar i2 => bij.insert? i1 i2
   | .mvar _, .mvar _ => bij
-  | .sort u1, .sort u2 => bij -- TODO?
-  | .const n1 ls1, .const n2 ls2 =>
+  | .sort _u1, .sort _u2 => bij -- TODO?
+  | .const n1 _ls1, .const n2 _ls2 =>
     if n1 == n2 then bij else none -- && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
   | .app f1 a1, .app f2 a2 =>
     some bij

server/GameServer/SaveData.lean

@@ -22,15 +22,21 @@ def copyImages : IO Unit := do
         let content ← readBinFile file
         writeBinFile outFile content
 
+namespace GameData
+  def gameDataPath : System.FilePath := ".lake" / "gamedata"
+  def gameFileName := s!"game.json"
+  def docFileName := fun (inventoryType : InventoryType) (name : Name) => s!"doc__{inventoryType}__{name}.json"
+  def levelFileName := fun (worldId : Name) (levelId : Nat) => s!"level__{worldId}__{levelId}.json"
+  def inventoryFileName := s!"inventory.json"
+end GameData
 
--- TODO: I'm not sure this should be happening here...
-#eval IO.FS.createDirAll ".lake/gamedata/"
-
+open GameData in
 -- TODO: register all of this as ToJson instance?
-def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do
+def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
+    (inventory : InventoryOverview): CommandElabM Unit := do
   let game ← getCurGame
   let env ← getEnv
-  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
+  let path := (← IO.currentDir) / gameDataPath
 
   if ← path.isDir then
     IO.FS.removeDirAll path
@@ -41,25 +47,32 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : Comma
 
   for (worldId, world) in game.worlds.nodes.toArray do
     for (levelId, level) in world.levels.toArray do
-      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
+      IO.FS.writeFile (path / levelFileName worldId levelId) (toString (toJson (level.toInfo env)))
 
-  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
+  IO.FS.writeFile (path / gameFileName) (toString (getGameJson game))
 
   for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
     for name in allItemsByType.findD inventoryType {} do
       let some item ← getInventoryItem? name inventoryType
         | throwError "Expected item to exist: {name}"
-      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
+      IO.FS.writeFile (path / docFileName inventoryType name) (toString (toJson item))
 
-  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
-    (allItemsByType.findD type {}).toArray.mapM (fun name => do
-      let some item ← getInventoryItem? name type
-        | throwError "Expected item to exist: {name}"
-      return item.toTile)
-  let inventory : InventoryOverview := {
-    lemmas := ← getTiles .Lemma
-    tactics := ← getTiles .Tactic
-    definitions := ← getTiles .Definition
-    lemmaTab := none
-  }
-  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))
+  IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
+
+open GameData
+
+def loadData (f : System.FilePath) (α : Type) [FromJson α] : IO α := do
+  let str ← IO.FS.readFile f
+  let json ← match Json.parse str with
+  | .ok v => pure v
+  | .error e => throw (IO.userError e)
+  let data ← match fromJson? json with
+  | .ok v => pure v
+  | .error e => throw (IO.userError e)
+  return data
+
+def loadGameData (gameDir : System.FilePath) : IO Game :=
+  loadData (gameDir / gameDataPath / gameFileName) Game
+
+def loadLevelData (gameDir : System.FilePath) (worldId : Name) (levelId : Nat) : IO LevelInfo :=
+  loadData (gameDir / gameDataPath / levelFileName worldId levelId) LevelInfo

server/GameServer/Watchdog.lean

@@ -1,158 +0,0 @@
-/- This file is mostly copied from `Lean/Server/Watchdog.lean`. -/
-import Lean.Server.Watchdog
-import GameServer.Game
-
-namespace MyServer.Watchdog
-open Lean
-open Server
-open Watchdog
-open IO
-open Lsp
-open JsonRpc
-open System.Uri
-
-  partial def mainLoop (clientTask : Task ServerEvent) : GameServerM Unit := do
-    let st ← read
-    let workers ← st.fileWorkersRef.get
-    let mut workerTasks := #[]
-    for (_, fw) in workers do
-      if let WorkerState.running := fw.state then
-        workerTasks := workerTasks.push <| fw.commTask.map (ServerEvent.workerEvent fw)
-
-    let ev ← IO.waitAny (clientTask :: workerTasks.toList)
-
-    if ← Game.handleServerEvent ev then -- handle Game requests
-      mainLoop (←runClientTask)
-    else
-      match ev with
-      | ServerEvent.clientMsg msg =>
-        match msg with
-        | Message.request id "shutdown" _ =>
-          shutdown
-          st.hOut.writeLspResponse ⟨id, Json.null⟩
-        | Message.request id method (some params) =>
-          handleRequest id method (toJson params)
-          mainLoop (←runClientTask)
-        | Message.response .. =>
-          -- TODO: handle client responses
-          mainLoop (←runClientTask)
-        | Message.responseError _ _ e .. =>
-          throwServerError s!"Unhandled response error: {e}"
-        | Message.notification method (some params) =>
-          if method == "textDocument/didOpen" then
-            -- for lean4game, we need to pass in extra information when a level is opened:
-            Game.handleDidOpenLevel (← parseParams _ (toJson params))
-          else
-            handleNotification method (toJson params)
-          mainLoop (←runClientTask)
-        | _ => throwServerError "Got invalid JSON-RPC message"
-      | ServerEvent.clientError e => throw e
-      | ServerEvent.workerEvent fw ev =>
-        match ev with
-        | WorkerEvent.ioError e =>
-          throwServerError s!"IO error while processing events for {fw.doc.uri}: {e}"
-        | WorkerEvent.crashed _ =>
-          handleCrash fw.doc.uri #[]
-          mainLoop clientTask
-        | WorkerEvent.terminated =>
-          throwServerError "Internal server error: got termination event for worker that should have been removed"
-        | .importsChanged =>
-          startFileWorker fw.doc
-          mainLoop clientTask
-
-def initAndRunWatchdogAux : GameServerM Unit := do
-  let st ← read
-  try
-    discard $ st.hIn.readLspNotificationAs "initialized" InitializedParams
-    let clientTask ← runClientTask
-    mainLoop clientTask
-  catch err =>
-    shutdown
-    throw err
-  /- NOTE(WN): It looks like instead of sending the `exit` notification,
-  VSCode just closes the stream. In that case, pretend we got an `exit`. -/
-  let Message.notification "exit" none ←
-    try st.hIn.readLspMessage
-    catch _ => pure (Message.notification "exit" none)
-    | throwServerError "Got `shutdown` request, expected an `exit` notification"
-
-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"] }
-  if out.exitCode != 0 then
-    throwServerError s!"Error while running Lake: {out.stderr}"
-
-  -- Make the paths relative to the current directory
-  let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
-  let currentDir ← IO.currentDir
-  let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
-
-  -- Set the search path
-  Lean.searchPathRef.set paths
-
-  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 < 2 then
-    throwServerError s!"Expected 1-3 command line arguments in addition to `--server`:
-      game directory, the name of the main module (optional), and the name of the game (optional)."
-  let gameDir := args[1]!
-  let module := if args.length < 3 then defaultGameModule else args[2]!
-  let gameName := if args.length < 4 then defaultGameName else args[3]!
-  let workerPath := "./gameserver"
-  -- TODO: Do the following commands slow us down?
-  let srcSearchPath ← initSrcSearchPath (← getBuildDir)
-  let references ← IO.mkRef (← loadReferences)
-  let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
-  let i ← maybeTee "wdIn.txt" false i
-  let o ← maybeTee "wdOut.txt" true o
-  let e ← maybeTee "wdErr.txt" true e
-  let state := {
-    env := ← createEnv gameDir module,
-    game := gameName,
-    gameDir := gameDir,
-    inventory := #[]
-    difficulty := 0
-    }
-  let initRequest ← i.readLspRequestAs "initialize" InitializeParams
-  -- We misuse the `rootUri` field to the gameName
-  let rootUri? := gameName
-  let initRequest := {initRequest with param := {initRequest.param with rootUri?}}
-  o.writeLspResponse {
-    id     := initRequest.id
-    result := {
-      capabilities := mkLeanServerCapabilities
-      serverInfo?  := some {
-        name     := "Lean 4 Game Server"
-        version? := "0.1.1"
-      }
-      : InitializeResult
-    }
-  }
-  let context : ServerContext := {
-    hIn            := i
-    hOut           := o
-    hLog           := e
-    args           := args
-    fileWorkersRef := fileWorkersRef
-    initParams     := initRequest.param
-    workerPath
-    srcSearchPath
-    references
-  }
-  discard $ ReaderT.run (StateT.run initAndRunWatchdogAux state) context
-
-def watchdogMain (args : List String) : IO UInt32 := do
-  let i ← IO.getStdin
-  let o ← IO.getStdout
-  let e ← IO.getStderr
-  try
-    initAndRunWatchdog args i o e
-    return 0
-  catch err =>
-    e.putStrLn s!"Watchdog error: {err}"
-    return 1
-
-end MyServer.Watchdog