update npm deps

bump npm dependencies
Update troubleshoot.md
2024-02-23 18:58:15 +01:00 · 2024-02-23 18:58:06 +01:00 · 2024-02-16 10:57:02 +01:00 · 2024-02-02 12:44:32 +01:00 · 2024-02-02 12:43:58 +01:00 · 2024-02-02 12:11:55 +01:00
51 changed files with 2796 additions and 3791 deletions
@@ -0,0 +1,7 @@
+GameSkeleton
+HiddenTactic
+subgoals
+KaTex
+gameserver
+lakefile
+Zulip
@@ -1,6 +1,6 @@
 # Lean 4 Game

-This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
+This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).

 ## Creating a Game

@@ -9,6 +9,7 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular,
 * Step 5: [How to Run Games Locally](doc/running_locally.md)
 * Step 7: [How to Update an existing Game](doc/update_game.md)
 * Step 8: [How to Publishing a Game](doc/publish_game.md)
+* [Troubleshooting](doc/troubleshoot.md)

 ## Documentation

@@ -28,7 +29,9 @@ should be up-to-date:

 ### Backend

-not written yet
+not fully written yet.
+
+* [Server](doc/DOCUMENTATION.md): describes the server part (i.e. the content of `server/` und `relay/`).

 ## Contributing

@@ -40,7 +43,8 @@ Providing the use access to a Lean instance running on the server is a severe se

 ## Credits

-The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
+The project has pimarily been developed by Alexander Bentkamp and Jon Eugster.
+
+It is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
 (NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
-by Kevin Buzzard and Mohammad Pedramfar.
-The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
+by Kevin Buzzard and Mohammad Pedramfar, and on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
@@ -8,28 +8,24 @@ import '@fontsource/roboto/700.css';

 import './css/reset.css';
 import './css/app.css';
-import { MobileContext } from './components/infoview/context';
-import { useWindowDimensions } from './window_width';
-import { connection } from './connection';
+import { PreferencesContext} from './components/infoview/context';
+import UsePreferences from "./state/hooks/use_preferences"

 export const GameIdContext = React.createContext<string>(undefined);

 function App() {
+
  const params = useParams()
  const gameId = "g/" + params.owner + "/" + params.repo
-  const {width, height} = useWindowDimensions()
-  const [mobile, setMobile] = React.useState(width < 800)

-  React.useEffect(() => {
-    connection.startLeanClient(gameId);
-  }, [gameId])
+  const {mobile, layout, isSavePreferences, setLayout, setIsSavePreferences} = UsePreferences()

  return (
    <div className="app">
      <GameIdContext.Provider value={gameId}>
-        <MobileContext.Provider value={{mobile, setMobile}}>
+          <PreferencesContext.Provider value={{mobile, layout, isSavePreferences, setLayout, setIsSavePreferences}}>
            <Outlet />
-        </MobileContext.Provider>
+          </PreferencesContext.Provider>
      </GameIdContext.Provider>
    </div>
  )
@@ -5,9 +5,9 @@ import * as React from 'react'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
  faArrowRight, faArrowLeft, faXmark, faBars, faCode,
-  faCircleInfo, faTerminal } from '@fortawesome/free-solid-svg-icons'
+  faCircleInfo, faTerminal, faMobileScreenButton, faDesktop, faGear } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from "../app"
-import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context"
+import { InputModeContext, PreferencesContext, WorldLevelIdContext } from "./infoview/context"
 import { GameInfo, useGetGameInfoQuery } from '../state/api'
 import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress } from '../state/progress'
 import { useAppDispatch, useAppSelector } from '../hooks'
@@ -150,22 +150,23 @@ function InventoryButton({pageNumber, setPageNumber}) {
 }

 /** the navigation bar on the welcome page */
-export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo} : {
+export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo, togglePreferencesPopup} : {
  pageNumber: number,
  setPageNumber: any,
  gameInfo: GameInfo,
  toggleImpressum: any,
  toggleEraseMenu: any,
  toggleUploadMenu: any,
-  toggleInfo: any
+  toggleInfo: any,
+  togglePreferencesPopup: () => void;
 }) {
  const gameId = React.useContext(GameIdContext)
  const gameProgress = useAppSelector(selectProgress(gameId))
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
  const [navOpen, setNavOpen] = React.useState(false)

  return <div className="app-bar">
-    <div>
+    <div className='app-bar-left'>
      <Button inverted="false" title="back to games selection" to="/">
        <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
      </Button>
@@ -194,6 +195,9 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres
      <Button title="Impressum, privacy policy" inverted="true" to="" onClick={() => {toggleImpressum(); setNavOpen(false)}}>
        <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Impressum
      </Button>
+      <Button title="Preferences" inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}>
+         <FontAwesomeIcon icon={faGear} />&nbsp;Preferences
+       </Button>
    </div>
  </div>
 }
@@ -208,7 +212,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=
 }) {
  const gameId = React.useContext(GameIdContext)
  const {worldId, levelId} = React.useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
  const [navOpen, setNavOpen] = React.useState(false)
  const gameInfo = useGetGameInfoQuery({game: gameId})
  const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
@@ -237,7 +241,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=
      </> :
      <>
        {/* DESKTOP VERSION */}
-        <div>
+        <div className='app-bar-left'>
          <HomeButton isDropdown={false} />
          <span className="app-bar-title">{worldTitle && `World: ${worldTitle}`}</span>
        </div>
@@ -5,6 +5,7 @@ import * as React from 'react';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { InteractiveDiagnostic, InteractiveTermGoal } from '@leanprover/infoview-api';
 import { GameHint, InteractiveGoal, InteractiveGoals } from './rpc_api';
+import { PreferencesState } from '../../state/preferences';

 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(
  null as any)
@@ -62,12 +63,18 @@ export const ProofStateContext = React.createContext<{
  setProofState: () => {},
 })

-export const MobileContext = React.createContext<{
-  mobile : boolean,
-  setMobile: React.Dispatch<React.SetStateAction<Boolean>>,
-}>({
+export interface IPreferencesContext extends PreferencesState{
+  mobile: boolean, // The variables that actually control the page 'layout' can only be changed through layout.
+  setLayout: React.Dispatch<React.SetStateAction<PreferencesState["layout"]>>;
+  setIsSavePreferences: React.Dispatch<React.SetStateAction<Boolean>>;
+}
+
+export const PreferencesContext = React.createContext<IPreferencesContext>({
  mobile: false,
-  setMobile: () => {},
+  layout: "auto",
+  isSavePreferences: false,
+  setLayout: () => {},
+  setIsSavePreferences: () => {}
 })

 export const WorldLevelIdContext = React.createContext<{
@@ -27,7 +27,7 @@ import Markdown from '../markdown';
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
 import { Goal } from './goals';
-import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context';
+import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context';
 import { Typewriter, hasErrors, hasInteractiveErrors } from './typewriter';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 import { Button } from '../button';
@@ -349,7 +349,7 @@ export function TypewriterInterface({props}) {
  const [disableInput, setDisableInput] = React.useState<boolean>(false)
  const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
  const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
  const { proof } = React.useContext(ProofContext)
  const { setTypewriterInput } = React.useContext(InputModeContext)
  const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
@@ -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) &&
+                  }
+                  <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>
                  }
-                  </>
-                  }
-                  <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/>
+
                  {/* 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
@@ -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,18 +34,19 @@ 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,
+    tab?: any,
+    setTab?: any,
    level?: LevelInfo|InventoryOverview,
    enableAll?: boolean,
  }) {
@@ -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,6 +84,7 @@ 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} />
@@ -98,12 +94,16 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
    </>
 }

-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>
 }
@@ -134,7 +134,8 @@ function LandingPage() {
    "leanprover-community/nng4",
    "hhu-adam/robo",
    "djvelleman/stg4",
-    "miguelmarco/STG4",
+    "miguelmarco/stg4",
+    "trequetrum/lean4game-logic",
  ]
  let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))

@@ -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,
@@ -28,7 +27,7 @@ import { Button } from './button'
 import Markdown from './markdown'
 import {InventoryPanel} from './inventory'
 import { hasInteractiveErrors } from './infoview/typewriter'
-import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext,
+import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
  ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
 import { GameHint } from './infoview/rpc_api'
@@ -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()
@@ -66,7 +74,7 @@ function Level() {

 function ChatPanel({lastLevel}) {
  const chatRef = useRef<HTMLDivElement>(null)
-  const {mobile} = useContext(MobileContext)
+  const {mobile} = useContext(PreferencesContext)
  const gameId = useContext(GameIdContext)
  const {worldId, levelId} = useContext(WorldLevelIdContext)
  const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
@@ -207,14 +215,12 @@ function PlayableLevel({impressum, setImpressum}) {
  const codeviewRef = useRef<HTMLDivElement>(null)
  const gameId = React.useContext(GameIdContext)
  const {worldId, levelId} = useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)

  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(PreferencesContext)

  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`}>
@@ -467,7 +468,7 @@ export default Level
 /** The site with the introduction text of a world */
 function Introduction({impressum, setImpressum}) {
  const gameId = React.useContext(GameIdContext)
-  const {mobile} = useContext(MobileContext)
+  const {mobile} = useContext(PreferencesContext)

  const inventory = useLoadInventoryOverviewQuery({game: gameId})

@@ -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() }
-  }, [])
-
-  const {leanClient, leanClientStarted} = useLeanClient(gameId)
-  const uriStr = `file:///${worldId}/${levelId}`
-  const uri = monaco.Uri.parse(uriStr)
-
-  // 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();
-      }
-    }
-  }, [editor, levelId, connection, leanClientStarted])
-
-
-  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 taskGutter = new LeanTaskGutter(infoProvider.client, editor)
-      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+    // TODO:
+    // setRestart(() => restart)

-      return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
+    return () => {
+      editor.dispose();
+      model.dispose();
+      abbrevRewriter.dispose();
+      taskgutter.dispose();
+      infoProvider.dispose();
+      client.dispose();
+    }
+  }, [gameId, worldId, levelId])
+
+  const showRestartMessage = () => {
+    // setRestartMessage(true)
+    console.log("TODO: SHOW RESTART MESSAGE")
  }
-  }, [editor, connection, leanClientStarted])

  return {editor, infoProvider, editorConnection}
 }
@@ -0,0 +1,90 @@
+import * as React from 'react'
+import { Input, Typography } from '@mui/material'
+import Markdown from '../markdown'
+import { Switch, Button, ButtonGroup } from '@mui/material';
+import Box from '@mui/material/Box';
+import Slider from '@mui/material/Slider';
+
+import FormControlLabel from '@mui/material/FormControlLabel';
+
+import { IPreferencesContext } from "../infoview/context"
+
+interface PreferencesPopupProps extends Omit<IPreferencesContext, 'mobile'> {
+    handleClose: () => void
+}
+
+export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSavePreferences, handleClose }: PreferencesPopupProps) {
+
+    const marks = [
+        {
+            value: 0,
+            label: 'Mobile',
+            key: "mobile"
+        },
+        {
+            value: 1,
+            label: 'Auto',
+            key: "auto"
+        },
+        {
+            value: 2,
+            label: 'Desktop',
+            key: "desktop"
+        },
+    ];
+
+    const handlerChangeLayout = (_: Event, value: number) => {
+        setLayout(marks[value].key as IPreferencesContext["layout"])
+    }
+
+    return <div className="modal-wrapper">
+        <div className="modal-backdrop" onClick={handleClose} />
+        <div className="modal">
+            <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+            <Typography variant="body1" component="div" className="settings">
+                <div className='preferences-category'>
+                    <div className='category-title'>
+                        <h3>Layout</h3>
+                    </div>
+                    <div className='preferences-item first leave-left-gap'>
+                        <FormControlLabel
+                            control={
+                                <Box sx={{ width: 300 }}>
+                                    <Slider
+                                        aria-label="Always visible"
+                                        value={marks.find(item => item.key === layout).value}
+                                        step={1}
+                                        marks={marks}
+                                        max={2}
+                                        sx={{
+                                            '& .MuiSlider-track': { display: 'none', },
+                                        }}
+                                        onChange={handlerChangeLayout}
+                                    />
+                                </Box>
+                            }
+                            label=""
+                        />
+                    </div>
+                </div>
+
+                <div className='preferences-category tail-category'>
+                    <div className='preferences-item'>
+                        <FormControlLabel
+                            control={
+                                <Switch
+                                    checked={isSavePreferences}
+                                    onChange={() => setIsSavePreferences(!isSavePreferences)}
+                                    name="checked"
+                                    color="primary"
+                                />
+                            }
+                            label="Save my settings (in the browser store)"
+                            labelPlacement="end"
+                        />
+                    </div>
+                </div>
+            </Typography>
+        </div>
+    </div>
+}
@@ -10,13 +10,14 @@ import { useAppDispatch, useAppSelector } from '../hooks'
 import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
 import { Button } from './button'
-import { MobileContext } from './infoview/context'
+import { PreferencesContext } from './infoview/context'
 import { InventoryPanel } from './inventory'
 import { ErasePopup } from './popup/erase'
 import { InfoPopup } from './popup/game_info'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import { RulesHelpPopup } from './popup/rules_help'
 import { UploadPopup } from './popup/upload'
+import { PreferencesPopup} from "./popup/preferences"
 import { WorldTreePanel } from './world_tree'

 import '../css/welcome.css'
@@ -26,7 +27,7 @@ import { Hint } from './hints'

 /** the panel showing the game's introduction text */
 function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) {
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
  const gameId = React.useContext(GameIdContext)
  const dispatch = useAppDispatch()

@@ -63,7 +64,9 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string,
 /** main page of the game showing among others the tree of worlds/levels */
 function Welcome() {
  const gameId = React.useContext(GameIdContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
+  const {layout, isSavePreferences, setLayout, setIsSavePreferences} = React.useContext(PreferencesContext)
+
  const gameInfo = useGetGameInfoQuery({game: gameId})
  const inventory = useLoadInventoryOverviewQuery({game: gameId})

@@ -77,15 +80,20 @@ function Welcome() {
  const [info, setInfo] = React.useState(false)
  const [rulesHelp, setRulesHelp] = React.useState(false)
  const [uploadMenu, setUploadMenu] = React.useState(false)
+  const [preferencesPopup, setPreferencesPopup] = React.useState(false)
+
  function closeEraseMenu()   {setEraseMenu(false)}
  function closeImpressum()   {setImpressum(false)}
  function closeInfo()        {setInfo(false)}
  function closeRulesHelp()   {setRulesHelp(false)}
  function closeUploadMenu()  {setUploadMenu(false)}
+  function closePreferencesPopup() {setPreferencesPopup(false)}
  function toggleEraseMenu()  {setEraseMenu(!eraseMenu)}
  function toggleImpressum()  {setImpressum(!impressum)}
  function toggleInfo()       {setInfo(!info)}
  function toggleUploadMenu() {setUploadMenu(!uploadMenu)}
+  function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
+

  // set the window title
  useEffect(() => {
@@ -101,7 +109,7 @@ function Welcome() {
  : <>
    <WelcomeAppBar pageNumber={pageNumber} setPageNumber={setPageNumber} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum}
      toggleEraseMenu={toggleEraseMenu} toggleUploadMenu={toggleUploadMenu}
-      toggleInfo={toggleInfo} />
+      toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
    <div className="app-content">
      { mobile ?
          <div className="welcome mobile">
@@ -128,6 +136,7 @@ function Welcome() {
    {eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
    {uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
    {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
+    {preferencesPopup ? <PreferencesPopup layout={layout} isSavePreferences={isSavePreferences} setLayout={setLayout} setIsSavePreferences={setIsSavePreferences} handleClose={closePreferencesPopup}/> : null}
  </>
 }

@@ -16,6 +16,7 @@ import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/p
 import { store } from '../state/store'

 import '../css/world_tree.css'
+import { PreferencesContext } from './infoview/context'

 // Settings for the world tree
 cytoscape.use( klay )
@@ -197,13 +198,15 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
  const gameId = React.useContext(GameIdContext)
  const difficulty = useSelector(selectDifficulty(gameId))
  const dispatch = useAppDispatch()
+  const { mobile } = React.useContext(PreferencesContext)
+

  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 +216,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)},
@@ -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}
-}
@@ -105,11 +105,18 @@ em {
  position: relative;
  flex-direction: row;
  justify-content: space-between;
+  align-items: center;
  padding: 1.1em;
  filter: drop-shadow(0 0 5px rgba(0,0,0,0.5));
  z-index: 2;
 }

+.app-bar > .app-bar-left{
+  display: flex;
+  align-items: center;
+  gap: .5em;
+}
+
 .app-bar-title, .app-bar-subtitle {
  color: white;
  font-weight: 500;
@@ -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;
+}
@@ -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;
@@ -317,11 +331,6 @@ td code  {
  margin-right: 0;
 }

-#home-btn {
-  margin-right: .5em;
-  margin-left: 0;
-}
-
 .menu.dropdown .svg-inline--fa {
  width: 1.8rem;
 }
@@ -187,3 +187,15 @@ h5, h6 {
  margin-left: 0.3rem;
  margin-right: 0.3rem;
 }
+
+.preferences-category.tail-category{
+  margin-top: 2em;
+}
+
+.preferences-item.first{
+  margin-top: 1em;
+}
+
+.preferences-item.leave-left-gap{
+  margin-left: 3em;
+}
@@ -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;
@@ -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>
    </Provider>
  </React.StrictMode>
 );
@@ -35,6 +35,7 @@ export interface InventoryTile {
  locked: boolean,
  new: boolean,
  hidden: boolean
+  altTitle: string,
 }

 export interface LevelInfo {
@@ -0,0 +1,41 @@
+import React, { useState } from "react";
+import { useAppDispatch, useAppSelector } from "../../hooks";
+import { 
+    PreferencesState, 
+    setLayout as setPreferencesLayout, 
+    setIsSavePreferences as setPreferencesIsSavePreferences,
+    getWindowDimensions,
+    AUTO_SWITCH_THRESHOLD
+} from "../preferences";
+
+
+const UsePreferences = () => {
+    const dispatch = useAppDispatch()
+    const [mobile, setMobile] = React.useState<boolean>()
+
+    const layout = useAppSelector((state) => state.preferences.layout);
+    const setLayout = (layout: PreferencesState["layout"]) => dispatch(setPreferencesLayout(layout))
+
+    const isSavePreferences = useAppSelector((state) => state.preferences.isSavePreferences);
+    const setIsSavePreferences = (isSave: boolean) => dispatch(setPreferencesIsSavePreferences(isSave))
+
+    const automaticallyAdjustLayout = () => {
+        const {width} = getWindowDimensions()
+        setMobile(width < AUTO_SWITCH_THRESHOLD)
+    }
+
+    React.useEffect(()=>{
+        if (layout === "auto"){
+          void automaticallyAdjustLayout()
+          window.addEventListener('resize', automaticallyAdjustLayout)
+    
+          return () => window.removeEventListener('resize', automaticallyAdjustLayout)
+        } else {
+          setMobile(layout === "mobile")
+        }
+    }, [layout])
+
+    return {mobile, layout, isSavePreferences, setLayout, setIsSavePreferences}
+} 
+
+export default UsePreferences;
@@ -36,3 +36,33 @@ export async function saveState(state: any) {
    // Ignore
  }
 }
+
+const PREFERENCES_KEY = "preferences"
+
+/** Load from browser storage */
+export function loadPreferences() {
+  try {
+    const serializedState = localStorage.getItem(PREFERENCES_KEY);
+    return JSON.parse(serializedState)
+  } catch (e) {
+    return undefined;
+  }
+}
+
+export function savePreferences(state: any) {
+  try {
+    const serializedState = JSON.stringify(state)
+    localStorage.setItem(PREFERENCES_KEY, serializedState);
+  } catch (e) {
+    // Ignore
+  }
+}
+
+export function removePreferences() {
+  try {
+    localStorage.removeItem(PREFERENCES_KEY);
+  } catch (e) {
+    // Ignore
+  }
+}
+
@@ -0,0 +1,35 @@
+import { createSlice } from "@reduxjs/toolkit";
+
+import { loadPreferences, removePreferences, savePreferences } from "./local_storage";
+
+export interface PreferencesState {
+  layout: "mobile" | "auto" | "desktop";
+  isSavePreferences: boolean;
+}
+
+export function getWindowDimensions() {
+  const {innerWidth: width, innerHeight: height } = window
+  return {width, height}
+}
+
+export const AUTO_SWITCH_THRESHOLD = 800
+
+const initialState: PreferencesState = loadPreferences() ??{
+    layout: "auto",
+    isSavePreferences: false
+}
+
+export const preferencesSlice = createSlice({
+  name: "preferences",
+  initialState,
+  reducers: {
+    setLayout: (state, action) => {
+      state.layout = action.payload;
+    },
+    setIsSavePreferences: (state, action) => {
+      state.isSavePreferences = action.payload;
+    },
+  },
+});
+
+export const { setLayout, setIsSavePreferences } = preferencesSlice.actions;
@@ -53,22 +53,22 @@ const initalLevelProgressState: LevelProgressState = {code: "", completed: false

 /** Add an empty skeleton with progress for the current game */
 function addGameProgress (state: ProgressState, action: PayloadAction<{game: string}>) {
-  if (!state.games[action.payload.game]) {
-    state.games[action.payload.game] = {inventory: [], openedIntro: true, data: {}, difficulty: DEFAULT_DIFFICULTY}
+  if (!state.games[action.payload.game.toLowerCase()]) {
+    state.games[action.payload.game.toLowerCase()] = {inventory: [], openedIntro: true, data: {}, difficulty: DEFAULT_DIFFICULTY}
  }
-  if (!state.games[action.payload.game].data) {
-    state.games[action.payload.game].data = {}
+  if (!state.games[action.payload.game.toLowerCase()].data) {
+    state.games[action.payload.game.toLowerCase()].data = {}
  }
 }

 /** Add an empty skeleton with progress for the current level */
 function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
  addGameProgress(state, action)
-  if (!state.games[action.payload.game].data[action.payload.world]) {
-    state.games[action.payload.game].data[action.payload.world] = {}
+  if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world]) {
+    state.games[action.payload.game.toLowerCase()].data[action.payload.world] = {}
  }
-  if (!state.games[action.payload.game].data[action.payload.world][action.payload.level]) {
-    state.games[action.payload.game].data[action.payload.world][action.payload.level] = {...initalLevelProgressState}
+  if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level]) {
+    state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = {...initalLevelProgressState}
  }
 }

@@ -79,58 +79,58 @@ export const progressSlice = createSlice({
    /** put edited code in the state and set completed to false */
    codeEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, code: string}>) {
      addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].code = action.payload.code
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].completed = false
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].code = action.payload.code
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = false
    },
    /** TODO: docstring */
    changedSelection(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, selections: Selection[]}>) {
      addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].selections = action.payload.selections
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].selections = action.payload.selections
    },
    /** mark level as completed */
    levelCompleted(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
      addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].completed = true
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = true
    },
    /** Set the list of rows where help is displayed */
    helpEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, help: number[]}>) {
      addLevelProgress(state, action)
      console.debug(`!setting help to: ${action.payload.help}`)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].help = action.payload.help
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].help = action.payload.help
    },
    /** delete all progress for this game */
    deleteProgress(state: ProgressState, action: PayloadAction<{game: string}>) {
-      state.games[action.payload.game] = {inventory: [], data: {}, openedIntro: true, difficulty: DEFAULT_DIFFICULTY}
+      state.games[action.payload.game.toLowerCase()] = {inventory: [], data: {}, openedIntro: true, difficulty: DEFAULT_DIFFICULTY}
    },
    /** delete progress for this level */
    deleteLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
      addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level] = initalLevelProgressState
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = initalLevelProgressState
    },
    /** load progress, e.g. from external import */
    loadProgress(state: ProgressState, action: PayloadAction<{game: string, data:GameProgressState}>) {
      console.debug(`setting data to:\n ${action.payload.data}`)
-      state.games[action.payload.game] = action.payload.data
+      state.games[action.payload.game.toLowerCase()] = action.payload.data
    },
    /** set the current inventory */
    changedInventory(state: ProgressState, action: PayloadAction<{game: string, inventory: string[]}>) {
      addGameProgress(state, action)
-      state.games[action.payload.game].inventory = action.payload.inventory
+      state.games[action.payload.game.toLowerCase()].inventory = action.payload.inventory
    },
    /** set the difficulty */
    changedDifficulty(state: ProgressState, action: PayloadAction<{game: string, difficulty: number}>) {
      addGameProgress(state, action)
-      state.games[action.payload.game].difficulty = action.payload.difficulty
+      state.games[action.payload.game.toLowerCase()].difficulty = action.payload.difficulty
    },
    /** set the difficulty */
    changedOpenedIntro(state: ProgressState, action: PayloadAction<{game: string, openedIntro: boolean}>) {
      addGameProgress(state, action)
-      state.games[action.payload.game].openedIntro = action.payload.openedIntro
+      state.games[action.payload.game.toLowerCase()].openedIntro = action.payload.openedIntro
    },
    /** set the typewriter mode */
    changeTypewriterMode(state: ProgressState, action: PayloadAction<{game: string, typewriterMode: boolean}>) {
      addGameProgress(state, action)
-      state.games[action.payload.game].typewriterMode = action.payload.typewriterMode
+      state.games[action.payload.game.toLowerCase()].typewriterMode = action.payload.typewriterMode
    }
  }
 })
@@ -138,74 +138,74 @@ export const progressSlice = createSlice({
 /** if the level does not exist, return default values */
 export function selectLevel(game: string, world: string, level: number) {
  return (state) =>{
-    if (!state.progress.games[game]) { return initalLevelProgressState }
-    if (!state.progress.games[game].data[world]) { return initalLevelProgressState }
-    if (!state.progress.games[game].data[world][level]) { return initalLevelProgressState }
-    return state.progress.games[game].data[world][level]
+    if (!state.progress.games[game.toLowerCase()]) { return initalLevelProgressState }
+    if (!state.progress.games[game.toLowerCase()].data[world]) { return initalLevelProgressState }
+    if (!state.progress.games[game.toLowerCase()].data[world][level]) { return initalLevelProgressState }
+    return state.progress.games[game.toLowerCase()].data[world][level]
  }
 }

 /** return the code of the current level */
 export function selectCode(game: string, world: string, level: number) {
  return (state) => {
-    return selectLevel(game, world, level)(state).code
+    return selectLevel(game.toLowerCase(), world, level)(state).code
  }
 }

 /** return the current inventory */
 export function selectInventory(game: string) {
  return (state) => {
-    if (!state.progress.games[game]) { return [] }
-    return state.progress.games[game].inventory
+    if (!state.progress.games[game.toLowerCase()]) { return [] }
+    return state.progress.games[game.toLowerCase()].inventory
  }
 }

 /** return the code of the current level */
 export function selectHelp(game: string, world: string, level: number) {
  return (state) => {
-    return selectLevel(game, world, level)(state).help
+    return selectLevel(game.toLowerCase(), world, level)(state).help
  }
 }

 /** return the selections made in the current level */
 export function selectSelections(game: string, world: string, level: number) {
  return (state) => {
-    return selectLevel(game, world, level)(state).selections
+    return selectLevel(game.toLowerCase(), world, level)(state).selections
  }
 }

 /** return whether the current level is clompleted */
 export function selectCompleted(game: string, world: string, level: number) {
  return (state) => {
-    return selectLevel(game, world, level)(state).completed
+    return selectLevel(game.toLowerCase(), world, level)(state).completed
  }
 }

 /** return progress for the current game if it exists */
 export function selectProgress(game: string) {
  return (state) => {
-    return state.progress.games[game] ?? null
+    return state.progress.games[game.toLowerCase()] ?? null
  }
 }

 /** return difficulty for the current game if it exists */
 export function selectDifficulty(game: string) {
  return (state) => {
-    return state.progress.games[game]?.difficulty ?? DEFAULT_DIFFICULTY
+    return state.progress.games[game.toLowerCase()]?.difficulty ?? DEFAULT_DIFFICULTY
  }
 }

 /** return whether the intro has been read */
 export function selectOpenedIntro(game: string) {
  return (state) => {
-    return state.progress.games[game]?.openedIntro
+    return state.progress.games[game.toLowerCase()]?.openedIntro
  }
 }

 /** return typewriter mode for the current game if it exists */
 export function selectTypewriterMode(game: string) {
  return (state) => {
-    return state.progress.games[game]?.typewriterMode ?? true
+    return state.progress.games[game.toLowerCase()]?.typewriterMode ?? true
  }
 }

@@ -7,21 +7,19 @@ import { debounce } from "debounce";
 import { connection } from '../connection'
 import { apiSlice } from './api'
 import { progressSlice } from './progress'
-import { saveState } from "./local_storage";
+import { preferencesSlice } from "./preferences"
+import { saveState, savePreferences, removePreferences} from "./local_storage";


 export const store = configureStore({
  reducer: {
    [apiSlice.reducerPath]: apiSlice.reducer,
    [progressSlice.name]: progressSlice.reducer,
+    [preferencesSlice.name]: preferencesSlice.reducer,
  },
  // Make connection available in thunks:
  middleware: getDefaultMiddleware =>
-    getDefaultMiddleware({
-      thunk: {
-        extraArgument: { connection }
-      }
-    }).concat(apiSlice.middleware),
+    getDefaultMiddleware().concat(apiSlice.middleware),
 });

 /**
@@ -31,6 +29,9 @@ export const store = configureStore({
 store.subscribe(
  debounce(() => {
    saveState(store.getState()[progressSlice.name]);
+
+    const preferencesState = store.getState()[preferencesSlice.name]
+    preferencesState.isSavePreferences ? savePreferences(preferencesState) : removePreferences()
  }, 800)
 );

@@ -1,21 +0,0 @@
-import {useState, useEffect} from 'react'
-
-function getWindowDimensions() {
-  const {innerWidth: width, innerHeight: height } = window
-  return {width, height}
-}
-
-export function useWindowDimensions() {
-  const [windowDimensions, setWindowDimensions] = useState(getWindowDimensions())
-
-  useEffect(() => {
-    function handleResize() {
-      setWindowDimensions(getWindowDimensions())
-    }
-    window.addEventListener('resize', handleResize)
-    return () => window.removeEventListener('resize', handleResize)
-
-  }, [])
-
-  return windowDimensions
-}
@@ -1,335 +1,67 @@
-**NOTE! This document is deprecated! The current documentation is [How To Create A Game](create_game.md)**
+# Server

-# Creating a game.
+The server is made out of two parts, named "relay" and "server".

-Ideally one takes the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new game.
+The former, "relay", is the server which
+sets up a socket connection to the client, starts the lean servers to work on files and
+relays messages between the lean server and the client. `index.mjs` is the file that needs to
+be run, which is done for example using `pm2` or by calling `npm run start_server` or
+`npm run production`, see more later.

-## Game Structure
+The latter, "server", is the lean server which has two jobs. For one, it produces the "gameserver"
+executable which is the lean server that handles the files the player plays on. The second job
+is to provide the lean commands which are used when creating a game. These are located in
+`Commands.lean`.

-A game consist of worlds which have multiple levels each. In the following we describe how to create a level file and how to combine these into a game.

-### Level
+## Integration into Games

-A level file is a lean file that imports at least `import GameServer.Commands` and starts with the following Lean commands.
+Games need the "server" as a lake-dependency, which is done in the game's lakefile.
+
+A game imports `GameServer.Commands` which provides to all the API required to
+create a game.
+
+In particular the lean command `MakeGame` compiles the entire game. Static information is
+stored as JSON files in `.lake/gamedata` for faster loading, while other data is only
+saved to lean env-extensions which the lean server has access to after loading the lean file.
+
+For games to be run successfully, it is important that the "gameserver" executable inside
+the game's `.lake` folder is actually built.
+Currently, this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`.
+(both commands are to be executed in the game's directory!)
+
+## Modifying the server
+
+### Starting the server
+
+When using the [manual installation](running_locally.md#manual-installation) you can run the server
+using

-```lean
-Game "NNG"
-World "Addition"
-Level 1
-Title "The rfl tactic"
 ```
-
-Note that the levels inside a world must have consecutive numbering starting with `1`. The `Game`
-and `World` strings can be anything, see below.
-
-#### Statement
-
-The core of a level is the `Statement`, which is the exercise that should be proven.
-
-```lean
-/-- For all natural numbers $n$, we have $0 + n = n$. -/
-@[simp]
-Statement MyNat.zero_add
-    (n : ℕ) : 0 + n = n := by
-  Hint "You can start a proof by `induction n`."
-  induction n with n hn
-  · Hint "This is the base case."
-    rw [add_zero]
-    rfl
-  · Hint "This is the induction hypothesis"
-    rw [add_succ]
-    Branch
-      simp
-      Hint "A branch is an alternative tactic sequence. Does not need to finish the proof."
-    rw [hn]
-    rfl
-```
-
-##### Proof
-
-The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax.
-
-There are a few extra tactics that help you structuring the proof:
-
- `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
-  the one where `Hint` is placed. For more options about hints, see below.
- `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which
-  helps setting `Hints` in different   places. The `Branch` does not affect the main
-  proof and does not need to finish any goals.
- `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template`
-  will be copied into the editor with all `Hole`s replaced with `sorry`. Note that
-  having a `Template` will force the user to use Editor-mode for this level.
-
-##### Statement Name (optional)
-
-If you specify a name (`MyNat.zero_add`), this lemma will be available in future levels.
-(Note that a future level must also import this level,
-so that Lean knows about the added statement).
-
-The name must be *fully qualified*. (TODO: is that still true? Did we implement namespaces?)
-
-##### Doc Comment (optional)
-
-There are three places where the documentation comment appears:
-
-1. as doc comment when hovering over the theorem
-2. as exercise description at the top of the level: ``Theorem `zero_add`: yada yada.``
-3. in the inventory. This can be overwritten by using
-  `LemmaDoc MyNat.zero_add "different yada yada"` as one might want to add a more detailed
-  description there including examples etc.
-
-Both latter points support Markdown (including katex).
-
-##### Attributes (optional)
-
-the `@[ attributes ]` prefix should work just like you know it from the `theorem` keyword.
-
-#### Introduction/Conclusion
-
-Optionally, you can add an `Introduction "some text"` and `Conclusion "some text"` to your level.
-The introduction will be shown at the beginning, the conclusion is displayed once the level
-is solved.
-
-#### Theorems/Tactics/Definitions
-
-Only enabled theorems/tactics/definitions (called "items" here) are available in a level.
-
-To add a new item in a level, you can add
-
-```lean
-NewTactic rfl simp
-NewLemma MyNat.add_zero MyNat.add_succ
-NewDefinition Nat Pow Mul
-```
-
-Once added, items will be available in all future levels/worlds,
-unless you disable them for a particular level with
-
-```lean
-DisabledTactic tauto
-DisabledLemma MyNat.add_zero
-```
-
-or specify explicitly which items should be available with
-
-```lean
-OnlyTactic rw rfl apply
-OnlyLemma MyNat.add_zero
-```
-
-Lastly, all items need documentation entries (which are imported in the level),
-see more about that below. There is also explains the `LemmaTab` keyword.
-
-### World
-
-Multiple levels are combined into a world and the worlds are then added to the game. It is recommended that all levels of a world are inside one folder (e.g. `NNG/Levels/Addition/`) and
-then there is one world file (`NNG/Levels/Addition.lean`) which contains the following
-
-```lean
-import NNG.Levels.Addition.Level_1
-import NNG.Levels.Addition.Level_2
-
-Game "NNG"
-World "Addition"
-Title "Addition World"
-
-Introduction "some text"
-```
-
-The `Title` is the world's display title. The `Introduction` is displayed before loading level 1.
-Note that all levels of a world should be imported by the world file.
-
-BUG: A level **must not** be imported in a different world's level. Instead, you have to import an entire world there: `import NNG.Levels.Addition`
-
-### Game
-
-The Game itself (i.e. the main file of you lake project, `NNG.lean`) should import all worlds and have the following layout, concluding with `MakeGame`:
-
-```lean
-import NNG.Levels.Addition
-import NNG.Levels.Multiplication
-import NNG.Levels.Power
-
-Game "NNG"
-Title "Natural Number Game"
-Introduction "some text"
-
-MakeGame
-```
-
-The game will automatically compute the order of the worlds depending on the sample proofs of the Levels (ignoring anything inside a `Branch`). You can add additional dependencies manually by adding `Dependency PowerWorld → ImpossibleWorld` before `MakeGame`.
-The order of worlds influences which tactics and lemmas will be unlocked in a given level.
-
-`MakeGame` will display warnings about things in the game that need to be fixed, like missing
-documentation or if a tactic is never introduced.
-
-### Documentation
-
-Each tactic, theorem, or definition (all called items here) that is introduced in the game
-needs a documentation entry. These are statements of the following form:
-
-```lean
-LemmaDoc MyNat.add_squared as "add_squared" in "Pow"
-"(missing)"
-
-TacticDoc constructor
-"(missing)"
-
-DefinitionDoc One as "1"
-"(missing)"
-```
-
-Notes:
-
-* The lemma name must be **fully qualified**. The string display name can be arbitrary.
-* Tactics must have their proper name. use `TacticDoc «have» ""` if it does not work
-  without french quotes.
-* Definition names can be arbitrary. E.g. I used `DefinitionDoc Symbol.Fun as "fun x ↦ x" "(missing)"` once.
-
-Moreover, the lemmas are in sorted in tabs (the `in "Pow`) part. In each level file, you
-can define which tab is open when the level is loaded by adding `LemmaTab "Pow"`.
-
-There will be features added to get automatic information from mathlib!
-
-## Escaping
-(TODO: Move)
-
-
-Inside the doc comment you don't need to escape the backslashes:
-
-```lean
-/-- $\operatorname{succ}(n)$. notation for naturals is `\N`. -/
-Statement ...
-```
-
-However, inside interpolated strings (e.g. in `Hint`, `Introduction` and `Conclusion`)
-you do need to escape backslashes
-with `\\` and `{` with `\{`:
-
-```lean
-Hint "This code has some $\\operatorname\{succ}(n)$ math. The value of `h` is {h}.
-Notation for naturals is `\\N`."
-```
-
-## Game design
-Here are some things you should consider designing a new game:
-
-* A world with more than 16 levels will be displayed with the levels spiraling outwards,
-  it might be desirable to stay below that bound. Above 22 levels the spiral start getting out
-  of control.
-
-# Running Games Locally
-
-The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
-
-## VSCode Dev Containers
-
-1.  **Install Docker and Dev Containers** *(once)*:<br/>
-    See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
-    Explicitly this means:
-    * Install docker engine if you have not yet: [Instructions](https://docs.docker.com/engine/install/).
-      I followed the "Server" instructions for linux.
-    * Note that on Linux you need to add your user to the `docker` group
-      ([see instructions](https://docs.docker.com/engine/install/linux-postinstall/)) and probably reboot.
-    * Open the games folder in VSCode: `cd NNG4 && code .` or "Open Folder" within VSCode
-    * a message appears prompting you to install the "Dev Containers" extension (by Microsoft).
-
-2.  **Open Project in Dev Container** *(everytime)*:<br/>
-    Once you have the Dev Containers Extension installed, (re)open the project folder of your game in VSCode.
-    A message appears asking you to "Reopen in Container".
-
-    * The first start will take a while, ca. 2-10 minutes. After the first
-      start this should be very quickly.
-    * Once built, it should open a tab "Simple Browser" inside VSCode displaying
-      the game. (Alternatively, open http://localhost:3000 in your browser).
-
-3.  **Editing Files** *(everytime)*:<br/>
-    After editing some files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`.
-    Now you can reload your browser to see the changes.
-
-### Errors
-
-* If you don't get the pop-up, you might have disabled them and you can reenable it by
-  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
-* If the starting the container fails, in particular with a message `Error: network xyz not found`,
-  you might have deleted stuff from docker via your shell. Try deleting the container and image
-  explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
-  container. (this will again take some time)
-
-
-## Without Dev Containers
-Install `nvm`:
-```bash
-curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
-```
-then reopen bash and test with `command -v nvm` if it is available (Should print "nvm").
-
-Now install node:
-```bash
-nvm install node
-```
-
-Clone the game (e.g. `NNG4` here):
-```bash
-git clone https://github.com/hhu-adam/NNG4.git
-# or: git clone git@github.com:hhu-adam/NNG4.git
-```
-
-Download dependencies and build the game:
-```bash
-cd NNG4
-lake update
-lake exe cache get   # if your game depends on mathlib
-lake build
-```
-
-Clone the game repository into a directory next to the game:
-```bash
-cd ..
-git clone https://github.com/leanprover-community/lean4game.git
-# or: git clone git@github.com:leanprover-community/lean4game.git
-```
-The folders `NNG4` and `lean4game` must be in the same directory!
-
-In `lean4game`, install dependencies:
-```bash
-cd lean4game
-npm install
-```
-
-TODO: This is outdated!
-If you are developing a game other than `Robo` or `NNG4`, adapt the
-code at the beginning of `lean4game/relay/index.mjs`:
-```typescript
-const games = {
-    "g/hhu-adam/robo": {
-        dir: "../../../../Robo",
-        queueLength: 5
-    },
-    "g/hhu-adam/nng4": {
-        dir: "../../../../NNG4",
-        queueLength: 5
-    }
-}
-```
-
-Run the game:
-```bash
 npm start
 ```

-This takes a little time. Eventually, the server is available on http://localhost:3000/
-and the game is available on http://localhost:3000/#/g/hhu-adam/NNG4.
+This way any changes to files in `client/` or `relay/` will cause the server to restart automatically.

-### Modifying the GameServer
+Alternative, you can run `npm run build` followed by the commands

-When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with this
-setup by setting `export NODE_ENV=development` inside your local game before building it:
-
-```bash
-cd NNG4
-export NODE_ENV=development
-lake update
-lake build
 ```
-This causes lake to search locally for the `GameServer` lake package instead of using the version from github.
+npm run start_client
+npm run production
+```
+
+(in two separate terminals) to test the production mode of the server. This way it will only
+change once you build and restart the server.
+
+### Modifying the lean server
+
+To test a modified lean server (i.e. content of `server/`), you can use the local dev setup and call
+`lake update -R -Klean4game.local` in your game followed by `lake build`.
+This will cause lake to look for the
+local lean server as a dependency instead of the version it downloaded from git.
+
+You can play a local game at https://localhost:3000/#/g/local/{FolderName} where you replace `{FolderName}` with the game folder name.
+
+After modifications in `server/`, you will need to call `lake build gameserver` (called in `server/` or in your game's folder) to rebuild
+the gameserver executable and
+`lake build` (called in the game's folder) to rebuild the game.
@@ -0,0 +1,9 @@
+# Changelog
+
+## v4.5.0
+
+### Breaking changes
+
+* Fix (#183): local store accepts case insensitive URL. The game progress has previously been saved under case sensitive URLs. You might need to recover old progress from your browser storage.
+
+## Other
@@ -98,7 +98,7 @@ This introduction text is shown when one first enters a world.
 1. Use the template above and make sure you import all levels of this world.
 1. In `Game.lean` import the world with `import Game.Levels.MyWorld`

-Now you created a world with one level and added it🎉 The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently it shows
+Now you created a world with one level and added it🎉 The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently, it shows

 ```text
 No world introducing sorry, but required by MyWorld
@@ -125,23 +125,32 @@ The player has an inventory with tactics, theorems, and definitions that unlock

 ```lean
 NewTactic induction simp
-NewLemma Nat.zero_mul
+NewTheorem Nat.zero_mul
 NewDefinition Pow
 ```

+**Important:** All commands in this section 6a) expect the `Name` they take as input
+to be **fully qualified**. For example `NewTheorem Nat.zero_mul` and not `NewTheorem zero_mul`.
+
 #### Doc entries

-You'll see a warning about a missing Lemma documentation. You can fix it by adding doc-entries like the following somewhere above it.
+You'll see a warning about a missing Theorem documentation. You can fix it by adding doc-entries like the following somewhere above it.

 ```lean
-LemmaDoc Nat.zero_mul as "zero_mul" in "Mul"
-"some description"
+/--
+some description
+-/
+TheoremDoc Nat.zero_mul as "zero_mul" in "Mul"

+/--
+some description
+-/
 TacticDoc simp
-"some description"

+/--
+some description
+-/
 DefinitionDoc Pow as "^"
-"some description"
 ```

 (e.g. you could also create a file `Game/Doc/MyTheorems.lean`, add there your documentation and import it)
@@ -153,7 +162,7 @@ If you do not provide any content for the inventory, the game will try to find a
 You have a few options to disable inventory items that have been unlocked in previous levels:

 ```lean
-DisableTactic, DisableLemma, OnlyTactic, OnlyLemma
+DisabledTactic, DisabledTheorem, OnlyTactic, OnlyTheorem
 ```

 have the same syntax as above. The former two disable items for this level, the latter two
@@ -161,7 +170,7 @@ disable all items except the ones specified.

 #### Theorem Tab

-Theorems are sorted into tabs. with `LemmaTab "Mul"` you specify which tab should be open by default in this level.
+Theorems are sorted into tabs. With `TheoremTab "Mul"` you specify which tab should be open by default in this level.

 #### HiddenTactic

@@ -176,12 +185,14 @@ and only `rw` would show up in the inventory.

 ### 6. b) Statement

-The statement is the exercise of the level. the basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax
+The statement is the exercise of the level. The basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax

 #### Name

 You can give your exercise a name: `Statement my_first_exercise (n : Nat) ...`. If you do so, it will be added to the inventory and be available in future levels.

+You can but a `Statement` inside namespaces like you would with `theorem`.
+
 #### Doc String / Exercise statement

 Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports Latex.
@@ -205,12 +216,12 @@ Statement my_simp_lemma ...

 The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax.

-There are a few extra tactics that help you structuring the proof:
+There are a few extra tactics that help you with structuring the proof:

 - `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
  the one where `Hint` is placed. For more options about hints, see below.
 - `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which
-  helps setting `Hints` in different places. The `Branch` does not affect the main
+  helps to set `Hints` in different places. The `Branch` does not affect the main
  proof and does not need to finish any goals.
 - `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template`
  will be copied into the editor with all `Hole`s replaced with `sorry`. Note that
@@ -225,7 +236,7 @@ Most important for game development are probably the `Hints`.
 The hints will be displayed whenever the player's current goal matches the goal the hint is
 placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands.

-Read [More about Hints](doc/hints.md) for how they work and what the options are.
+Read [More about Hints](hints.md) for how they work and what the options are.

 ### 6. e) Extra: Images
 You can add images on any layer of the game (i.e. game/world/level). These will be displayed in your game.
@@ -237,11 +248,11 @@ NOTE: At present, only the images for a world are displayed. They appear in the

 ## 7. Update your game

-In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](doc/update_game.md).
+In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](update_game.md).

 ## 8. Publish your game

-To publish your game on the official server, see [Publishing a game](doc/publish_game.md)
+To publish your game on the official server, see [Publishing a game](publish_game.md)

 There are a few more options you can add in `Game.lean` before the `MakeGame` command, which describe the tile that is visible on the server's landing page:

@@ -10,6 +10,8 @@ Statement .... := by
  ...
 ```

+Note that hints are only **context-aware but not history-aware**. In particular, they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps to place hints outside the sample solution's proof.
+
 ## 1. When do hints show?

 A hint will be displayed if the player's goal matches the one where the hint was placed in the
@@ -17,7 +19,7 @@ sample solutions and the entire context from the sample solutions is present in
 player's context. The player's context may contain additional items.

 This means if you have multiple identical
-subgoals, you should only place a single hint in one of them and it will be displayed in
+subgoals, you should only place a single hint in one of them, and it will be displayed in
 all of them.

 However, identical (non-hidden) hints which where already present in the step
@@ -30,12 +32,12 @@ Hidden hints are not filtered.
 You can use `Branch` to place hints
 in dead ends or alternative proof strands.

-A proof inside a `Branch`-block is normally evaluated by lean but it's discarded at the end
+A proof inside a `Branch`-block is normally evaluated by lean, but it's discarded at the end
 so that no progress has been made on proofing the goal.

 ```
 Statement .... := by
-  Hint "Huse `rw` or `rewrite`."
+  Hint "use `rw` or `rewrite`."
  Branch
    rewrite [h]
    Hint "now you still need `rfl`"
@@ -1,6 +1,6 @@
 # Publishing games

-You can publish your game on the official (Lean Game Server)[https://adam.math.hhu.de] in a few simple
+You can publish your game on the official [Lean Game Server](https://adam.math.hhu.de) in a few simple
 steps.

 ## 1. Upload Game to github
@@ -11,7 +11,7 @@ tab.

 ## 2. Import the game

-You call the URL that's listed under "What's Next?" in the latest action run. Explicitely you call
+You call the URL that's listed under "What's Next?" in the latest action run. Explicitly you call
 the URL of the form

 > adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY}
@@ -2,6 +2,8 @@

 The installation instructions are not yet tested on Mac/Windows. Comments very welcome!

+Please also consult the [Troubleshooting Collection](troubleshoot.md), where some known pitfalls are collected.
+
 There are several options to play a game locally:

 1. VSCode Dev Container: needs `docker` installed on your machine
@@ -31,24 +33,14 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta

    * The first start will take a while, ca. 2-15 minutes. After the first
      start this should be very quickly.
-    * Once built, you can open http://localhost:3000 in your browser. which should load the game.
+    * Once built, you can open http://localhost:3000 in your browser, which should load the game.

 3.  **Editing Files** *(everytime)*:<br/>
    After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes.

-### Errors
-
-* If you don't get the pop-up, you might have disabled them and you can reenable it by
-  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
-* If the starting the container fails, in particular with a message `Error: network xyz not found`,
-  you might have deleted stuff from docker via your shell. Try deleting the container and image
-  explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
-  container. (this will again take some time)
-* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.
-
 ## Codespaces

-You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
+You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".

 Note: You have to wait until npm started properly, which might take a good while.

@@ -108,6 +100,29 @@ Run the game:
 npm start
 ```

+You should see a message like this:
+```bash
+[server] > lean4-game@0.1.0 start_server
+[server] > (cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec "node ./index.mjs")
+[server]
+[client]
+[client] > lean4-game@0.1.0 start_client
+[client] > cross-env NODE_ENV=development vite --host
+[client]
+[server] [nodemon] 3.0.#
+[server] [nodemon] to restart at any time, enter `rs`
+[server] [nodemon] watching path(s): *.*
+[server] [nodemon] watching extensions: mjs
+[server] [nodemon] starting `node ./index.mjs`
+[client]
+[client]   VITE v4.5.1  ready in \#\#\# ms
+[client]
+[client]   ➜  Local:   http://localhost:3000/
+[client]   ➜  Network: http://###.###.###.##:3000/
+[client] [vite-plugin-static-copy] Collected 7 items.
+[server] (node:#####) [DEP0040] [server] Listening on 8080
+```
+
 This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/GameSkeleton. Replace `GameSkeleton` with the folder name of your local game.

 ## Modifying the GameServer
@@ -6,7 +6,7 @@ In order to set up the server to allow imports, one needs to create a
 repos will suffice.

 You need to set the environment variables `LEAN4GAME_GITHUB_USER` and `LEAN4GAME_GITHUB_TOKEN`
-with your user name and access token. For example, you can seet these in `ecosystem.config.cjs` if
+with your user name and access token. For example, you can set these in `ecosystem.config.cjs` if
 you're using `pm2`

 Then people can call:
@@ -22,7 +22,7 @@ where you replace:

 > https://{website}/#/g/{owner}/{repo}

-## data management
+## Data management
 Everything downloaded remains in the folder `lean4game/games`.
-the subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
+The subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
 The other folders should only contain the built lean-games, sorted by owner and repo.
@@ -0,0 +1,37 @@
+# Troubleshooting
+
+Here are some issues experienced by users.
+
+- You can reset the lake projects involved (i.e. the `server/` folder here as well as your [game's folder](https://github.com/hhu-adam/GameSkeleton)) with the following commands:
+  ```
+  cd [THE PROJECT]
+  rm -rf .lake/
+  lake update -R
+  lake build
+  ```
+  If you experience problems related to Lean or lake, you should first try to reset it this way.
+
+# VSCode Dev-Container
+* If you don't get the pop-up, you might have disabled them, and you can reenable it by
+  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
+* If the starting the container fails, in particular with a message `Error: network xyz not found`,
+  you might have deleted stuff from docker via your shell. Try deleting the container and image
+  explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
+  container. (this will again take some time)
+* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.
+
+
+# Manual Installation
+Here are known issues/pitfalls with the local setup using `npm`.
+
+* If `CDPATH` is set on your mac/linux system, it might provide issues with `npm start` resulting in a server crash or blank screen. In particular `npm start` will display
+  ```
+  [server] sh: line 0: cd: server: No such file or directory
+  [server] npm run start_server exited with code 1
+  ```
+  As a fix you might need to delete your manually set `CDPATH` environment variable.
+
+# Publication
+Errors concerning uploads to the server.
+
+* Your game overview loads but the server crashes on loading a level: Check your game's github action is identical to the [GameSkeleton's](https://github.com/hhu-adam/GameSkeleton/blob/main/.github/workflows/build.yml), in particular that there is a step about building the "`gameserver`-executable".
@@ -9,8 +9,8 @@ Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https:

 Then, depending on the setup you use, do one of the following:

-* Dev Container: Rebuild the VSCode Devcontainer.
-* Local Setup: in your game's folder run the following:
+* **Dev Container**: Rebuild the VSCode Devcontainer (without Cache!).
+* **Local Setup**: in your game's folder run the following:
  ```
  lake update -R
  lake build
@@ -24,7 +24,7 @@ Then, depending on the setup you use, do one of the following:
    npm install
    ```
    where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
-* Gitpod/Codespaces: Create a fresh one
+* **Gitpod/Codespaces**: Create a fresh one

 This will update your game (and the mathlib version you might be using) to the new lean version.

@@ -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,8 +28,8 @@
    "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",
-    "octokit": "^2.0.14",
+    "lean4web": "github:hhu-adam/lean4web#414d9e62638a392fca278761b4c61a1d2e138bc7",
+    "octokit": "^3.1.2",
    "path-browserify": "^1.0.1",
    "react": "^18.2.0",
    "react-dom": "^18.2.0",
@@ -1,5 +1,6 @@
 #/bin/bash

+# Note: This fails if there is no default toolchain installed
 ELAN_HOME=$(lake env printenv ELAN_HOME)

 # $1 : the game directory
@@ -19,7 +19,8 @@ import { importTrigger, importStatus } from './import.mjs'
 const queueLength = {
  "g/hhu-adam/robo": 2,
  "g/hhu-adam/nng4": 5,
-  "g/djvelleman/stg4": 2,
+  "g/djvelleman/stg4": 0,
+  "g/trequetrum/lean4game-logic": 0,
 }

 const __filename = url.fileURLToPath(import.meta.url);
@@ -28,3 +28,7 @@ do
  #tar -xvzf $f -C games/${OWNER}/${REPO}
  unzip -q -o $f -d ${OWNER}/${REPO}
 done
+
+# Delete temporary files
+rm -f tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip
+rm -fr tmp/${OWNER}_${REPO}_${ARTIFACT_ID}
@@ -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 {}
+    GameServer.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
@@ -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
@@ -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
@@ -1,9 +1,11 @@
-/- 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
 open Elab
 open Parser
@@ -17,7 +19,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
@@ -47,7 +49,8 @@ partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)

 end MyModule

-namespace MyServer.FileWorker
+namespace GameServer.FileWorker
+
 open Lean
 open Lean.Server
 open Lean.Server.FileWorker
@@ -56,8 +59,50 @@ open IO
 open Snapshots
 open JsonRpc

+/--
+Game-specific state to be packed on top of the `Lean.Server.FileWorker.WorkerState`
+used by the lean server.
+-/
+structure WorkerState :=
+  /--
+  Collection of items which are considered unlocked.
+  Tactics and theorems are mixed together.
+  -/
+  inventory : Array String
+  /--
+  Difficulty determines whether tactics/theorems can be locked.
+  * 0: do not check
+  * 1: give warnings when locked items are used
+  * 2: give errors when locked items are used
+  -/
+  difficulty : Nat
+  /--
+  `levelInfo` contains all the (static) information about the level which is not influenced
+  by the user's progress.
+  -/
+  levelInfo : LevelInfo
+deriving ToJson, FromJson
+
+/--
+Pack the `GameServer.FileWorker.WorkerState` on top of the normal worker monad
+`Server.FileWorker.WorkerM`.
+-/
+abbrev WorkerM := StateT WorkerState Server.FileWorker.WorkerM
+
 section Elab

+/-- Add a message. use `(severity := .warning)` to specify the severity-/
+def addMessage (info : SourceInfo) (inputCtx : Parser.InputContext)
+    (severity := MessageSeverity.warning) (s : MessageData) :
+    Elab.Command.CommandElabM Unit := do
+  modify fun st => { st with
+    messages := st.messages.add {
+      fileName := inputCtx.fileName
+      severity := severity
+      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
+      data     := s }}
+
+/-- Deprecated! -/
 def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
    Elab.Command.CommandElabM Unit := do
  modify fun st => { st with
@@ -65,79 +110,96 @@ def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : Me
      fileName := inputCtx.fileName
      severity := MessageSeverity.error
      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
-        data     := s
-      }
-    }
+      data     := s }}

 -- TODO: use HashSet for allowed tactics?
-/-- 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) :
-    Elab.Command.CommandElabM Unit := do
+/--
+Find all tactics in syntax object that are forbidden according to a
+set `allowed` of allowed tactics.
+-/
+partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState : WorkerState)
+    (stx : Syntax) : Elab.Command.CommandElabM Unit := do
+  let levelInfo := workerState.levelInfo
+  -- Parse the syntax object and look for tactics and declarations.
  match stx with
  | .missing => return ()
  | .node _info _kind args =>
+    -- Go inside a node.
    for arg in args do
-      findForbiddenTactics inputCtx levelParams arg
+      findForbiddenTactics inputCtx workerState 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"]
+    -- Atoms might be tactic names or other keywords.
+    -- Note: We whitelisted known keywords because we cannot
+    -- distinguish keywords from tactic names.
+    let allowed := ["with", "fun", "at", "only", "by", "to", "generalizing", "says"]
+    -- Ignore syntax elements that do not start with a letter or are listed above.
    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
+      -- Treat `simp?` and `simp!` like `simp`
+      let val := val.dropRightWhile (fun c => c == '!' || c == '?')
+      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
+        -- Tactic will never be introduced in the game.
+        match workerState.inventory.find? (· == val) with
+        | some _ =>
+          -- Tactic is in the inventory, allow it.
+          -- Note: This case shouldn't be possible...
+          pure ()
        | none =>
-          addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
-        | some _ => pure () -- tactic is in the inventory, allow it.
+          -- Tactic is not in the inventory.
+          addMessageByDifficulty info s!"The tactic '{val}' is not available in this game!"
      | some tac =>
-        if tac.locked then
-          match levelParams.inventory.find? (· == val) with
+        -- Tactic is introduced at some point in the game.
+        if tac.disabled then
+          -- Tactic is disabled in this level.
+          addMessageByDifficulty info s!"The tactic '{val}' is disabled in this level!"
+        else if tac.locked then
+          match workerState.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.
-        else if tac.disabled then
-          addWarningMessage info s!"The tactic '{val}' is disabled in this level!"
+            -- Tactic is marked as locked and not in the inventory.
+            addMessageByDifficulty info s!"You have not unlocked the tactic '{val}' yet!"
+          | some _ =>
+            -- Tactic is in the inventory, allow it.
+            pure ()
  | .ident info _rawVal val _preresolved =>
+    -- Try to resolve the name
    let ns ←
      try resolveGlobalConst (mkIdent val)
-        catch | _ => pure [] -- catch "unknown constant" error
+      -- Catch "unknown constant" error
+      catch | _ => pure []
    for n in ns do
      let some (.thmInfo ..) := (← getEnv).find? n
-          | return () -- not a theorem -> ignore
+        -- Not a theorem, no checks needed.
+        | return ()
+      if some n = levelInfo.statementName then
        -- Forbid the theorem we are proving currently
-        if n = levelParams.statementName then
-          addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
+        addMessage info inputCtx (severity := .error)
+          s!"Structural recursion: you can't use '{n}' to proof itself!"
+      let theoremsAndDefs := levelInfo.lemmas ++ levelInfo.definitions
+      match theoremsAndDefs.find? (·.name == n) with
+      | none =>
+        -- Theorem will never be introduced in this game
+        addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
+      | some thm =>
+        -- Theorem is introduced at some point in the game.
+        if thm.disabled then
+          -- Theorem is disabled in this level.
+          addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!"
+        else if thm.locked then
+          -- Theorem is still locked.
+          addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"

-        let lemmasAndDefs := levelParams.lemmas ++ levelParams.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 =>
-          if lem.locked then
-            addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
-          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
+where addMessageByDifficulty (info : SourceInfo) (s : MessageData) :=
+  -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors
+  -- deppending on difficulty.
+  let difficulty := workerState.difficulty
  if difficulty > 0 then
-    modify fun st => { st with
-      messages := st.messages.add {
-        fileName := inputCtx.fileName
-        severity := if difficulty > 1 then MessageSeverity.error else MessageSeverity.warning
-        pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
-        data     := s
-      }
-    }
+    addMessage info inputCtx (if difficulty > 1 then .error else .warning) s
  else pure ()
-- where addErrorMessage (info : SourceInfo) (s : MessageData) :=
--   pure ()

 open Elab Meta Expr in
+
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
-    (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams)
+    (couldBeEndSnap : Bool) (gameWorkerState : WorkerState)
    (initParams : Lsp.InitializeParams) : IO Snapshot := do
  -- Recognize end snap
  if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
@@ -168,7 +230,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 +248,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 +281,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 +333,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 : WorkerState) (initParams : Lsp.InitializeParams)
      : AsyncElabM (Option Snapshot) := do
    cancelTk.check
    let s ← get
@@ -288,7 +351,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 +373,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 : WorkerState)
      : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
    let ctx ← read
    let some headerSnap := snaps[0]? | panic! "empty snapshots"
@@ -326,21 +389,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
+def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do
  let s ← get
-    let levelParams := s.levelParams
  let ctx ← read
  let oldDoc := (← StateT.lift get).doc
  oldDoc.cancelTk.set
@@ -382,7 +439,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 +454,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 +514,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 : WorkerState) : IO (WorkerContext × Server.FileWorker.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,12 +529,14 @@ 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,
  { doc             := doc
    initHeaderStx   := headerStx
+    currHeaderStx      := headerStx
+    importCachingTask? := none
    pendingRequests := RBMap.empty
    rpcSessions     := RBMap.empty
  })
@@ -486,7 +545,7 @@ end Initialization

 section NotificationHandling

-  def handleDidChange (p : DidChangeTextDocumentParams) : GameWorkerM Unit := do
+def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do
  let docId := p.textDocument
  let changes := p.contentChanges
  let oldDoc := (← StateT.lift get).doc
@@ -503,25 +562,39 @@ end NotificationHandling

 section MessageHandling

-  def handleNotification (method : String) (params : Json) : GameWorkerM Unit := do
-    let handle := fun paramType [FromJson paramType] (handler : paramType → GameWorkerM Unit) =>
+
+/--
+Modified notification handler.
+
+Compare to `Lean.Server.FileWorker.handleNotification`.
+We use the modified `WorkerM` and use our custom `handleDidChange`.
+
+-/
+def handleNotification (method : String) (params : Json) : WorkerM Unit := do
+  let handle := fun paramType [FromJson paramType] (handler : paramType → WorkerM Unit) =>
    (StateT.lift <| parseParams paramType params) >>= handler
  match method with
+  -- Modified `textDocument/didChange`, using a custom `handleDidChange`
  | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
+  -- unmodified
  | "$/cancelRequest"        => handle CancelParams (handleCancelRequest ·)
+  -- unmodified
  | "$/lean/rpc/release"     => handle RpcReleaseParams (handleRpcRelease ·)
+  -- unmodified
  | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
+  -- New. TODO: What is this for?
+  | "$/setTrace"        => pure ()
  | _                        => throwServerError s!"Got unsupported notification method: {method}"

 end MessageHandling

 section MainLoop
-  partial def mainLoop : GameWorkerM Unit := do
-    let ctx ← read
-    let mut st ← StateT.lift get
-    let msg ← ctx.hIn.readLspMessage
-    let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
-        : IO PendingRequestMap := do
+
+/--
+Erase finished tasks if there are no errors.
+-/
+private def filterFinishedTasks (acc : PendingRequestMap) (id : RequestID)
+    (task : Task (Except IO.Error Unit)) : IO PendingRequestMap := do
  if (← hasFinished task) then
    /- Handler tasks are constructed so that the only possible errors here
    are failures of writing a response into the stream. -/
@@ -529,9 +602,17 @@ section MainLoop
      throwServerError s!"Failed responding to request {id}: {e}"
    pure <| acc.erase id
  else pure acc
-    let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests
-    st := { st with pendingRequests }

+/--
+The main-loop.
+-/
+partial def mainLoop : WorkerM Unit := do
+  let ctx ← read
+  let mut st ← StateT.lift get
+  let msg ← ctx.hIn.readLspMessage
+  let pendingRequests ← st.pendingRequests.foldM (fun acc id task =>
+    filterFinishedTasks acc id task) st.pendingRequests
+  st := { st with pendingRequests }
  -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired.
  for (id, seshRef) in st.rpcSessions do
    let sesh ← seshRef.get
@@ -539,34 +620,47 @@ section MainLoop
      st := { st with rpcSessions := st.rpcSessions.erase id }

  set st
+
+  -- Process the RPC-message and restart main-loop.
  match msg with
+  | Message.request id "shutdown" none =>
+    ctx.hOut.writeLspResponse ⟨id, Json.null⟩
+    mainLoop
  | Message.request id method (some params) =>
+    -- Requests are handled by the unmodified lean server.
    handleRequest id method (toJson params)
    mainLoop
  | Message.notification "exit" none =>
    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}}
-      mainLoop
  | Message.notification method (some params) =>
+    -- Custom notification handler
    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 +672,25 @@ 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 : WorkerState := {
+      inventory := initializationOptions.inventory
+      difficulty := initializationOptions.difficulty
+      levelInfo
+    }
+    let (ctx, st) ← initializeWorker meta i o e initParams opts gameDir gameWorkerState
+    -- Run the main loop
    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,14 +700,21 @@ 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
+/--
+The main function. Simply wrapping `initAndRunWorker`.
+
+TODO: The first arg `args[0]` is always expected to be `--server`. We could drop this completely.
+-/
+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
-    -- 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
+    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
    e.flush
    IO.Process.exit exitCode.toUInt8
@@ -605,4 +722,4 @@ def workerMain (opts : Options) : IO UInt32 := do
    e.putStrLn s!"worker initialization error: {err}"
    return (1 : UInt32)

-end MyServer.FileWorker
+end GameServer.FileWorker
@@ -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?
  }
+  capabilities := p.capabilities
+  trace := p.trace
+  workspaceFolders? := p.workspaceFolders?
 }

-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
-
 end Game
@@ -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 : β) :=
@@ -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
@@ -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
@@ -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
@@ -4,10 +4,10 @@
 [{"url": "https://github.com/leanprover/std4.git",
   "type": "git",
   "subDir": null,
-   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
+   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
   "name": "std",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
+   "inputRev": "v4.5.0",
   "inherited": false,
   "configFile": "lakefile.lean"}],
 "name": "GameServer",
@@ -1 +1 @@
-leanprover/lean4:v4.3.0
+leanprover/lean4:v4.5.0
Author	SHA1	Message	Date
Jon Eugster	d689c7ec86	update npm deps	2024-02-23 18:58:15 +01:00
Jon Eugster	16c979a6c2	bump npm dependencies	2024-02-23 18:58:06 +01:00
Jon Eugster	698a88c545	Update troubleshoot.md	2024-02-16 10:57:02 +01:00
Jon Eugster	3b660c5185	Merge branch 'dev'. Bump to v4.5.0	2024-02-02 12:44:32 +01:00
Jon Eugster	ebb8c98145	bump to v4.5.0	2024-02-02 12:43:58 +01:00
Jon Eugster	4abf05b77e	Merge branch 'dev' into v4.5.0-bump	2024-02-02 12:11:55 +01:00
Jon Eugster	df423aaace	Merge pull request #181 from Wzixiao/auto-mobile-layout Modify logic for preferences	2024-01-26 12:06:29 +01:00
Jon Eugster	a67dcb306f	fix indent	2024-01-26 11:55:00 +01:00
Jon Eugster	37582e04d4	fix errors for disabled tactics #188	2024-01-26 11:54:36 +01:00
ran	9d4a6df139	Remove MobileContext and use PreferencesContext instead	2024-01-23 22:59:43 +08:00
Jon Eugster	26202e5f36	fix typo	2024-01-22 14:09:54 +01:00
Jon Eugster	ed017fa605	documentation & cleanup in FileWorker	2024-01-22 14:06:52 +01:00
Jon Eugster	36bc52c960	add logic game to landing page	2024-01-22 13:31:43 +01:00
Jon Eugster	e085f2f106	Merge pull request #186 from Geoc2022/main Cleaned up Documentation	2024-01-22 13:26:30 +01:00
Jon Eugster	e975c455fe	Update doc/DOCUMENTATION.md	2024-01-22 12:44:12 +01:00
geo	c006be5a9f	Fix minor typos	2024-01-20 16:15:15 -05:00
geo	49379a0930	Fix link references	2024-01-20 16:02:46 -05:00
geo	03076b0161	Add example `npm start` message	2024-01-19 10:52:26 -05:00
geo	bfb60ffedd	Updated "Doc entries"	2024-01-19 10:41:20 -05:00
Jon Eugster	ca576542ba	whitelist generalizing and says. #173	2024-01-19 10:53:43 +01:00
Jon Eugster	fd5e507541	lint: fix line widths	2024-01-19 10:50:48 +01:00
Jon Eugster	c103eeacfa	fix: case insensitive url in local store #183	2024-01-18 14:57:50 +01:00
Jon Eugster	e277a48749	add changelog file	2024-01-18 14:19:32 +01:00
Jon Eugster	16ff701518	Update troubleshoot.md	2024-01-18 13:51:33 +01:00
Jon Eugster	20ca385e14	Update README.md	2024-01-18 13:48:43 +01:00
Jon Eugster	5a38543e3b	Merge pull request #185 from leanprover-community/joneugster-patch-1 Update docs	2024-01-18 13:48:08 +01:00
Jon Eugster	a4a6f2e725	Merge pull request #184 from leanprover-community/joneugster-patch-1-1 Create troubleshoot.md	2024-01-18 13:47:48 +01:00
Jon Eugster	cc89e78e4c	Create troubleshoot.md	2024-01-18 13:47:16 +01:00
Jon Eugster	c533a635c2	Update docs	2024-01-18 13:47:08 +01:00
ran	ab98eaa3ba	Change the selected button to a slider	2024-01-16 11:21:46 +08:00
Jon Eugster	7114a8c4cb	fix: remove tmp files after import	2024-01-15 12:15:12 +01:00
Jon Eugster	b7eb15184d	Merge pull request #182 from lnay/patch-1 Minor: correct error in markdown	2024-01-15 11:24:46 +01:00
Luke Naylor	892c70165a	Minor: correct error in markdown	2024-01-12 21:07:19 +00:00
ran	8929813e48	Added a missing space regarding code style in store.ts	2024-01-12 23:48:47 +08:00
ran	5d88cd6739	Remove logically duplicated code	2024-01-12 23:47:04 +08:00
ran	d16956da9b	Modify the props definition of the preference popup component	2024-01-12 23:43:21 +08:00
ran	e15e5af126	Add todo about setMobile	2024-01-12 23:31:22 +08:00
ran	8c93b3c5b3	Modify logic for all preferences	2024-01-12 23:29:03 +08:00
Jon Eugster	cd1d212a3c	npm audit	2024-01-10 15:40:57 +01:00
Jon Eugster	406c2799b1	bump to v4.5.0-rc1	2023-12-25 12:07:56 +01:00
Jon Eugster	e579071a3b	Merge branch 'v4.4.0'	2023-12-25 12:01:49 +01:00
Jon Eugster	8cdac88b5a	bump to v4.4.0	2023-12-22 13:28:49 +01:00
Jon Eugster	7882958f54	Update update_game.md	2023-12-18 16:20:26 +01:00
Alexander Bentkamp	c9f97b3285	remove watchdog	2023-12-15 22:17:09 +01:00
Jon Eugster	614b762b6c	rename LemmaDoc into TheoremDoc and so on	2023-12-15 16:05:49 +01:00
Jon Eugster	c4f4dbdc6b	update doc #171	2023-12-15 00:04:54 +01:00
Jon Eugster	5a78118bb6	improve display of buttons on mobile	2023-12-14 23:04:18 +01:00
Jon Eugster	a6775d5495	move 'show more help'-button on mobile #143	2023-12-14 22:13:44 +01:00
Jon Eugster	03a370464b	fix altTitle for backwards compatibility	2023-12-14 22:06:53 +01:00
Jon Eugster	eaa214ec37	improve world tree on mobile #101	2023-12-14 21:59:47 +01:00
Jon Eugster	d7f1f70d41	Merge pull request #168 from Wzixiao/mobile-option Mobile option (template)	2023-12-14 21:53:08 +01:00
Jon Eugster	2d0f69d337	fix: prevent multiple NewTactic per level #125	2023-12-14 21:44:36 +01:00
Jon Eugster	1ab50710f5	fix: update rules slider on erasing progress #157	2023-12-14 21:24:08 +01:00
Jon Eugster	e76e287763	fix: persistent lemma tab #144	2023-12-14 21:14:42 +01:00
Jon Eugster	5fd49abb90	improve hover text for inventory items #144	2023-12-14 21:05:37 +01:00
Jon Eugster	4b7d540a80	update fortawesome packages to matching versions	2023-12-14 20:49:38 +01:00
Jon Eugster	aec196deff	add button to copy inventory item name to clipboard #144	2023-12-14 20:26:31 +01:00
Jon Eugster	ae636a03ed	fix: hide hidden inventory items in overview #169	2023-12-14 19:01:11 +01:00
Jon Eugster	deec431620	Merge branch 'dev' into mobile-option	2023-12-13 15:20:24 +01:00
ran	9f692ccf61	Add basic preference framework and mobile options and Add missing files	2023-12-13 00:37:50 +08:00
ran	47d7f606c6	Add basic preference framework and mobile options	2023-12-13 00:34:38 +08:00
Jon Eugster	5aa0764844	add comment	2023-12-12 14:42:02 +01:00
Jon Eugster	93c55dc9f7	Merge pull request #167 from Wzixiao/home-button-margin Adjust the margin of the home button.	2023-12-12 13:43:21 +01:00
Jon Eugster	aab7441323	Merge pull request #166 from Wzixiao/app-bar-align-center Adjust the top navigation bar to center both the Home button and some divs on the right.	2023-12-12 13:42:00 +01:00
ran	2ba36b91d5	Adjust the margin of the home button	2023-12-12 19:51:20 +08:00
ran	a2726ae287	Adjust the top navigation bar so that it is centered above and below	2023-12-12 19:29:21 +08:00
ran	7515561883	Add a button to toggle mobile	2023-12-12 19:17:55 +08:00
Jon Eugster	5f52e23f29	Update hints.md	2023-12-11 16:04:37 +01:00
Jon Eugster	b067dea6e7	Update README.md	2023-12-09 23:38:18 +01:00
Jon Eugster	4edf67f0d6	Update README.md	2023-12-09 23:37:59 +01:00
Jon Eugster	004f81835f	write more docs	2023-12-09 23:34:39 +01:00