work on network interruption errors

.env

@@ -0,0 +1 @@
+LEAN4GAME_SINGLE_GAME=false

.github/workflows/build.yml

@@ -5,17 +5,7 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-      - name: install elan
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v3
       - uses: actions/setup-node@v3
-      - name: print lean and lake versions
-        run: |
-          lean --version
-          lake --version
       - run: npm install
       - run: npm run build

.gitignore

@@ -1,5 +1,4 @@
 node_modules
 client/dist
-games/
-server/.lake
-**/.DS_Store
+server/build
+**/lake-packages/

NOTES.md

@@ -15,6 +15,9 @@ npm install -g http-server
 
 ```
 git clone https://github.com/hhu-adam/NNG4.git
+cd NNG4
+docker rmi nng4:latest
+docker build --pull --rm -f "Dockerfile" -t nng4:latest "."
 ```
 
 
@@ -143,6 +146,12 @@ Activate config:
 ```
 
 
+## Install `unzip` for Importing Docker Images
+
+```
+sudo apt-get install unzip
+```
+
 ## Install bubblewrap (bwrap)
 ```
 sudo apt-get install bubblewrap

README.md

@@ -2,33 +2,30 @@
 
 This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
 
+The project 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/)
+of Kevin Buzzard and Mohammad Pedramfar.
+The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
+
 ## Creating a Game
 
-Please follow the tutorial [Creating a Game](doc/create_game.md). In particular, the following steps might be of interest:
+Please follow the tutorial [Creating a Game](doc/create_game.md).
+In particular step 5 thereof explains [How to Run Games Locally](doc/running_locally.md).
 
-* 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)
+### Publishing a Game
+
+We encourage anybody to have games hosted on our [Lean Game Server](https://adam.math.hhu.de) for anybody to play. For that you simply need to contact us with the link to your game repo. We are also happy to add work-in-progress games and games in any language.
+
+For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).
 
 ## Documentation
 
-The documentation is very much work in progress but the linked documentation here
-should be up-to-date:
+The documentation for the game engine itself is still missing, but there is [Creating a Game](doc/create_game.md) explaining the API to create a game.
 
-### Game creation API
+Some documentation:
 
-- [Creating a Game](doc/create_game.md): **the main document to consult**.
-- [More about Hints](doc/hints.md): describes the `Hint` and `Branch` tactic.
-
-### Frontend API
-
-* [How to Run Games Locally](doc/running_locally.md): play a game on your computer
-* [How to Update an existing Game](doc/update_game.md): update to a new lean version
-* [How to Publishing a Game](doc/publish_game.md): load your game to adam.math.hhu.de for others to play
-
-### Backend
-
-not written yet
+- [NPM Scripts](doc/npm_scripts.md)
+- [Old documentation](doc/DOCUMENTATION.md)
 
 ## Contributing
 
@@ -37,10 +34,3 @@ Contributions to `lean4game` are always welcome!
 ## Security
 
 Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server with bubblewrap.
-
-## Credits
-
-The project 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).

client/public/index.html

@@ -33,7 +33,7 @@
       </p>
     </div>
   </noscript>
-  <script type="module" src="/client/src/index.tsx"></script>
+  <script src="bundle.js"></script>
 </body>
 
 </html>

client/src/app.tsx

@@ -9,37 +9,20 @@ import '@fontsource/roboto/700.css';
 import './css/reset.css';
 import './css/app.css';
 import { MobileContext } from './components/infoview/context';
-import { useMobile } from './hooks';
-import { AUTO_SWITCH_THRESHOLD, getWindowDimensions} from './state/preferences';
+import { useWindowDimensions } from './window_width';
 
 export const GameIdContext = React.createContext<string>(undefined);
 
 function App() {
-  const { mobile, setMobile, lockMobile, setLockMobile } = useMobile();
-
   const params = useParams()
   const gameId = "g/" + params.owner + "/" + params.repo
-
-  const automaticallyAdjustLayout = () => {
-    const {width} = getWindowDimensions()
-    setMobile(width < AUTO_SWITCH_THRESHOLD)
-  }
-
-  React.useEffect(()=>{
-    if (!lockMobile){
-      void automaticallyAdjustLayout()
-      window.addEventListener('resize', automaticallyAdjustLayout)
-
-      return () => {
-        window.removeEventListener('resize', automaticallyAdjustLayout)
-      }
-    }
-  }, [lockMobile])
+  const {width, height} = useWindowDimensions()
+  const [mobile, setMobile] = React.useState(width < 800)
 
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>
-        <MobileContext.Provider value={{mobile, setMobile, lockMobile, setLockMobile}}>
+        <MobileContext.Provider value={{mobile, setMobile}}>
           <Outlet />
         </MobileContext.Provider>
       </GameIdContext.Provider>

client/src/components/app_bar.tsx

@@ -5,7 +5,7 @@ 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, faMobileScreenButton, faDesktop, faGear } from '@fortawesome/free-solid-svg-icons'
+  faCircleInfo, faTerminal } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from "../app"
 import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context"
 import { GameInfo, useGetGameInfoQuery } from '../state/api'
@@ -150,23 +150,22 @@ function InventoryButton({pageNumber, setPageNumber}) {
 }
 
 /** the navigation bar on the welcome page */
-export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo, togglePreferencesPopup} : {
+export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo} : {
   pageNumber: number,
   setPageNumber: any,
   gameInfo: GameInfo,
   toggleImpressum: any,
   toggleEraseMenu: any,
   toggleUploadMenu: any,
-  toggleInfo: any,
-  togglePreferencesPopup: () => void;
+  toggleInfo: any
 }) {
   const gameId = React.useContext(GameIdContext)
   const gameProgress = useAppSelector(selectProgress(gameId))
-  const {mobile, setMobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(MobileContext)
   const [navOpen, setNavOpen] = React.useState(false)
 
   return <div className="app-bar">
-    <div className='app-bar-left'>
+    <div>
       <Button inverted="false" title="back to games selection" to="/">
         <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
       </Button>
@@ -195,9 +194,6 @@ 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>
 }
@@ -241,7 +237,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=
       </> :
       <>
         {/* DESKTOP VERSION */}
-        <div className='app-bar-left'>
+        <div>
           <HomeButton isDropdown={false} />
           <span className="app-bar-title">{worldTitle && `World: ${worldTitle}`}</span>
         </div>

client/src/components/hints.tsx

@@ -1,7 +1,6 @@
 import { GameHint } from "./infoview/rpc_api";
 import * as React from 'react';
 import Markdown from './markdown';
-import { ProofStep } from "./infoview/context";
 
 export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
   return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
@@ -44,24 +43,3 @@ export function DeletedHints({hints} : {hints: GameHint[]}) {
     {hiddenHints.map((hint, i) => <DeletedHint key={`deleted-hidden-hint-${i}`} hint={hint}/>)}
   </>
 }
-
-/** Filter hints to not show consequtive identical hints twice.
- *
- * This function takes a `ProofStep[]` and extracts the hints in form of an
- * element of type `GameHint[][]` where it removes hints that are identical to hints
- * appearing in the previous step. Hidden hints are not filtered.
- *
- * This effectively means we prevent consequtive identical hints from being shown.
- */
-export function filterHints(proof: ProofStep[]): GameHint[][] {
-  return proof.map((step, i) => {
-    if (i == 0){
-      return step.hints
-    } else {
-      // TODO: Writing all fields explicitely is somewhat fragile to changes, is there a
-      // good way to shallow-compare objects?
-      return step.hints.filter((hint) => hint.hidden ||
-        (proof[i-1].hints.find((x) => (x.text == hint.text && x.hidden == hint.hidden)) === undefined))
-    }
-  })
-}

client/src/components/infoview/context.ts

@@ -62,18 +62,12 @@ export const ProofStateContext = React.createContext<{
   setProofState: () => {},
 })
 
-export interface IMobileContext {
+export const MobileContext = React.createContext<{
   mobile : boolean,
   setMobile: React.Dispatch<React.SetStateAction<Boolean>>,
-  lockMobile: boolean,
-  setLockMobile: React.Dispatch<React.SetStateAction<Boolean>>,
-}
-
-export const MobileContext = React.createContext<IMobileContext>({
-  mobile: false,
+}>({
+  mobile : false,
   setMobile: () => {},
-  lockMobile: false,
-  setLockMobile: () => {}
 })
 
 export const WorldLevelIdContext = React.createContext<{

client/src/components/infoview/main.tsx

@@ -1,6 +1,7 @@
 /* Partly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/main.tsx */
 
 import * as React from 'react';
+import {useEffect} from 'react';
 import type { DidCloseTextDocumentParams, DidChangeTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol';
 
 import 'tachyons/css/tachyons.css';
@@ -34,7 +35,7 @@ import { Button } from '../button';
 import { CircularProgress } from '@mui/material';
 import { GameHint } from './rpc_api';
 import { store } from '../../state/store';
-import { Hints, filterHints } from '../hints';
+import { Hints } from '../hints';
 
 /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
  * always present, or the monaco editor cannot start.
@@ -156,7 +157,7 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
 
   const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
 
-  console.debug(`template: ${props.data?.template}`)
+  console.debug(`template: ${props.data.template}`)
 
   // React.useEffect (() => {
   //   if (props.data.template) {
@@ -327,6 +328,17 @@ export function TypewriterInterfaceWrapper(props: { world: string, level: number
   // it's important not to reconstruct the `WithBlah` wrappers below since they contain state
   // that we want to persist.
 
+  // Catch loss of internet connection
+  try {
+    const editor = React.useContext(MonacoEditorContext)
+    const model = editor.getModel()
+    if (!model) {
+      return <p>no internet?</p>
+    }
+  } catch {
+    return <p>no internet??</p>
+  }
+
   if (!serverVersion) { return <></> }
   if (serverStoppedResult) {
     return <div>
@@ -338,20 +350,51 @@ export function TypewriterInterfaceWrapper(props: { world: string, level: number
   return <TypewriterInterface props={props} />
 }
 
+/** Delete all proof lines starting from a given line.
+* Note that the first line (i.e. deleting everything) is `1`!
+*/
+function deleteProof(line: number) {
+  const editor = React.useContext(MonacoEditorContext)
+  const { proof } = React.useContext(ProofContext)
+  const { setSelectedStep } = React.useContext(SelectionContext)
+  const { setDeletedChat, showHelp } = React.useContext(DeletedChatContext)
+  const { setTypewriterInput } = React.useContext(InputModeContext)
+
+  return (ev) => {
+    if (editor) {
+      const model = editor.getModel()
+      if (model) {
+        let deletedChat: Array<GameHint> = []
+        proof.slice(line).map((step, i) => {
+          // Only add these hidden hints to the deletion stack which were visible
+          deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
+        })
+        setDeletedChat(deletedChat)
+        editor.executeEdits("typewriter", [{
+          range: monaco.Selection.fromPositions(
+            { lineNumber: line, column: 1 },
+            model.getFullModelRange().getEndPosition()
+          ),
+          text: '',
+          forceMoveMarkers: false
+        }])
+        setSelectedStep(undefined)
+        setTypewriterInput(proof[line].command)
+        ev.stopPropagation()
+      }
+    }
+  }
+}
+
 /** The interface in command line mode */
 export function TypewriterInterface({props}) {
-  const ec = React.useContext(EditorContext)
   const gameId = React.useContext(GameIdContext)
   const editor = React.useContext(MonacoEditorContext)
-  const model = editor.getModel()
-  const uri = model.uri.toString()
 
   const [disableInput, setDisableInput] = React.useState<boolean>(false)
-  const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
-  const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
+  const { showHelp, setShowHelp } = React.useContext(DeletedChatContext)
   const {mobile} = React.useContext(MobileContext)
   const { proof } = React.useContext(ProofContext)
-  const { setTypewriterInput } = React.useContext(InputModeContext)
   const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
 
   const proofPanelRef = React.useRef<HTMLDivElement>(null)
@@ -359,33 +402,9 @@ export function TypewriterInterface({props}) {
   // const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
   // const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
 
-  const rpcSess = useRpcSessionAtPos({uri: uri, line: 0, character: 0})
-
-  /** Delete all proof lines starting from a given line.
-  * Note that the first line (i.e. deleting everything) is `1`!
-  */
-  function deleteProof(line: number) {
-    return (ev) => {
-      let deletedChat: Array<GameHint> = []
-      filterHints(proof).slice(line).map((hintsAtStep, i) => {
-        // Only add these hidden hints to the deletion stack which were visible
-        deletedChat = [...deletedChat, ...hintsAtStep.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
-      })
-      setDeletedChat(deletedChat)
-
-      editor.executeEdits("typewriter", [{
-        range: monaco.Selection.fromPositions(
-          { lineNumber: line, column: 1 },
-          editor.getModel().getFullModelRange().getEndPosition()
-        ),
-        text: '',
-        forceMoveMarkers: false
-      }])
-      setSelectedStep(undefined)
-      setTypewriterInput(proof[line].command)
-      ev.stopPropagation()
-    }
-  }
+  // rpc session
+  // editor, model or uri might be null if connection is broken
+  const rpcSess = useRpcSessionAtPos({uri: editor?.getModel()?.uri?.toString() ?? '', line: 0, character: 0})
 
   function toggleSelectStep(line: number) {
     return (ev) => {
@@ -400,8 +419,8 @@ export function TypewriterInterface({props}) {
     }
   }
 
-   // Scroll to the end of the proof if it is updated.
-   React.useEffect(() => {
+  // Scroll to the end of the proof if it is updated.
+  React.useEffect(() => {
     if (proof?.length > 1) {
       proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
     } else {
@@ -456,17 +475,6 @@ export function TypewriterInterface({props}) {
 
   let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false
 
-
-  useServerNotificationEffect("$/game/loading", (params : any) => {
-    if (params.kind == "loadConstants") {
-      setLoadingProgress(params.counter/100*50)
-    } else if (params.kind == "finalizeExtensions") {
-      setLoadingProgress(50 + params.counter/150*50)
-    } else {
-      console.error(`Unknown loading kind: ${params.kind}`)
-    }
-  })
-
   return <div className="typewriter-interface">
     <RpcContext.Provider value={rpcSess}>
     <div className="content">
@@ -493,20 +501,18 @@ export function TypewriterInterface({props}) {
                       <Markdown>{props.data?.introduction}</Markdown>
                     </div>
                   }
-                  {mobile &&
+                  {mobile && <>
                     <Hints key={`hints-${i}`}
                       hints={step.hints} showHidden={showHelp.has(i)} step={i}
                       selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
+                    {i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
+                      <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
+                        Show more help!
+                      </Button>
+                    }
+                  </>
                   }
                   <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/>
-
-                  {mobile && i == proof.length - 1 &&
-                    hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-                    <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
-                      Show more help!
-                    </Button>
-                  }
-
                   {/* Show a message that there are no goals left */}
                   {!step.goals.length && (
                     <div className="message information">
@@ -523,7 +529,7 @@ export function TypewriterInterface({props}) {
               }
             })}
             {mobile && completed &&
-              <div className="button-row mobile">
+              <div className="button-row">
                 {props.level >= props.worldSize ?
                   <Button to={`/${gameId}`}>
                     <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
@@ -535,7 +541,7 @@ export function TypewriterInterface({props}) {
                 }
               </div>
             }
-          </> : <CircularProgress variant="determinate" value={loadingProgress} />
+          </> : <CircularProgress />
         }
       </div>
     </div>

client/src/components/infoview/typewriter.tsx

@@ -68,8 +68,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
 
   /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
-  const model = editor.getModel()
-  const uri = model.uri.toString()
+  const model = editor?.getModel()
+  const uri = model?.uri?.toString()
 
   const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
   const [processing, setProcessing] = useState(false)
@@ -91,11 +91,15 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
    */
   const loadAllGoals = React.useCallback(() => {
 
+    if (!model || ! uri) {
+      return
+    }
+
     let goalCalls = []
     let msgCalls = []
 
     // For each line of code ask the server for the goals and the messages on this line
-    for (let i = 0; i < model.getLineCount(); i++) {
+    for (let i = 0; i < model?.getLineCount(); i++) {
       goalCalls.push(
         rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
       )
@@ -158,7 +162,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
           // with no goals there will be no hints.
           let hints : GameHint[] = goals.goals.length ? goals.goals[0].hints : []
 
-          console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
+          console.debug(`Command (${i}): `, i ? model?.getLineContent(i) : '')
           console.debug(`Goals: (${i}): `, goalsToString(goals)) //
           console.debug(`Hints: (${i}): `, hints)
           console.debug(`Errors: (${i}): `, messages)
@@ -166,7 +170,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
           tmpProof.push({
             // the command of the line above. Note that `getLineContent` starts counting
             // at `1` instead of `zero`. The first ProofStep will have an empty command.
-            command: i ? model.getLineContent(i) : '',
+            command: i ? model?.getLineContent(i) : '',
             // TODO: store correct data
             goals: goals.goals,
             // only need the hints of the active goals in chat
@@ -185,6 +189,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   // Run the command
   const runCommand = React.useCallback(() => {
     if (processing) {return}
+    if (!uri) {return}
 
     // TODO: Desired logic is to only reset this after a new *error-free* command has been entered
     setDeletedChat([])
@@ -195,7 +200,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
       editor.executeEdits("typewriter", [{
         range: monaco.Selection.fromPositions(
           pos,
-          editor.getModel().getFullModelRange().getEndPosition()
+          model.getFullModelRange().getEndPosition()
         ),
         text: typewriterInput.trim() + "\n",
         forceMoveMarkers: false
@@ -204,7 +209,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     }
 
     editor.setPosition(pos)
-  }, [typewriterInput, editor])
+  }, [typewriterInput, editor, model])
 
   useEffect(() => {
     if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) {
@@ -220,12 +225,14 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
 
   // React when answer from the server comes back
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
+    if (!uri) {return}
+
     if (params.uri == uri) {
       setProcessing(false)
       loadAllGoals()
       if (!hasErrors(params.diagnostics)) {
         //setTypewriterInput("")
-        editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
+        editor.setPosition(model.getFullModelRange().getEndPosition())
       }
     } else {
       // console.debug(`expected uri: ${uri}, got: ${params.uri}`)
@@ -234,7 +241,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     // TODO: This is the wrong place apparently. Where do wee need to load them?
     // TODO: instead of loading all goals every time, we could only load the last one
     // loadAllGoals()
-  }, [uri]);
+  }, [uri, editor, model]);
 
   useEffect(() => {
     const myEditor = monaco.editor.create(inputRef.current!, {
@@ -304,10 +311,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   // BUG: Causes `file closed` error
   //TODO: Intention is to run once when loading, does that work?
   useEffect(() => {
-    console.debug(`time to update: ${uri} \n ${rpcSess}`)
-    console.debug(rpcSess)
     loadAllGoals()
-  }, [rpcSess])
+  }, [])
 
   /** Process the entered command */
   const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {

client/src/components/inventory.tsx

@@ -2,21 +2,19 @@ import * as React from 'react';
 import { useState, useEffect } from 'react';
 import '../css/inventory.css'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faLock, faBan, faCheck } from '@fortawesome/free-solid-svg-icons'
-import { faClipboard } from '@fortawesome/free-regular-svg-icons'
+import { faLock, faBan } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from '../app';
 import Markdown from './markdown';
 import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
+import { QueryStatus } from '@reduxjs/toolkit/query/react'
 import { selectDifficulty, selectInventory } from '../state/progress';
 import { store } from '../state/store';
 import { useSelector } from 'react-redux';
 
-export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=false} :
+export function Inventory({levelInfo, openDoc, enableAll=false} :
   {
     levelInfo: LevelInfo|InventoryOverview,
     openDoc: (props: {name: string, type: string}) => void,
-    lemmaTab: any,
-    setLemmaTab: any,
     enableAll?: boolean,
   }) {
 
@@ -34,20 +32,19 @@ export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=
       }
       <h2>Theorems</h2>
       {levelInfo?.lemmas &&
-        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} level={levelInfo} enableAll={enableAll} tab={lemmaTab} setTab={setLemmaTab}/>
+        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} defaultTab={levelInfo?.lemmaTab} level={levelInfo} enableAll={enableAll}/>
       }
     </div>
   )
 }
 
-function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, level=undefined, enableAll=false} :
+function InventoryList({items, docType, openDoc, defaultTab=null, level=undefined, enableAll=false} :
   {
     items: InventoryTile[],
     docType: string,
     openDoc(props: {name: string, type: string}): void,
-    tab?: any,
-    setTab?: any,
-    level?: LevelInfo|InventoryOverview,
+    defaultTab? : string,
+    level? : LevelInfo|InventoryOverview,
     enableAll?: boolean,
   }) {
   // TODO: `level` is only used in the `useEffect` below to check if a new level has
@@ -63,6 +60,8 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev
   }
   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
@@ -70,6 +69,13 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev
   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">
@@ -81,29 +87,24 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev
       {[...modifiedItems].sort(
           // For lemas, sort entries `available > disabled > locked`
           // otherwise alphabetically
-          (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
+          (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled)
         ).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => {
             return <InventoryItem key={`${item.category}-${item.name}`}
-              item={item}
               showDoc={() => {openDoc({name: item.name, type: docType})}}
               name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false}
-              disabled={item.disabled} newly={item.new} enableAll={enableAll} />
+              disabled={item.disabled} newly={item.new} enableAll={enableAll}/>
         })
       }
     </div>
     </>
 }
 
-function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
+function InventoryItem({name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
   const icon = locked ? <FontAwesomeIcon icon={faLock} /> :
-               disabled ? <FontAwesomeIcon icon={faBan} /> : item.st
+               disabled ? <FontAwesomeIcon icon={faBan} /> : ""
   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" : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
-
-  const [copied, setCopied] = useState(false)
+                disabled ? "Not available in this level" : ""
 
   const handleClick = () => {
     if (enableAll || !locked) {
@@ -111,21 +112,26 @@ function InventoryItem({item, name, displayName, locked, disabled, newly, showDo
     }
   }
 
-  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>
+}
 
-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>
+/** Wrapper to catch rejected/pending queries. */
+function DocContent({doc}) {
+  switch(doc.status) {
+    case QueryStatus.fulfilled:
+      return <>
+        <h1 className="doc">{doc.data.displayName}</h1>
+        <p><code>{doc.data.statement}</code></p>
+        {/* <code>docstring: {doc.data.docstring}</code> */}
+        <Markdown>{doc.data.content}</Markdown>
+      </>
+    case QueryStatus.rejected:
+      return <p>Looks like there is a connection problem!</p>
+    case QueryStatus.pending:
+      return <p>Loading...</p>
+    default:
+      return <></>
+  }
 }
 
 export function Documentation({name, type, handleClose}) {
@@ -134,10 +140,7 @@ export function Documentation({name, type, handleClose}) {
 
   return <div className="documentation">
     <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h1 className="doc">{doc.data?.displayName}</h1>
-    <p><code>{doc.data?.statement}</code></p>
-    {/* <code>docstring: {doc.data?.docstring}</code> */}
-    <Markdown>{doc.data?.content}</Markdown>
+      <DocContent doc={doc} />
   </div>
 }
 
@@ -145,25 +148,16 @@ 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} lemmaTab={lemmaTab} setLemmaTab={setLemmaTab}/>
+      <Inventory levelInfo={levelInfo} openDoc={setInventoryDoc} enableAll={true}/>
     }
   </div>
 }

client/src/components/landing_page.tsx

@@ -7,12 +7,11 @@ import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 
 import '../css/landing_page.css'
+import coverRobo from '../assets/covers/formaloversum.png'
 import bgImage from '../assets/bg.jpg'
 
 import Markdown from './markdown';
 import {PrivacyPolicyPopup} from './popup/privacy_policy'
-import { GameTile, useGetGameInfoQuery } from '../state/api'
-import path from 'path';
 
 const flag = {
   'Dutch': '🇳🇱',
@@ -20,7 +19,6 @@ const flag = {
   'French': '🇫🇷',
   'German': '🇩🇪',
   'Italian': '🇮🇹',
-  'Spanish': '🇪🇸',
 }
 
 function GithubIcon({url='https://github.com'}) {
@@ -34,42 +32,47 @@ function GithubIcon({url='https://github.com'}) {
     </div>
 }
 
-function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
+function GameTile({
+  title,
+  gameId,
+  intro, // Catchy intro phrase.
+  image=null,
+  worlds='?',
+  levels='?',
+  prereq='&ndash;', // Optional list of games that this game builds on. Use markdown.
+  description, // Longer description. Supports Markdown.
+  language}) {
 
   let navigate = useNavigate();
   const routeChange = () =>{
     navigate(gameId);
   }
 
-  if (typeof data === 'undefined') {
-    return <></>
-  }
-
   return <div className="game" onClick={routeChange}>
     <div className="wrapper">
-      <div className="title">{data.title}</div>
-      <div className="short-description">{data.short}
+      <div className="title">{title}</div>
+      <div className="short-description">{intro}
       </div>
-      { data.image ? <img className="image" src={path.join("data", gameId, data.image)} alt="" /> : <div className="image"/> }
-      <div className="long description"><Markdown>{data.long}</Markdown></div>
+      { image ? <img className="image" src={image} alt="" /> : <div className="image"/> }
+      <div className="long description"><Markdown>{description}</Markdown></div>
     </div>
     <table className="info">
       <tbody>
       <tr>
         <td title="consider playing these games first.">Prerequisites</td>
-        <td><Markdown>{data.prerequisites.join(', ')}</Markdown></td>
+        <td><Markdown>{prereq}</Markdown></td>
       </tr>
       <tr>
         <td>Worlds</td>
-        <td>{data.worlds}</td>
+        <td>{worlds}</td>
       </tr>
       <tr>
         <td>Levels</td>
-        <td>{data.levels}</td>
+        <td>{levels}</td>
       </tr>
       <tr>
         <td>Language</td>
-        <td title={`in ${data.languages.join(', ')}`}>{data.languages.map((lan) => flag[lan]).join(', ')}</td>
+        <td title={`in ${language}`}>{flag[language]}</td>
       </tr>
       </tbody>
     </table>
@@ -85,58 +88,6 @@ function LandingPage() {
   const openImpressum = () => setImpressum(true);
   const closeImpressum = () => setImpressum(false);
 
-  // const [allGames, setAllGames] = React.useState([])
-  // const [allTiles, setAllTiles] = React.useState([])
-
-  // const getTiles=()=>{
-  //   fetch('featured_games.json', {
-  //     headers : {
-  //       'Content-Type': 'application/json',
-  //       'Accept': 'application/json'
-  //     }
-  //   }
-  //   ).then(function(response){
-  //     return response.json()
-  //   }).then(function(data) {
-  //     setAllGames(data.featured_games)
-
-  //   })
-  // }
-
-  // React.useEffect(()=>{
-  //   getTiles()
-  // },[])
-
-  // React.useEffect(()=>{
-
-  //   Promise.allSettled(
-  //     allGames.map((gameId) => (
-  //       fetch(`data/g/${gameId}/game.json`).catch(err => {return undefined})))
-  //   ).then(responses =>
-  //     responses.forEach((result) => console.log(result)))
-  //   //   Promise.all(responses.map(res => {
-  //   //     if (res.status == "fulfilled") {
-  //   //       console.log(res.value.json())
-  //   //       return res.value.json()
-  //   //     } else {
-  //   //       return undefined
-  //   //     }
-  //   //   }))
-  //   // ).then(allData => {
-  //   //   setAllTiles(allData.map(data => data?.tile))
-  //   // })
-  // },[allGames])
-
-  // TODO: I would like to read the supported games list form a JSON,
-  // Then load all these games in
-  //
-  let allGames = [
-    "leanprover-community/nng4",
-    "hhu-adam/robo",
-    "djvelleman/stg4",
-    "miguelmarco/STG4",
-  ]
-  let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
 
   return <div className="landing-page">
     <header style={{backgroundImage: `url(${bgImage})`}}>
@@ -153,26 +104,49 @@ function LandingPage() {
       </div>
     </header>
     <div className="game-list">
-      {allTiles.length == 0 ?
-        <p>No Games loaded. Use <a>http://localhost:3000/#/g/local/FOLDER</a> to open a
-          game directly from a local folder.
-        </p>
-        : allGames.map((id, i) => (
-          <Tile
-            key={id}
-            gameId={`g/${id}`}
-            data={allTiles[i]}
-          />
-        ))
-      }
+
+      <GameTile
+        title="Natural Number Game"
+        gameId="g/hhu-adam/NNG4"
+        intro="The classical introduction game for Lean."
+        description="In this game you recreate the natural numbers $\mathbb{N}$ from the Peano axioms,
+learning the basics about theorem proving in Lean.
+
+This is a good first introduction to Lean!"
+        worlds="4"
+        levels="30"
+        language="English"
+        />
+
+      <GameTile
+        title="Formaloversum"
+        gameId="g/hhu-adam/Robo"
+        intro="Erkunde das Leansche Universum mit deinem Robo, welcher dir bei der Verständigung mit den Formalosophen zur Seite steht."
+        description="
+Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet danach verschiedene Bereiche des Bachelorstudiums an.
+
+(Das Spiel befindet sich noch in der Entstehungsphase.)"
+        image={coverRobo}
+        language="German"
+        />
+
+      <GameTile
+        title="NNG (OLD)"
+        gameId="g/hhu-adam/nng4-old"
+        intro="The old version of the NNG copied from lean3."
+        description="This version is not maintained and might break at any point. You should play the new version instead"
+        worlds="9"
+        levels="72"
+        language="English"
+        />
     </div>
     <section>
       <div className="wrapper">
         <h2>Development notes</h2>
         <p>
           As this server runs lean on our university machines, it has a limited capacity.
-          Our current estimate is about 70 simultaneous games.
-          We hope to address and test this limitation better in the future.
+          Our current estimate is about 55 copies of the NNG or 25 copies of games importing
+          mathlib. We hope to address this limitation in the future.
         </p>
         <p>
           Most aspects of the games and the infrastructure are still in development. Feel free to
@@ -186,19 +160,18 @@ function LandingPage() {
         <h2>Adding new games</h2>
         <p>
           If you are considering writing your own game, you should use
-          the <a target="_blank" href="https://github.com/hhu-adam/GameSkeleton">GameSkeleton Github Repo</a> as
-          a template and read <a target="_blank" href="https://github.com/leanprover-community/lean4game/">How to Create a Game</a>.
+          the <a target="_blank" href="https://github.com/hhu-adam/NNG4">NNG Github Repo</a> as
+          a template.
         </p>
         <p>
-          You can directly load your games into the server and play it using
-          the correct URL. The <a target="_blank" href="https://github.com/leanprover-community/lean4game/">instructions above</a> also
-          explain the details for how to load your game to the server.
-
-          We'd like to encourage you to contact us if you have any questions.
+          There is an option to load and run your own games directly on the server,
+          instructions are in the NNG repo. Since this is still in development we'd like to
+          encourage you to contact us for support creating your own game. The documentation is
+          not polished yet.
         </p>
         <p>
-          Featured games on this page are added manually.
-          Please get in contact and we-ll happily add yours.
+          To add games to this main page, you should get in contact as
+          games will need to be added manually.
         </p>
       </div>
     </section>
@@ -216,6 +189,9 @@ function LandingPage() {
       <a className="link" onClick={openImpressum}>Impressum</a>
       {impressum? <PrivacyPolicyPopup handleClose={closeImpressum} />: null}
     </footer>
+
+    {/* <PrivacyPolicy/> */}
+
   </div>
 
 }

client/src/components/level.tsx

@@ -18,10 +18,11 @@ 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,
-  selectHelp, selectDifficulty, selectInventory, selectTypewriterMode, changeTypewriterMode } from '../state/progress'
+  selectHelp, selectDifficulty, selectInventory } from '../state/progress'
 import { store } from '../state/store'
 import { Button } from './button'
 import Markdown from './markdown'
@@ -31,9 +32,8 @@ import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContex
   ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
 import { GameHint } from './infoview/rpc_api'
-import { DeletedHints, Hint, Hints, filterHints } from './hints'
+import { DeletedHints, Hint, Hints } from './hints'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
-import path from 'path';
 
 import '@fontsource/roboto/300.css'
 import '@fontsource/roboto/400.css'
@@ -43,20 +43,12 @@ 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()
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
+  // useLoadWorldFiles(worldId)
 
   const [impressum, setImpressum] = React.useState(false)
 
@@ -146,24 +138,19 @@ function ChatPanel({lastLevel}) {
 
   let introText: Array<string> = level?.data?.introduction.split(/\n(\s*\n)+/)
 
-  // experimental: Remove all hints that appeared identically in the previous step
-  // This effectively prevent consequtive hints being shown.
-  let modifiedHints : GameHint[][] = filterHints(proof)
-
   return <div className="chat-panel">
     <div ref={chatRef} className="chat">
       {introText?.filter(t => t.trim()).map(((t, i) =>
-        // Show the level's intro text as hints, too
         <Hint key={`intro-p-${i}`}
           hint={{text: t, hidden: false}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
       ))}
-      {modifiedHints.map((step, i) => {
+      {proof.map((step, i) => {
         // It the last step has errors, it will have the same hints
         // as the second-to-last step. Therefore we should not display them.
         if (!(i == proof.length - 1 && withErr)) {
           // TODO: Should not use index as key.
           return <Hints key={`hints-${i}`}
-            hints={step} showHidden={showHelp.has(i)} step={i}
+            hints={step.hints} showHidden={showHelp.has(i)} step={i}
             selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.length - 1}/>
         }
       })}
@@ -217,13 +204,10 @@ function PlayableLevel({impressum, setImpressum}) {
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const {mobile} = React.useContext(MobileContext)
 
-  const dispatch = useAppDispatch()
-
+  const difficulty = useSelector(selectDifficulty(gameId))
   const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
   const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
-
-  const typewriterMode = useSelector(selectTypewriterMode(gameId))
-  const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
+  const inventory: Array<String> = useSelector(selectInventory(gameId))
 
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
@@ -237,11 +221,12 @@ function PlayableLevel({impressum, setImpressum}) {
   const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
   // Only for mobile layout
   const [pageNumber, setPageNumber] = useState(0)
-
+  const [typewriterMode, setTypewriterMode] = useState(true)
   // set to true to prevent switching between typewriter and editor
   const [lockInputMode, setLockInputMode] = useState(false)
   const [typewriterInput, setTypewriterInput] = useState("")
   const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
+  const dispatch = useAppDispatch()
 
   // impressum pop-up
   function toggleImpressum() {setImpressum(!impressum)}
@@ -252,8 +237,6 @@ function PlayableLevel({impressum, setImpressum}) {
   const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
   function closeInventoryDoc () {setInventoryDoc(null)}
 
-
-
   const onDidChangeContent = (code) => {
     dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code}))
   }
@@ -269,66 +252,77 @@ function PlayableLevel({impressum, setImpressum}) {
   const {editor, infoProvider, editorConnection} =
     useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection)
 
-  /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside
-   * `TypewriterInterface`.
-   */
-  const handleUndo = () => {
-    const endPos = editor.getModel().getFullModelRange().getEndPosition()
-    let range
-    console.log(endPos.column)
-    if (endPos.column === 1) {
-      range = monaco.Selection.fromPositions(
-        new monaco.Position(endPos.lineNumber - 1, 1),
-        endPos
-      )
-    } else {
-      range = monaco.Selection.fromPositions(
-        new monaco.Position(endPos.lineNumber, 1),
-        endPos
-      )
-    }
-    editor.executeEdits("undo-button", [{
-      range,
-      text: "",
-      forceMoveMarkers: false
-    }]);
-  }
+  // /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside
+  //  * `TypewriterInterface`.
+  //  */
+  // const handleUndo = () => {
+  //   const endPos = editor.getModel().getFullModelRange().getEndPosition()
+  //   let range
+  //   console.log(endPos.column)
+  //   if (endPos.column === 1) {
+  //     range = monaco.Selection.fromPositions(
+  //       new monaco.Position(endPos.lineNumber - 1, 1),
+  //       endPos
+  //     )
+  //   } else {
+  //     range = monaco.Selection.fromPositions(
+  //       new monaco.Position(endPos.lineNumber, 1),
+  //       endPos
+  //     )
+  //   }
+  //   editor.executeEdits("undo-button", [{
+  //     range,
+  //     text: "",
+  //     forceMoveMarkers: false
+  //   }]);
+  // }
 
   // Select and highlight proof steps and corresponding hints
   // TODO: with the new design, there is no difference between the introduction and
   // 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) {
       setTypewriterMode(false)
 
       if (editor) {
-        let code = editor.getModel().getLinesContent()
+        let model = editor.getModel()
+        if (model) {
+          let code = model.getLinesContent()
 
-        // console.log(`insert. code: ${code}`)
-        // console.log(`insert. join: ${code.join('')}`)
-        // console.log(`insert. trim: ${code.join('').trim()}`)
-        // console.log(`insert. length: ${code.join('').trim().length}`)
-        // console.log(`insert. range: ${editor.getModel().getFullModelRange()}`)
+          // console.log(`insert. code: ${code}`)
+          // console.log(`insert. join: ${code.join('')}`)
+          // console.log(`insert. trim: ${code.join('').trim()}`)
+          // console.log(`insert. length: ${code.join('').trim().length}`)
+          // console.log(`insert. range: ${editor.getModel().getFullModelRange()}`)
 
 
-        // TODO: It does seem that the template is always indented by spaces.
-        // This is a hack, assuming there are exactly two.
-        if (!code.join('').trim().length) {
-          console.debug(`inserting template:\n${level.data.template}`)
-          // TODO: This does not work! HERE
-          // Probably overwritten by a query to the server
-          editor.executeEdits("template-writer", [{
-            range: editor.getModel().getFullModelRange(),
-            text: level.data.template + `\n`,
-            forceMoveMarkers: true
-          }])
-        } else {
-          console.debug(`not inserting template.`)
+          // TODO: It does seem that the template is always indented by spaces.
+          // This is a hack, assuming there are exactly two.
+          if (!code.join('').trim().length) {
+            console.debug(`inserting template:\n${level.data.template}`)
+            // TODO: This does not work! HERE
+            // Probably overwritten by a query to the server
+            editor.executeEdits("template-writer", [{
+              range: model.getFullModelRange(),
+              text: level.data.template + `\n`,
+              forceMoveMarkers: true
+            }])
+          } else {
+            console.debug(`not inserting template.`)
+          }
         }
       }
+    } else {
+      setTypewriterMode(true)
     }
   }, [level, levelId, worldId, gameId, editor])
 
@@ -342,17 +336,49 @@ function PlayableLevel({impressum, setImpressum}) {
     setShowHelp(new Set(selectHelp(gameId, worldId, levelId)(store.getState())))
   }, [gameId, worldId, levelId])
 
+  // switching editor mode
   useEffect(() => {
-    if (!typewriterMode && editor) {
-      // Delete last input attempt from command line
-      editor.executeEdits("typewriter", [{
-        range: editor.getSelection(),
-        text: "",
-        forceMoveMarkers: false
-      }]);
-      editor.focus()
+    if (editor) {
+      let model = editor.getModel()
+      if (model) {
+        if (typewriterMode) {
+          // typewriter gets enabled
+          let code = model.getLinesContent().filter(line => line.trim())
+          editor.executeEdits("typewriter", [{
+            range: model.getFullModelRange(),
+            text: code.length ? code.join('\n') + '\n' : '',
+            forceMoveMarkers: true
+          }])
+
+          // let endPos = model.getFullModelRange().getEndPosition()
+          // if (model.getLineContent(endPos.lineNumber).trim() !== "") {
+          //   editor.executeEdits("typewriter", [{
+          //     range: monaco.Selection.fromPositions(endPos, endPos),
+          //     text: "\n",
+          //     forceMoveMarkers: true
+          //   }]);
+          // }
+          // let endPos = model.getFullModelRange().getEndPosition()
+          // let currPos = editor.getPosition()
+          // if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) {
+          //   // This is not a position that would naturally occur from Typewriter, reset:
+          //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
+          // }
+        } else {
+          // typewriter gets disabled
+          // delete last input attempt from command line
+          editor.executeEdits("typewriter", [{
+            range: editor.getSelection(),
+            text: "",
+            forceMoveMarkers: false
+          }]);
+          editor.focus()
+        }
+      }
+
+
     }
-  }, [typewriterMode])
+  }, [editor, typewriterMode])
 
   useEffect(() => {
     // Forget whether hidden hints are displayed for steps that don't exist yet
@@ -370,33 +396,6 @@ function PlayableLevel({impressum, setImpressum}) {
     }
   }, [showHelp])
 
-  // Effect when command line mode gets enabled
-  useEffect(() => {
-    if (onigasmH && editor && typewriterMode) {
-      let code = editor.getModel().getLinesContent().filter(line => line.trim())
-      editor.executeEdits("typewriter", [{
-        range: editor.getModel().getFullModelRange(),
-        text: code.length ? code.join('\n') + '\n' : '',
-        forceMoveMarkers: true
-      }]);
-
-      // let endPos = editor.getModel().getFullModelRange().getEndPosition()
-      // if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
-      //   editor.executeEdits("typewriter", [{
-      //     range: monaco.Selection.fromPositions(endPos, endPos),
-      //     text: "\n",
-      //     forceMoveMarkers: true
-      //   }]);
-      // }
-      // let endPos = editor.getModel().getFullModelRange().getEndPosition()
-      // let currPos = editor.getPosition()
-      // if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) {
-      //   // This is not a position that would naturally occur from Typewriter, reset:
-      //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
-      // }
-    }
-  }, [editor, typewriterMode, onigasmH == null])
-
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
     <DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
@@ -441,7 +440,6 @@ function PlayableLevel({impressum, setImpressum}) {
 function IntroductionPanel({gameInfo}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId} = useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(MobileContext)
 
   let text: Array<string> = gameInfo.data?.worlds.nodes[worldId].introduction.split(/\n(\s*\n)+/)
 
@@ -452,7 +450,7 @@ function IntroductionPanel({gameInfo}) {
           hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
       ))}
     </div>
-    <div className={`button-row${mobile ? ' mobile' : ''}`}>
+    <div className="button-row">
       {gameInfo.data?.worldSize[worldId] == 0 ?
         <Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
         <Button to={`/${gameId}/world/${worldId}/level/1`}>
@@ -474,11 +472,6 @@ function Introduction({impressum, setImpressum}) {
 
   const gameInfo = useGetGameInfoQuery({game: gameId})
 
-  const {worldId} = useContext(WorldLevelIdContext)
-
-  let image: string = gameInfo.data?.worlds.nodes[worldId].image
-
-
   const toggleImpressum = () => {
     setImpressum(!impressum)
   }
@@ -492,71 +485,30 @@ function Introduction({impressum, setImpressum}) {
       :
         <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
           <IntroductionPanel gameInfo={gameInfo} />
-          <div className="world-image-container empty">
-            {image &&
-              // TODO: Temporary for testing
-              <img className={worldId=="Proposition" ? "cover" : "contain"} src={path.join("data", gameId, image)} alt="" />
-            }
-
-          </div>
+          <div className="world-image-container empty"></div>
           <InventoryPanel levelInfo={inventory?.data} />
         </Split>
       }
-
   </>
 }
 
-// {mobile?
-//   // TODO: This is copied from the `Split` component below...
-//   <>
-//     <div className={`app-content level-mobile ${level.isLoading ? 'hidden' : ''}`}>
-//       <ExercisePanel
-//         impressum={impressum}
-//         closeImpressum={closeImpressum}
-//         codeviewRef={codeviewRef}
-//         visible={pageNumber == 0} />
-//       <InventoryPanel levelInfo={level?.data} visible={pageNumber == 1} />
-//     </div>
-//   </>
-// :
-//   <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
-//     <ChatPanel lastLevel={lastLevel}/>
-//     <ExercisePanel
-//       impressum={impressum}
-//       closeImpressum={closeImpressum}
-//       codeviewRef={codeviewRef} />
-//     <InventoryPanel levelInfo={level?.data} />
-//   </Split>
-// }
-
 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)
 
-  const uriStr = `file:///${worldId}/${levelId}`
-  const uri = monaco.Uri.parse(uriStr)
-
-  const inventory: Array<String> = useSelector(selectInventory(gameId))
-  const difficulty: number = useSelector(selectDifficulty(gameId))
-
+  // Create Editor
   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
       },
@@ -568,61 +520,11 @@ 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 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 infoProvider = new InfoProvider(connection.getLeanClient(gameId))
 
     const editorApi = infoProvider.getApi()
 
@@ -667,27 +569,81 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
 
     setEditor(editor)
     setInfoProvider(infoProvider)
+    setInfoviewApi(infoviewApi)
 
-    infoProvider.openPreview(editor, infoviewApi)
-    const taskgutter = new LeanTaskGutter(infoProvider.client, editor)
+    return () => { infoProvider.dispose(); editor.dispose() }
+  }, [])
 
-    // TODO:
-    // setRestart(() => restart)
+  const {leanClient, leanClientStarted} = useLeanClient(gameId)
+  const uriStr = `file:///${worldId}/${levelId}`
+  const uri = monaco.Uri.parse(uriStr)
 
-    return () => {
-      editor.dispose();
-      model.dispose();
-      abbrevRewriter.dispose();
-      taskgutter.dispose();
-      infoProvider.dispose();
-      client.dispose();
+  // Create model when level changes
+  useEffect(() => {
+    if (editor && leanClientStarted) {
+
+      let model = monaco.editor.getModel(uri)
+      if (!model) {
+        model = monaco.editor.createModel(initialCode, 'lean4', uri)
+      }
+      if (model) { // in case of broken pipe, this remains null
+        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(); }
+      }
     }
-  }, [gameId, worldId, levelId])
+  }, [editor, levelId, connection, leanClientStarted])
 
-  const showRestartMessage = () => {
-    // setRestartMessage(true)
-    console.log("TODO: SHOW RESTART MESSAGE")
-  }
+
+  useEffect(() => {
+    if (editor && leanClientStarted) {
+
+      let model = monaco.editor.getModel(uri)
+      if (model) {
+        infoviewApi.serverRestarted(leanClient.initializeResult)
+
+        infoProvider.openPreview(editor, infoviewApi)
+
+        const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
+        const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+
+        return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
+      }
+    }
+  }, [editor, connection, leanClientStarted])
 
   return {editor, infoProvider, editorConnection}
 }
+
+/** Open all files in this world on the server so that they will load faster when accessed */
+function useLoadWorldFiles(worldId) {
+  const gameId = React.useContext(GameIdContext)
+  const gameInfo = useGetGameInfoQuery({game: gameId})
+  const store = useStore()
+
+  useEffect(() => {
+    if (gameInfo.data) {
+      const models = []
+      for (let levelId = 1; levelId <= gameInfo.data.worldSize[worldId]; levelId++) {
+        const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`)
+        let model = monaco.editor.getModel(uri)
+        if (model) {
+          models.push(model)
+        } else {
+          const code = selectCode(gameId, worldId, levelId)(store.getState())
+          models.push(monaco.editor.createModel(code, 'lean4', uri))
+        }
+      }
+      return () => { for (let model of models) { try {model.dispose()} catch {console.log(`failed to dispose model ${model}`)}} }
+    }
+  }, [gameInfo.data, worldId])
+}

client/src/components/popup/preferences.tsx

@@ -1,55 +0,0 @@
-import * as React from 'react'
-import { Input, Typography } from '@mui/material'
-import Markdown from '../markdown'
-import Switch from '@mui/material/Switch';
-import FormControlLabel from '@mui/material/FormControlLabel';
-
-import { IMobileContext } from "../infoview/context"
-
-interface PreferencesPopupProps extends IMobileContext{
-    handleClose: () => void
-} 
-
-export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile, handleClose }: PreferencesPopupProps) {
-    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>Mobile layout</h3>
-                    </div>
-                    <div className='preferences-item'>
-                        <FormControlLabel
-                            control={
-                            <Switch
-                                checked={mobile}
-                                onChange={() => setMobile(!mobile)}
-                                name="checked"
-                                color="primary"
-                            />
-                            }
-                            label="Enable"
-                            labelPlacement="start"
-                        />
-                    </div>
-                    <div className='preferences-item'>
-                        <FormControlLabel
-                            control={
-                            <Switch
-                                checked={!lockMobile}
-                                onChange={() => setLockMobile(!lockMobile)}
-                                name="checked"
-                                color="primary"
-                            />
-                            }
-                            label="Auto"
-                            labelPlacement="start"
-                        />
-                    </div>
-                </div>
-            </Typography>
-        </div>
-    </div>
-}

client/src/components/welcome.tsx

@@ -17,7 +17,6 @@ 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'
@@ -64,7 +63,7 @@ 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, setMobile, lockMobile, setLockMobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(MobileContext)
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
@@ -78,20 +77,15 @@ 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(() => {
@@ -107,7 +101,7 @@ function Welcome() {
   : <>
     <WelcomeAppBar pageNumber={pageNumber} setPageNumber={setPageNumber} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum}
       toggleEraseMenu={toggleEraseMenu} toggleUploadMenu={toggleUploadMenu}
-      toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
+      toggleInfo={toggleInfo} />
     <div className="app-content">
       { mobile ?
           <div className="welcome mobile">
@@ -134,7 +128,6 @@ function Welcome() {
     {eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
     {uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
     {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
-    {preferencesPopup ? <PreferencesPopup mobile={mobile} setMobile={setMobile} lockMobile={lockMobile} setLockMobile={setLockMobile} handleClose={closePreferencesPopup}/> : null}
   </>
 }
 

client/src/components/world_tree.tsx

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

client/src/connection.ts

@@ -0,0 +1,68 @@
+/**
+ *  @fileOverview todo
+ */
+
+import * as React from 'react';
+import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
+import { LeanClient } from 'lean4web/client/src/editor/leanclient';
+
+export class Connection {
+  private game: string = undefined // We only keep a connection to a single game at a time
+  private leanClient: LeanClient = null
+
+  getLeanClient(game): LeanClient {
+    if (this.game !== game) {
+      if (this.leanClient) {
+        this.leanClient.stop() // Stop previous Lean client
+      }
+      this.game = game
+      // Start a new Lean client for the new `gameId`.
+      const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + game
+      const uri = monaco.Uri.parse('file:///')
+      this.leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
+    }
+
+    return this.leanClient
+  }
+
+  /** If not already started, starts the Lean client. resolves the returned promise as soon as a
+   * Lean client is running.
+   */
+  startLeanClient = (game) => {
+    return new Promise<LeanClient>((resolve) => {
+      const leanClient = this.getLeanClient(game)
+      if (leanClient.isRunning()) {
+        resolve(leanClient)
+      } else {
+        if (!leanClient.isStarted()) {
+          leanClient.start()
+        }
+        leanClient.restarted(() => {
+          // This keep alive message is not recognized by the server,
+          // but it makes sure that the websocket connection does not
+          // time out after 60 seconds.
+          setInterval(() => {leanClient.sendNotification('$/keepAlive', {}) }, 5000)
+          resolve(leanClient)
+        })
+      }
+    })
+  }
+}
+
+export const connection = new Connection()
+
+export const ConnectionContext = React.createContext(null);
+
+export const useLeanClient = (gameId) => {
+  const leanClient = connection.getLeanClient(gameId)
+  const [leanClientStarted, setLeanClientStarted] = React.useState(leanClient.isStarted())
+
+  React.useEffect(() => {
+    const t1 = leanClient.restarted(() => { console.log("START"); setLeanClientStarted(true) })
+    const t2 = leanClient.stopped(() => { console.log("STOP"); setLeanClientStarted(false) })
+
+    return () => {t1.dispose(); t2.dispose()}
+  }, [leanClient, setLeanClientStarted])
+
+  return {leanClientStarted, leanClient}
+}

client/src/css/app.css

@@ -42,6 +42,12 @@ body {
   border-radius: .3em;
 }
 
+
+/* Hide monaco editor notifications */
+.monaco-workbench > .notifications-toasts.visible {
+  display: none !important;
+}
+
 .loading {
   margin: auto;
   height: 100%;
@@ -105,18 +111,11 @@ 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;

client/src/css/inventory.css

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

client/src/css/landing_page.css

@@ -48,7 +48,6 @@ a {
   border: 1px solid rgb(140, 140, 140);
   border-radius: 20px;
   box-shadow: 5px 5px 8px rgb(140, 140, 140);
-  width: 100%;
   max-width: 500px;
   display: flex;
   flex-direction: column;

client/src/css/level.css

@@ -232,20 +232,6 @@ 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;
@@ -331,6 +317,11 @@ td code  {
   margin-right: 0;
 }
 
+#home-btn {
+  margin-right: .5em;
+  margin-left: 0;
+}
+
 .menu.dropdown .svg-inline--fa {
   width: 1.8rem;
 }
@@ -345,21 +336,6 @@ td code  {
   background-color: #eee;
 }
 
-.world-image-container {
-  display: flex;
-  flex-direction: column;
-  justify-content: center;
-}
-
-.world-image-container img.contain {
-  object-fit: contain;
-}
-
-.world-image-container img.cover {
-  height: 100%;
-  object-fit: cover;
-}
-
 .typewriter-interface .proof {
   background-color: #fff;
 }

client/src/css/world_tree.css

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

client/src/hooks.ts

@@ -1,30 +1,6 @@
 import { TypedUseSelectorHook, useDispatch, useSelector } from 'react-redux'
 import type { RootState, AppDispatch } from './state/store'
 
-import { setMobile as setMobileState, setLockMobile as setLockMobileState} from "./state/preferences"
-
 // Use throughout your app instead of plain `useDispatch` and `useSelector`
 export const useAppDispatch: () => AppDispatch = useDispatch
 export const useAppSelector: TypedUseSelectorHook<RootState> = useSelector
-
-export const useMobile = () => {
-  const dispatch = useAppDispatch();
-
-  const mobile = useAppSelector((state) => state.preferences.mobile);
-  const lockMobile = useAppSelector((state) => state.preferences.lockMobile);
-
-  const setMobile = (val: boolean) => {
-    dispatch(setMobileState(val));
-  };
-
-  const setLockMobile = (val: boolean) => {
-    dispatch(setLockMobileState(val));
-  };
-
-  return {
-    mobile,
-    setMobile,
-    lockMobile,
-    setLockMobile,
-  };
-};

client/src/index.tsx

@@ -1,39 +1,31 @@
-import * as React from 'react'
-import { createRoot } from 'react-dom/client'
-import App from './app'
-import { store } from './state/store'
-import { Provider } from 'react-redux'
-import type { RouteObject } from "react-router"
-import { createHashRouter, RouterProvider, Route, redirect } from "react-router-dom"
-import ErrorPage from './components/error_page'
-import Welcome from './components/welcome'
-import LandingPage from './components/landing_page'
-import Level from './components/level'
+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 {
+  createHashRouter,
+  RouterProvider,
+  Route,
+} from "react-router-dom";
+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';
+import { redirect } from 'react-router-dom';
 
-
-
-// If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
-// `/g/local/game`. This is used for the devcontainer setup
-let single_game = (import.meta.env.VITE_LEAN4GAME_SINGLE == "true")
-let root_object: RouteObject = single_game ? {
-  path: "/",
-  loader: () => redirect("/g/local/game")
-} : {
-  path: "/",
-  element: <LandingPage />,
-}
+monacoSetup()
 
 const router = createHashRouter([
-  root_object,
   {
-    // For backwards compatibility
-    path: "/game/nng",
-    loader: () => redirect("/g/hhu-adam/NNG4")
+    path: "/",
+    element: <LandingPage />,
   },
   {
-    // For backwards compatibility
-    path: "/g/hhu-adam/NNG4",
-    loader: () => redirect("/g/leanprover-community/NNG4")
+    path: "/game/nng",
+    loader: () => redirect("/g/hhu-adam/NNG4")
   },
   {
     path: "/g/:owner/:repo",
@@ -57,7 +49,9 @@ const root = createRoot(container!);
 root.render(
   <React.StrictMode>
     <Provider store={store}>
-      <RouterProvider router={router} />
+      <ConnectionContext.Provider value={connection}>
+        <RouterProvider router={router} />
+      </ConnectionContext.Provider>
     </Provider>
   </React.StrictMode>
 );

client/src/index_local.tsx

@@ -0,0 +1,55 @@
+// This file is a copy of `index.tsx` where the path "/" is redirected to "/g/local/game".
+// It is used for the dev. setup where there is only one game in a folder called `game`.
+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 {
+  createHashRouter,
+  RouterProvider,
+  Route,
+} from "react-router-dom";
+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';
+import { redirect } from 'react-router-dom';
+
+monacoSetup()
+
+const router = createHashRouter([
+  {
+    path: "/",
+    loader: () => redirect("/g/local/game")
+  },
+  {
+    path: "/g/:owner/:repo",
+    element: <App />,
+    errorElement: <ErrorPage />,
+    children: [
+      {
+        path: "/g/:owner/:repo",
+        element: <Welcome />,
+      },
+      {
+        path: "/g/:owner/:repo/world/:worldId/level/:levelId",
+        element: <Level />,
+      },
+    ],
+  },
+]);
+
+const container = document.getElementById('root');
+const root = createRoot(container!);
+root.render(
+  <React.StrictMode>
+    <Provider store={store}>
+      <ConnectionContext.Provider value={connection}>
+        <RouterProvider router={router} />
+      </ConnectionContext.Provider>
+    </Provider>
+  </React.StrictMode>
+);

client/src/state/api.ts

@@ -2,29 +2,16 @@
  * @fileOverview Define API of the server-client communication
 */
 import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react'
-
-
-export interface GameTile {
-  title: string
-  short: string
-  long: string
-  languages: Array<string>
-  prerequisites: Array<string>
-  worlds: number
-  levels: number
-  image: string
-}
+import { Connection } from '../connection'
 
 export interface GameInfo {
   title: null|string,
   introduction: null|string,
   info: null|string,
-  worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string, image: string}}, edges: string[][]},
+  worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string}}, edges: string[][]},
   worldSize: null|{[key: string]: number},
   authors: null|string[],
   conclusion: null|string,
-  tile: null|GameTile,
-  image: null|string
 }
 
 export interface InventoryTile {
@@ -35,7 +22,6 @@ export interface InventoryTile {
   locked: boolean,
   new: boolean,
   hidden: boolean
-  altTitle: string,
 }
 
 export interface LevelInfo {
@@ -51,8 +37,7 @@ export interface LevelInfo {
   lemmaTab: null|string,
   statementName: null|string,
   displayName: null|string,
-  template: null|string,
-  image: null|string
+  template: null|string
 }
 
 /** Used to display the inventory on the welcome page */
@@ -72,22 +57,40 @@ interface Doc {
   category: string,
 }
 
+
+const customBaseQuery = async (
+  args : {game: string, method: string, params?: any},
+  { signal, dispatch, getState, extra },
+  extraOptions
+) => {
+  try {
+    const connection : Connection = extra.connection
+    let leanClient = await connection.startLeanClient(args.game)
+    console.log(`Sending request ${args.method}`)
+    let res = await leanClient.sendRequest(args.method, args.params)
+    console.log('Received response') //, res)
+    return {'data': res}
+   } catch (e) {
+    return {'error': e}
+   }
+}
+
 // Define a service using a base URL and expected endpoints
 export const apiSlice = createApi({
   reducerPath: 'gameApi',
-  baseQuery: fetchBaseQuery({ baseUrl: window.location.origin + "/data" }),
+  baseQuery: customBaseQuery,
   endpoints: (builder) => ({
     getGameInfo: builder.query<GameInfo, {game: string}>({
-      query: ({game}) => `${game}/game.json`,
+      query: ({game}) => {return {game, method: 'info', params: {}}},
     }),
     loadLevel: builder.query<LevelInfo, {game: string, world: string, level: number}>({
-      query: ({game, world, level}) => `${game}/level__${world}__${level}.json`,
+      query: ({game, world, level}) => {return {game, method: "loadLevel", params: {world, level}}},
     }),
     loadInventoryOverview: builder.query<InventoryOverview, {game: string}>({
-      query: ({game}) => `${game}/inventory.json`,
+      query: ({game}) => {return {game, method: "loadInventoryOverview", params: {}}},
     }),
     loadDoc: builder.query<Doc, {game: string, name: string, type: "lemma"|"tactic"}>({
-      query: ({game, type, name}) => `${game}/doc__${type}__${name}.json`,
+      query: ({game, name, type}) => {return {game, method: "loadDoc", params: {name, type}}},
     }),
   }),
 })

client/src/state/local_storage.ts

@@ -36,24 +36,3 @@ 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
-  }
-}

client/src/state/preferences.ts

@@ -1,37 +0,0 @@
-import { createSlice } from "@reduxjs/toolkit";
-
-import { loadPreferences } from "./local_storage";
-
-interface PreferencesState {
-  mobile: boolean;
-  lockMobile: boolean;
-}
-
-export function getWindowDimensions() {
-  const {innerWidth: width, innerHeight: height } = window
-  return {width, height}
-}
-
-const { width } = getWindowDimensions()
-
-export const AUTO_SWITCH_THRESHOLD = 800
-
-const initialState: PreferencesState = loadPreferences() ?? {
-    mobile: width < AUTO_SWITCH_THRESHOLD,
-    lockMobile: false
-}
-
-export const preferencesSlice = createSlice({
-  name: "preferences",
-  initialState,
-  reducers: {
-    setMobile: (state, action) => {
-      state.mobile = action.payload;
-    },
-    setLockMobile: (state, action) => {
-      state.lockMobile = action.payload;
-    },
-  },
-});
-
-export const { setMobile, setLockMobile } = preferencesSlice.actions;

client/src/state/progress.ts

@@ -26,8 +26,7 @@ export interface GameProgressState {
   inventory: string[],
   difficulty: number,
   openedIntro: boolean,
-  data: WorldProgressState,
-  typewriterMode?: boolean
+  data: WorldProgressState
 }
 
 /**
@@ -127,11 +126,6 @@ export const progressSlice = createSlice({
       addGameProgress(state, action)
       state.games[action.payload.game].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
-    }
   }
 })
 
@@ -202,14 +196,7 @@ export function selectOpenedIntro(game: string) {
   }
 }
 
-/** return typewriter mode for the current game if it exists */
-export function selectTypewriterMode(game: string) {
-  return (state) => {
-    return state.progress.games[game]?.typewriterMode ?? true
-  }
-}
-
 /** Export actions to modify the progress */
 export const { changedSelection, codeEdited, levelCompleted, deleteProgress,
   deleteLevelProgress, loadProgress, helpEdited, changedInventory, changedOpenedIntro,
-  changedDifficulty, changeTypewriterMode} = progressSlice.actions
+  changedDifficulty } = progressSlice.actions

client/src/state/store.ts

@@ -7,19 +7,21 @@ import { debounce } from "debounce";
 import { connection } from '../connection'
 import { apiSlice } from './api'
 import { progressSlice } from './progress'
-import { preferencesSlice } from "./preferences"
-import { saveState, savePreferences } from "./local_storage";
+import { saveState } 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().concat(apiSlice.middleware),
+    getDefaultMiddleware({
+      thunk: {
+        extraArgument: { connection }
+      }
+    }).concat(apiSlice.middleware),
 });
 
 /**
@@ -29,7 +31,6 @@ export const store = configureStore({
 store.subscribe(
   debounce(() => {
     saveState(store.getState()[progressSlice.name]);
-    savePreferences(store.getState()[preferencesSlice.name]);
   }, 800)
 );
 

client/src/window_width.tsx

@@ -0,0 +1,21 @@
+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
+}

doc/DOCUMENTATION.md

@@ -1,8 +1,6 @@
-**NOTE! This document is deprecated! The current documentation is [How To Create A Game](create_game.md)**
-
 # Creating a game.
 
-Ideally one takes the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new game.
+Ideally one takes the [NNG template](https://github.com/hhu-adam/NNG4) to create a new game.
 
 ## Game Structure
 
@@ -297,9 +295,8 @@ 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`:
+code at the beginning of `lean4game/server/index.mjs`:
 ```typescript
 const games = {
     "g/hhu-adam/robo": {

doc/create_game.md

@@ -4,7 +4,7 @@ This tutorial walks you through creating a new game for lean4. It covers from wr
 
 ## 1. Create the project
 
-1. Use the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
+1. Use the [NNG template](https://github.com/hhu-adam/NNG4) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
 2. Clone the game repo.
 3. Call `lake update && lake exe cache get && lake build` to build the Lean project.
 
@@ -223,40 +223,25 @@ One thing to keep in mind is that the game will look at the main proof to figure
 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.
+placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands. If you specify
 
-Read [More about Hints](doc/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.
-
-The images need to be placed in `images/` and you need to add a command like `Image "images/path/to/myWorldImage.png"` 
-in one of the files you created in 2), 3), or 4) (i.e. game/world/level).
-
-NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world.
-
-## 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).
-
-## 8. Publish your game
-
-To publish your game on the official server, see [Publishing a game](doc/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:
-
-```lean
-Languages "English"
-CaptionShort "Game Template"
-CaptionLong "You should use this game as a template for your own game and add your own levels."
-Prerequisites "NNG"
-CoverImage "images/cover.png"
 ```
-* `Languages`: Currently only a single language (capital English name). The tile will show a corresponding flag.
-* `CaptionShort`: One catch phrase. Appears above the image.
-* `CaptionLong`: 2-4 sentences to describe the game.
-* `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text.
-* `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens.
+Hint (strict := true) "some hidden hint"
+```
+
+a hint only matches iff the assumptions match exactly one-to-one. (Otherwise, it does not care if there are additional assumptions in context)
+
+Further, you can choose to hide hints and only have them displayed when the player presses "More Help":
+```
+Hint (hidden := true) "some hidden hint"
+```
+
+Lastly, you should put variable names in hints inside brackets:
+
+```
+Hint "now use `rw [{h}]` to use your assumption {h}."
+```
+That way, the game will replace it with the actual name the assumption has in the player's proof state.
 
 ## Further Notes
 

doc/hints.md

@@ -1,87 +0,0 @@
-# Hints
-
-Most important for game development are probably the "Hints". You can add Hints at any place in your proof using the `Hint` tactic
-
-```
-Statement .... := by
-  Hint "Hint to show at the start"
-  rw [h]
-  Hint "some tip after using rw"
-  ...
-```
-
-## 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
-sample solutions and the entire context from the sample solutions is present in the
-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
-all of them.
-
-However, identical (non-hidden) hints which where already present in the step
-before are omitted. This is to allow a player to add new assumptions to context, for example
-with `have`, without seeing the same hint over and over again.
-Hidden hints are not filtered.
-
-## 2. Alternative Proofs / `Branch`
-
-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
-so that no progress has been made on proofing the goal.
-
-```
-Statement .... := by
-  Hint "Huse `rw` or `rewrite`."
-  Branch
-    rewrite [h]
-    Hint "now you still need `rfl`"
-  rw [h]
-```
-
-## 3. Variables names
-
-Put variables in the hint text inside brackets like this: `{h}`! This way the server can replace
-the variable's name with the one the user actually used.
-
-For example, if the sample proof contains
-
-```
-have h : True := trivial
-Hint "Now use `rw [{h}]` to use your assumption `{h}`."
-```
-
-but the player writes `have g : True := trivial`, they will see a hint saying
-"Now use `rw [g]` to use your assumption `g`."
-
-## 4. Hidden hints
-
-Some hints can be hidden, and only show after the user clicks on a button to get additional
-help. You mark a hint as hidden with `(hidden := true)`:
-
-```
-Hint (hidden := true) "some hidden hint"
-```
-
-## 5. Strict context matching
-
-If you use the attribute `(strict := true)` a hint is only shown if the entire context
-matches exactly the one where the hint is placed. With `(hint := false)`, which is the default,
-it does not matter if additional assumptions are present in the player's context.
-
-```
-Hint (strict := true) "now use `have` to create a new assumption."
-```
-
-You should probably use `(strict := true)` if you want to give fine-grained details about
-tactics like `have` which do not modify the goal or any existing assumptions, but only
-create new assumptions.
-
-## 6. Formatting
-
-You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$`
-
-TODO: Write a doc about latex/markdown options available.

doc/publish_game.md

@@ -1,32 +0,0 @@
-# Publishing games
-
-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
-
-First, you need your game in a public Github repository and make sure the github action has run.
-You can check this by spotting the green checkmark on the start page, or by looking at the "Actions"
-tab.
-
-## 2. Import the game
-
-You call the URL that's listed under "What's Next?" in the latest action run. Explicitely you call
-the URL of the form
-
-> adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY}
-
-where `{USER}` and `{REPOSITORY}` are replaced with the github user and repository name.
-
-You should see a white screen which shows import updates and eventually reports "Done."
-
-## 3. Play the game
-
-Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITORY}`!
-
-## 4. Main page
-
-Adding games to the main page happens manually by the server maintainers. Tell us if you want us
-to add a tile for your game!
-
-For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).

doc/running_locally.md

@@ -4,15 +4,13 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
 
 There are several options to play a game locally:
 
-1. VSCode Dev Container: needs `docker` installed on your machine
-2. Codespaces: Needs active internet connection and computing time is limited.
-3. Gitpod: does not work yet (Is that true?)
-4. Manual installation: Needs `npm` installed on your system
+- VSCode Dev Container: needs `docker` installed on your machine
+- Codespaces: Needs active internet connection and computing time is limited.
+- Gitpod: does not work yet (I that true?)
+- Manual installation: Needs `npm` installed on your system
 
 The recommended option is "VSCode Dev containers" but you may choose any option above depending on your setup.
 
-The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) contains all the relevant files to make your local setup (dev container / gitpod / codespaces) work. You might need to update these files manually by copying them from there if you need any new improvements to the dev setup you're using in an existing game.
-
 ## VSCode Dev Containers
 
 1.  **Install Docker and Dev Containers** *(once)*:<br/>
@@ -29,9 +27,9 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta
     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-15 minutes. After the first
+    * The first start will take a while, ca. 2-10 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.
@@ -44,13 +42,12 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta
   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".
 
-Note: You have to wait until npm started properly, which might take a good while.
+Note: You have to wait until npm started properly. In particular, this is after a message like `[client] webpack 5.81.0 compiled successfully in 38119 ms` appears in the terminal, which might take a good while.
 
 As with devcontainers, you need to run `lake build` after changing any lean files and then reload the browser.
 
@@ -76,26 +73,27 @@ Now install node:
 nvm install node
 ```
 
-Clone the game (e.g. `GameSkeleton` here):
+Clone the game (e.g. `NNG4` here):
 ```bash
-git clone https://github.com/hhu-adam/GameSkeleton.git
-# or: git clone git@github.com:hhu-adam/GameSkeleton.git
+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 GameSkeleton
-lake update -R
+cd NNG4
+lake update
+lake exe cache get   # if your game depends on mathlib
 lake build
 ```
 
-Clone the server repository into a directory next to the game:
+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 `GameSkeleton` and `lean4game` must be in the same directory!
+The folders `NNG4` and `lean4game` must be in the same directory!
 
 In `lean4game`, install dependencies:
 ```bash
@@ -108,16 +106,16 @@ Run the game:
 npm start
 ```
 
-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.
+This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/NNG4. Replace `NNG4` with the folder name of your local game.
 
 ## Modifying the GameServer
 
-When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by using `lake update -R -Klean4game.local`:
+When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by setting `export NODE_ENV=development` inside your local game before building it:
 
 ```bash
 cd NNG4
-lake update -R -Klean4game.local
+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. Therefore, you can the local copy of the edit `GameServer` in `../lean4game` and
-`lake build` will then directly use this modified copy to build your game.
+This causes lake to search locally for the `GameServer` lake package instead of using the version from github. Therefore, when you `lake build` your game, it will rebuild with the modified `GameServer`.

doc/server.md

@@ -1,28 +0,0 @@
-
-# Notes for Server maintainer
-
-In order to set up the server to allow imports, one needs to create a
-[Github Access token](https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens). A fine-grained access token with only reading rights for public
-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
-you're using `pm2`
-
-Then people can call:
-
-> https://{website}/import/trigger/{owner}/{repo}
-
-where you replace:
-- website: The website your server runs on, e.g. `localhost:3000`
-- owner, repo: The owner and repository name of the game you want to load from github.
-
- will trigger to download the latest version of your game from github onto your server.
- Once this import reports "Done", you should be able to play your game under:
-
-> https://{website}/#/g/{owner}/{repo}
-
-## data management
-Everything downloaded remains in the folder `lean4game/games`.
-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.

doc/update_game.md

@@ -1,52 +0,0 @@
-# How to update your Game
-
-## New Lean version
-
-You can update the game to any Lean version by simply editing the `lean-toolchain` in your game repo to contain the
-new lean version `leanprover/lean4:v4.X.0`.
-
-Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https://github.com/leanprover-community/lean4game/tags).
-
-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:
-  ```
-  lake update -R
-  lake build
-  ```
-
-  * Additionally, if you have a local copy of the server `lean4game`,
-    you should update this one to the matching version. Run the following in the folder `lean4game/`:
-    ```
-    git fetch
-    git checkout {VERSION_TAG}
-    npm install
-    ```
-    where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
-* Gitpod/Codespaces: Create a fresh one
-
-This will update your game (and the mathlib version you might be using) to the new lean version.
-
-## Newest developing setup
-
-There are a few files in your game repository which are used for the developing setup
-(dev container/codespaces/gitpod). If you need to update your developing setup, for example because it doesn't work
-anymore, you will need to copy the relevant files from the [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) template into your game repo.
-
-The relevant files are:
-
-```
-.devcontainer/
-.docker/
-.github/
-.gitpod/
-.vscode/
-lakefile.lean
-```
-
-simply copy them from the `GameSkeleton` into your game and proceed as above,
-i.e. `lake update -R && lake build`.
-
-(Note: You should not need to modify any of these files, with the exception of the `lakefile.lean`,
-where you need to add any dependencies of your game, or remove mathlib if you don't need it.)

ecosystem.config.js

@@ -2,12 +2,10 @@
 module.exports = {
   apps : [{
     name   : "lean4game",
-    script : "relay/index.mjs",
+    script : "server/index.mjs",
     env: {
-      LEAN4GAME_GITHUB_USER: "",
-      LEAN4GAME_GITHUB_TOKEN: "",
-      NODE_ENV: "production",
-      PORT: 8002
+       NODE_ENV: "production",
+       PORT: 8002
     },
   }]
 }

env.d.ts

@@ -1,10 +0,0 @@
-/// <reference types="vite/client" />
-
-interface ImportMetaEnv {
-  readonly VITE_LEAN4GAME_SINGLE: string
-  // more env variables...
-}
-
-interface ImportMeta {
-  readonly env: ImportMetaEnv
-}

package.json

@@ -1,7 +1,6 @@
 {
   "name": "lean4-game",
   "version": "0.1.0",
-  "type": "module",
   "private": true,
   "homepage": ".",
   "dependencies": {
@@ -10,17 +9,12 @@
     "@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",
     "@reduxjs/toolkit": "^1.9.1",
     "@types/cytoscape": "^3.19.9",
     "@types/react-router-dom": "^5.3.3",
-    "@vitejs/plugin-react-swc": "^3.4.0",
     "cross-env": "^7.0.3",
     "cytoscape": "^3.23.0",
     "cytoscape-elk": "^2.1.0",
@@ -28,7 +22,7 @@
     "debounce": "^1.2.1",
     "express": "^4.18.2",
     "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-    "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
+    "lean4web": "github:hhu-adam/lean4web",
     "octokit": "^2.0.14",
     "path-browserify": "^1.0.1",
     "react": "^18.2.0",
@@ -41,39 +35,45 @@
     "rehype-katex": "^6.0.2",
     "remark-gfm": "^3.0.1",
     "remark-math": "^5.1.1",
-    "request": "^2.88.2",
     "request-progress": "^3.0.0",
-    "vite": "^4.5.0",
-    "vite-plugin-static-copy": "^0.17.0",
-    "vite-plugin-svgr": "^4.1.0",
     "vscode-ws-jsonrpc": "^2.0.1",
     "web-worker": "^1.2.0",
     "ws": "^8.11.0"
   },
   "devDependencies": {
+    "@babel/cli": "^7.19.3",
+    "@babel/core": "^7.20.5",
+    "@babel/preset-env": "^7.20.2",
+    "@babel/preset-react": "^7.18.6",
+    "@babel/preset-typescript": "^7.18.6",
     "@pmmmwh/react-refresh-webpack-plugin": "^0.5.10",
     "@redux-devtools/core": "^3.13.1",
     "@testing-library/react": "^13.4.0",
     "@types/debounce": "^1.2.1",
+    "babel-loader": "^8.3.0",
     "concurrently": "^7.6.0",
     "css-loader": "^6.7.3",
     "file-loader": "^6.2.0",
-    "nodemon": "^3.0.1",
+    "nodemon": "^2.0.20",
     "react-refresh": "^0.14.0",
     "style-loader": "^3.3.1",
     "ts-loader": "^9.4.2",
     "typescript": "^4.9.4",
-    "url-loader": "^4.1.1"
+    "url-loader": "^4.1.1",
+    "webpack": "^5.75.0",
+    "webpack-cli": "^4.10.0",
+    "webpack-dev-server": "^4.11.1",
+    "webpack-shell-plugin-next": "^2.3.1"
   },
   "scripts": {
     "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
-    "start_server": "(cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\")",
-    "start_client": "cross-env NODE_ENV=development vite --host",
-    "build": "npm run build_server && npm run build_client",
-    "preview": "vite preview",
-    "build_server": "cd server && lake build",
-    "build_client": "cross-env NODE_ENV=production vite build",
-    "production": "cross-env NODE_ENV=production node relay/index.mjs"
+    "start_server": "cd server && lake build && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"",
+    "start_client": "cross-env NODE_ENV=development webpack-dev-server --hot",
+    "build": "cross-env NODE_ENV=production webpack",
+    "production": "cross-env NODE_ENV=production node server/index.mjs",
+    "build_robo": "rm -rf ./Robo && git clone https://github.com/hhu-adam/Robo && docker build ./Robo --file ./Robo/Dockerfile --tag g/hhu-adam/robo && rm -rf ./Robo",
+    "build_nng": "rm -rf ./NNG4 && git clone https://github.com/hhu-adam/NNG4 && docker build ./NNG4 --file ./NNG4/Dockerfile --tag g/hhu-adam/nng4 && rm -rf ./NNG4",
+    "update_lean": "./UPDATE_LEAN.sh"
   },
   "eslintConfig": {
     "extends": [

relay/unpack.sh

@@ -1,30 +0,0 @@
-#/bin/bash
-
-ARTIFACT_ID=$1
-OWNER=$2
-REPO=$3
-
-# mkdir -p games
-cd games
-
-# mkdir -p tmp
-mkdir -p ${OWNER}
-
-echo "Unpacking ZIP."
-unzip -o tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip -d tmp/${OWNER}_${REPO}_${ARTIFACT_ID}
-echo "Unpacking game."
-
-# exit the npm project to avoid reloading. TODO: Where should we actually save these?
-
-
-
-echo "Delete old version of the game"
-rm -rf ${OWNER}/${REPO}
-mkdir -p ${OWNER}/${REPO}
-
-for f in tmp/${OWNER}_${REPO}_${ARTIFACT_ID}/* #Should only be one file
-do
-  echo "Unpacking $f"
-  #tar -xvzf $f -C games/${OWNER}/${REPO}
-  unzip -q -o $f -d ${OWNER}/${REPO}
-done

server/.gitignore

@@ -0,0 +1,3 @@
+build
+adam
+nng

server/GameServer.lean

@@ -1,17 +0,0 @@
-import GameServer.FileWorker
-import GameServer.Commands
-
--- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`
--- should we have a different solution?
-
-unsafe def main : List String → IO UInt32 := fun args => do
-  let e ← IO.getStderr
-
-  Lean.enableInitializersExecution
-
-  -- TODO: remove this argument
-  if args[0]? == some "--server" then
-    MyServer.FileWorker.workerMain {} args
-  else
-    e.putStrLn s!"Expected `--server`"
-    return 1

server/GameServer/Commands.lean

@@ -1,12 +1,23 @@
-import GameServer.Helpers
-import GameServer.Inventory
-import GameServer.Options
-import GameServer.SaveData
+import GameServer.EnvExtensions
 
 open Lean Meta Elab Command
 
 set_option autoImplicit false
 
+/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
+register_option lean4game.showDependencyReasons : Bool := {
+  defValue := false
+  descr := "show reasons for calculated world dependencies."
+}
+
+/-- Let `MakeGame` print the reasons why the worlds depend on each other.
+
+Note: currently unused in favour of setting `set_option trace.debug true`. -/
+register_option lean4game.verbose : Bool := {
+  defValue := false
+  descr := "display more info messages to help developing the game."
+}
+
 /-! # Game metadata -/
 
 /-- Switch to the specified `Game` (and create it if non-existent). Example: `Game "NNG"` -/
@@ -35,101 +46,147 @@ elab "Title" t:str : command => do
   match ← getCurLayer with
   | .Level => modifyCurLevel fun level => pure {level with title := t.getString}
   | .World => modifyCurWorld  fun world => pure {world with title := t.getString}
-  | .Game => modifyCurGame  fun game => pure {game with
-      title := t.getString
-      tile := {game.tile with title := t.getString}}
+  | .Game => modifyCurGame  fun game => pure {game with title := t.getString}
 
 /-- Define the introduction of the current game/world/level. -/
 elab "Introduction" t:str : command => do
-  let intro := t.getString
   match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with introduction := intro}
-  | .World => modifyCurWorld  fun world => pure {world with introduction := intro}
-  | .Game => modifyCurGame  fun game => pure {game with introduction := intro}
+  | .Level => modifyCurLevel fun level => pure {level with introduction := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with introduction := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}
 
 /-- Define the info of the current game. Used for e.g. credits -/
 elab "Info" t:str : command => do
-  let info:= t.getString
   match ← getCurLayer with
-  | .Level =>
-    logError "Can't use `Info` in a level!"
-    pure ()
-  | .World =>
-    logError "Can't use `Info` in a world"
-    pure ()
-  | .Game => modifyCurGame  fun game => pure {game with info := info}
+  | .Level => pure ()
+  | .World => pure ()
+  | .Game => modifyCurGame  fun game => pure {game with info := t.getString}
 
-/-- Provide the location of the image for the current game/world/level.
-Paths are relative to the lean project's root. -/
-elab "Image" t:str : command => do
-  let file := t.getString
-  if not <| ← System.FilePath.pathExists file then
-    logWarningAt t s!"Make sure the cover image '{file}' exists."
-  if not <| file.startsWith "images/" then
-    logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."
-
-  match ← getCurLayer with
-  | .Level =>
-    logWarning "Level-images not implemented yet" -- TODO
-    modifyCurLevel fun level => pure {level with image := file}
-  | .World =>
-    modifyCurWorld  fun world => pure {world with image := file}
-  | .Game =>
-    logWarning "Main image of the game not implemented yet" -- TODO
-    modifyCurGame  fun game => pure {game with image := file}
 
 /-- Define the conclusion of the current game or current level if some
 building a level. -/
 elab "Conclusion" t:str : command => do
-  let conclusion := t.getString
   match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion}
-  | .World => modifyCurWorld  fun world => pure {world with conclusion := conclusion}
-  | .Game => modifyCurGame  fun game => pure {game with conclusion := conclusion}
+  | .Level => modifyCurLevel fun level => pure {level with conclusion := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with conclusion := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with conclusion := t.getString}
 
-/-- A list of games that should be played before this one. Example `Prerequisites "NNG" "STG"`. -/
-elab "Prerequisites" t:str* : command => do
-  modifyCurGame fun game => pure {game with
-    tile := {game.tile with prerequisites := t.map (·.getString) |>.toList}}
-
-/-- Short caption for the game (1 sentence) -/
-elab "CaptionShort" t:str : command => do
-  let caption := t.getString
-  modifyCurGame fun game => pure {game with
-    tile := {game.tile with short := caption}}
-
-/-- More detailed description what the game is about (2-4 sentences). -/
-elab "CaptionLong" t:str : command => do
-  let caption := t.getString
-  modifyCurGame fun game => pure {game with
-    tile := {game.tile with long := caption}}
-
-/-- A list of Languages the game is translated to. For example `Languages "German" "English"`.
-NOTE: For the time being, only a single language is supported.
- -/
-elab "Languages" t:str* : command => do
-  modifyCurGame fun game => pure {game with
-    tile := {game.tile with languages := t.map (·.getString) |>.toList}}
-
-/-- The Image of the game (optional). TODO: Not impementeds -/
-elab "CoverImage" t:str : command => do
-  let file := t.getString
-  if not <| ← System.FilePath.pathExists file then
-    logWarningAt t s!"Make sure the cover image '{file}' exists."
-  if not <| file.startsWith "images/" then
-    logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."
-
-  modifyCurGame fun game => pure {game with
-    tile := {game.tile with image := file}}
 
 /-! # Inventory
 
-The inventory contains docs for tactics, theorems, and definitions. These are all locked
+The inventory contains docs for tactics, lemmas, and definitions. These are all locked
 in the first level and get enabled during the game.
 -/
 
 /-! ## Doc entries -/
 
+/-- Copied from `Mathlib.Tactic.HelpCmd`.
+
+Gets the initial string token in a parser description. For example, for a declaration like
+`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations
+that don't start with a string constant. -/
+partial def getHeadTk (e : Expr) : Option String :=
+  match (Expr.withApp e λ e a => (e.constName?.getD Name.anonymous, a)) with
+  | (``ParserDescr.node, #[_, _, p]) => getHeadTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getHeadTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getHeadTk p
+  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getHeadTk p
+  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
+  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => some tk
+  | (``Parser.withAntiquot, #[_, p]) => getHeadTk p
+  | (``Parser.leadingNode, #[_, _, p]) => getHeadTk p
+  | (``HAndThen.hAndThen, #[_, _, _, _, p, _]) => getHeadTk p
+  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
+  | (``Parser.symbol, #[.lit (.strVal tk)]) => some tk
+  | _ => none
+
+/-- Modified from `#help` in `Mathlib.Tactic.HelpCmd` -/
+def getTacticDocstring (env : Environment) (name: Name) : CommandElabM (Option String) := do
+  let name := name.toString (escape := false)
+  let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {}
+
+  let catName : Name := `tactic
+  let catStx : Ident := mkIdent catName -- TODO
+  let some cat := (Parser.parserExtension.getState env).categories.find? catName
+    | throwErrorAt catStx "{catStx} is not a syntax category"
+  liftTermElabM <| Term.addCategoryInfo catStx catName
+  for (k, _) in cat.kinds do
+    let mut used := false
+    if let some tk := do getHeadTk (← (← env.find? k).value?) then
+      let tk := tk.trim
+      if name ≠ tk then -- was `!name.isPrefixOf tk`
+        continue
+      used := true
+      decls := decls.insert tk ((decls.findD tk #[]).push k)
+  for (_name, ks) in decls do
+    for k in ks do
+      if let some doc ← findDocString? env k then
+        return doc
+
+  logWarning <| m!"Could not find a docstring for tactic {name}, consider adding one " ++
+    m!"using `TacticDoc {name} \"some doc\"`"
+  return none
+
+/-- Retrieve the docstring associated to an inventory item. For Tactics, this
+is not guaranteed to work. -/
+def getDocstring (env : Environment) (name : Name) (type : InventoryType) :
+    CommandElabM (Option String) :=
+  match type with
+  -- for tactics it's a lookup following mathlib's `#help`. not guaranteed to be the correct one.
+  | .Tactic => getTacticDocstring env name
+  | .Lemma => findDocString? env name
+  -- TODO: for definitions not implemented yet, does it work?
+  | .Definition => findDocString? env name
+
+/-- Checks if `inventoryTemplateExt` contains an entry with `(type, name)` and yields
+a warning otherwise. If `template` is provided, it will add such an entry instead of yielding a
+warning.
+
+`ref` is the syntax piece. If `name` is not provided, it will use `ident.getId`.
+I used this workaround, because I needed a new name (with correct namespace etc)
+to be used, and I don't know how to create a new ident with same position but different name.
+-/
+def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.getId)
+    (template : Option String := none) : CommandElabM Unit := do
+  -- note: `name` is an `Ident` (instead of `Name`) for the log messages.
+  let env ← getEnv
+  let n := name
+  -- Find a key with matching `(type, name)`.
+  match (inventoryTemplateExt.getState env).findIdx?
+    (fun x => x.name == n && x.type == type) with
+  -- Nothing to do if the entry exists
+  | some _ => pure ()
+  | none =>
+    match template with
+    -- Warn about missing documentation
+    | none =>
+      let docstring ← match (← getDocstring env name type) with
+      | some ds =>
+        logInfoAt ref (m!"Missing {type} Documentation. Using existing docstring. " ++
+        m!"Add {name}\nAdd `{type}Doc {name}` somewhere above this statement.")
+        pure s!"*(lean docstring)*\\\n{ds}"
+      | none =>
+        logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
+        m!"somewhere above this statement.")
+        pure "(missing)"
+
+      -- We just add a dummy entry
+      modifyEnv (inventoryTemplateExt.addEntry · {
+        type := type
+        name := name
+        category := if type == .Lemma then s!"{n.getPrefix}" else ""
+        content := docstring})
+    -- Add the default documentation
+    | some s =>
+      modifyEnv (inventoryTemplateExt.addEntry · {
+        type := type
+        name := name
+        category := if type == .Lemma then s!"{n.getPrefix}" else ""
+        content := s })
+      logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++
+        m!"docstring) instead. If you want to write a different description, add " ++
+        m!"`{type}Doc {name}` somewhere above this statement.")
+
 /-- Documentation entry of a tactic. Example:
 
 ```
@@ -139,40 +196,37 @@ TacticDoc rw "`rw` stands for rewrite, etc. "
 * The identifier is the tactics name. Some need to be escaped like `«have»`.
 * The description is a string supporting Markdown.
  -/
-elab doc:docComment ? "TacticDoc" name:ident content:str ? : command => do
-  let doc ← parseDocCommentLegacy doc content
+elab "TacticDoc" name:ident content:str : command =>
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Tactic
     name := name.getId
     displayName := name.getId.toString
-    content := doc })
+    content := content.getString })
 
-/-- Documentation entry of a theorem. Example:
+/-- Documentation entry of a lemma. Example:
 
 ```
-TheoremDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
+LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 ```
 
-* 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 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 string following `as` is the displayed name (in the Inventory).
-* The identifier after `in` is the category to group theorems by (in the Inventory).
+* The identifier after `in` is the category to group lemmas 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 theorem/definition to have the same fully qualified name as in mathlib.
+The lemma/definition to have the same fully qualified name as in mathlib.
  -/
-elab doc:docComment ? "TheoremDoc" name:ident "as" displayName:str "in" category:str content:str ? :
-    command => do
-  let doc ← parseDocCommentLegacy doc content
+elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Lemma
     name := name.getId
     category := category.getString
     displayName := displayName.getString
-    content := doc })
+    content := content.getString })
 -- TODO: Catch the following behaviour.
--- 1. if `TheoremDoc` appears in the same file as `Statement`, it will silently use
+-- 1. if `LemmaDoc` 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,25 +244,37 @@ 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 theorem/definition to have the same fully qualified name as in mathlib.
+The lemma/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
+elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Definition
     name := name.getId,
     displayName := displayName.getString,
-    content := doc })
+    content := template.getString })
 
 /-! ## 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₃`!"
+def getStatement (name : Name) : CommandElabM MessageData := do
+  return ← addMessageContextPartial (.ofPPFormat { pp := fun
+    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
+    | none     => return "that's a bug." })
+
+-- Note: We use `String` because we can't send `MessageData` as json, but
+-- `MessageData` might be better for interactive highlighting.
+/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`.
+
+Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
+`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
+def getStatementString (name : Name) : CommandElabM String := do
+  try
+    return ← (← getStatement name).toString
+  catch
+  | _ => throwError m!"Could not find {name} in context."
+  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.
 
 /-- 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
@@ -216,16 +282,14 @@ 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 theorems that are introduced by this level. -/
-elab "NewTheorem" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewTheorem"
+/-- Declare lemmas that are introduced by this level. -/
+elab "NewLemma" args:ident* : command => do
   for name in ↑args do
     try let _decl ← getConstInfo name.getId catch
       | _ => logErrorAt name m!"unknown identifier '{name}'."
@@ -235,7 +299,6 @@ elab "NewTheorem" 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)}}
@@ -243,36 +306,31 @@ 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 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"
+/-- Declare lemmas that are temporarily disabled in this level.
+This is ignored if `OnlyLemma` is set. -/
+elab "DisabledLemma" args:ident* : command => do
   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 theorems except the ones declared here -/
-elab "OnlyTheorem" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyTheorem"
+/-- Temporarily disable all lemmas except the ones declared here -/
+elab "OnlyLemma" args:ident* : command => do
   for name in ↑args do checkInventoryDoc .Lemma name
   modifyCurLevel fun level => pure {level with
     lemmas := {level.lemmas with only := args.map (·.getId)}}
@@ -280,66 +338,65 @@ elab "OnlyTheorem" 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: `TheoremTab "Nat"`.
+/-- Define which tab of Lemmas is opened by default. Usage: `LemmaTab "Nat"`.
 If omitted, the current tab will remain open. -/
-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`"
+elab "LemmaTab"  category:str : command =>
   modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
 
 /-! # Exercise Statement -/
 
+/-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
+syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
+-- TODO
+
+-- TODO: Reuse the following code for checking available tactics in user code:
+structure UsedInventory where
+(tactics : HashSet Name := {})
+(definitions : HashSet Name := {})
+(lemmas : HashSet Name := {})
+
+partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : CommandElabM UsedInventory := do
+  match stx with
+  | .missing => return acc
+  | .node _info kind args =>
+    if kind == `GameServer.Tactic.Hint || kind == `GameServer.Tactic.Branch then return acc
+    return ← args.foldlM (fun acc arg => collectUsedInventory arg acc) acc
+  | .atom _info val =>
+    -- ignore syntax elements that do not start with a letter
+    -- and ignore some standard keywords
+    let allowed := ["with", "fun", "at", "only", "by"]
+    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`
+      return {acc with tactics := acc.tactics.insert val}
+    else
+      return acc
+  | .ident _info _rawVal val _preresolved =>
+      let ns ←
+        try resolveGlobalConst (mkIdent val)
+        catch | _ => pure [] -- catch "unknown constant" error
+      return ← ns.foldlM (fun acc n => do
+        if let some (.thmInfo ..) := (← getEnv).find? n then
+          return {acc with lemmas := acc.lemmas.insertMany ns}
+        else
+          return {acc with definitions := acc.definitions.insertMany ns}
+      ) acc
+
+-- #check expandOptDocComment?
+
 /-- Define the statement of the current level. -/
 elab doc:docComment ? attrs:Parser.Term.attributes ?
     "Statement" statementName:ident ? sig:declSig val:declVal : command => do
   let lvlIdx ← getCurLevelIdx
 
-  let docContent ← parseDocComment doc
+  let docContent : Option String := match doc with
+  | none => none
+  | some s => match s.raw[1] with
+    | .atom _ val => val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩))
+    | _           => none --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}"
 
   -- Save the messages before evaluation of the proof.
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
@@ -440,6 +497,23 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
 
 /-! # Hints -/
 
+syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
+
+/-- Remove any spaces at the beginning of a new line -/
+partial def removeIndentation (s : String) : String :=
+  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
+    let c := s.get i
+    let i := s.next i
+    if s.atEnd i then
+      acc.push c
+    else if removeSpaces && c == ' ' then
+      loop i acc (removeSpaces := true)
+    else if c == '\n' then
+      loop i (acc.push c) (removeSpaces := true)
+    else
+      loop i (acc.push c)
+  loop ⟨0⟩ ""
+
 /-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
 see hints. The tactic does not affect the goal state.
 -/
@@ -552,7 +626,6 @@ elab "Template" tacs:tacticSeq : tactic => do
   modifyLevel (←getCurLevelId) fun level => do
     return {level with template := s!"{template}"}
 
-
 -- TODO: Notes for testing if a declaration has the simp attribute
 
 -- -- Test: From zulip
@@ -571,6 +644,98 @@ elab "Template" tacs:tacticSeq : tactic => do
 
 /-! # Make Game -/
 
+def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
+| .Tactic => level.tactics
+| .Definition => level.definitions
+| .Lemma => level.lemmas
+
+def GameLevel.setComputedInventory (level : GameLevel) :
+    InventoryType → Array InventoryTile → GameLevel
+| .Tactic, v =>     {level with tactics     := {level.tactics     with tiles := v}}
+| .Definition, v => {level with definitions := {level.definitions with tiles := v}}
+| .Lemma, v =>      {level with lemmas      := {level.lemmas      with tiles := v}}
+
+partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name))
+      (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) :
+    HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do
+  match (newArrows.find? id, decendants.find? id) with
+  | (some _, some _) => return (newArrows, decendants)
+  | _ =>
+    let mut newArr := newArrows
+    let mut desc := decendants
+    desc := desc.insert id {} -- mark as worked in case of loops
+    newArr := newArr.insert id {} -- mark as worked in case of loops
+    let children := arrows.findD id {}
+    let mut trimmedChildren := children
+    let mut theseDescs := children
+    for child in children do
+      (newArr, desc) := removeTransitiveAux child arrows newArr desc
+      let childDescs := desc.findD child {}
+      theseDescs := theseDescs.insertMany childDescs
+      for d in childDescs do
+        trimmedChildren := trimmedChildren.erase d
+    desc := desc.insert id theseDescs
+    newArr := newArr.insert id trimmedChildren
+    return (newArr, desc)
+
+def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do
+  let mut newArr := {}
+  let mut desc := {}
+  for id in arrows.toArray.map Prod.fst do
+    (newArr, desc) := removeTransitiveAux id arrows newArr desc
+    if (desc.findD id {}).contains id then
+      logError <| m!"Loop at {id}. " ++
+        m!"This should not happen and probably means that `findLoops` has a bug."
+      -- DEBUG:
+      -- for ⟨x, hx⟩ in desc.toList do
+      --   m := m ++ m!"{x}: {hx.toList}\n"
+      -- logError m
+
+  return newArr
+
+/-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`.
+
+For performance reason it returns a HashSet of visited
+nodes as well. This is filled with all nodes ever looked at as they cannot be
+part of a loop anymore. -/
+partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name)
+    (path : Array Name := #[]) (visited : HashSet Name := {}) :
+    Array Name × HashSet Name := Id.run do
+  let mut visited := visited
+  match path.getIdx? node with
+  | some i =>
+    -- Found a loop: `node` is already the iᵗʰ element of the path
+    return (path.extract i path.size, visited.insert node)
+  | none =>
+    for successor in arrows.findD node {} do
+      -- If we already visited the successor, it cannot be part of a loop anymore
+      if visited.contains successor then
+        continue
+      -- Find any loop involving `successor`
+      let (loop, _) := findLoopsAux arrows successor (path.push node) visited
+      visited := visited.insert successor
+      -- No loop found in the dependants of `successor`
+      if loop.isEmpty then
+        continue
+      -- Found a loop, return it
+      return (loop, visited)
+  return (#[], visited.insert node)
+
+/-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/
+partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do
+  let mut visited : HashSet Name := {}
+  for node in arrows.toArray.map (·.1) do
+    -- Skip a node if it was already visited
+    if visited.contains node then
+      continue
+    -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its
+    -- search starting from `node`
+    let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited))
+    visited := moreVisited
+    if !loop.isEmpty then
+      return loop.toList
+  return []
+
 /-- The worlds of a game are joint by dependencies. These are
 automatically computed but can also be defined with the syntax
 `Dependency World₁ → World₂ → World₃`. -/
@@ -645,12 +810,8 @@ elab "MakeGame" : command => do
   -- Items that should not be displayed in inventory
   let mut hiddenItems : HashSet Name := {}
 
-  let allWorlds := game.worlds.nodes.toArray
-  let nrWorlds := allWorlds.size
-  let mut nrLevels := 0
-
   -- Calculate which "items" are used/new in which world
-  for (worldId, world) in allWorlds do
+  for (worldId, world) in game.worlds.nodes.toArray do
     let mut usedItems : HashSet Name := {}
     let mut newItems : HashSet Name := {}
     for inventoryType in #[.Tactic, .Definition, .Lemma] do
@@ -689,12 +850,9 @@ elab "MakeGame" : command => do
     -- logInfo m!"{worldId} uses: {usedItems.toList}"
     -- logInfo m!"{worldId} introduces: {newItems.toList}"
 
-    -- Moreover, count the number of levels in the game
-    nrLevels := nrLevels + world.levels.toArray.size
-
   /- for each "item" this is a HashSet of `worldId`s that introduce this item -/
   let mut worldsWithNewItem : HashMap Name (HashSet Name) := {}
-  for (worldId, _world) in allWorlds do
+  for (worldId, _world) in game.worlds.nodes.toArray do
     for newItem in newItemsInWorld.findD worldId {} do
       worldsWithNewItem := worldsWithNewItem.insert newItem $
         (worldsWithNewItem.findD newItem {}).insert worldId
@@ -706,7 +864,7 @@ elab "MakeGame" : command => do
   let mut dependencyReasons : HashMap (Name × Name) (HashSet Name) := {}
 
   -- Calculate world dependency graph `game.worlds`
-  for (dependentWorldId, _dependentWorld) in allWorlds do
+  for (dependentWorldId, _dependentWorld) in game.worlds.nodes.toArray do
     let mut dependsOnWorlds : HashSet Name := {}
     -- Adding manual dependencies that were specified via the `Dependency` command.
     for (sourceId, targetId) in game.worlds.edges do
@@ -757,25 +915,14 @@ elab "MakeGame" : command => do
         logError m!"{w1} depends on {w2} because of {items.toList}."
   else
     worldDependsOnWorlds ← removeTransitive worldDependsOnWorlds
-
-    -- need to delete all existing edges as they are already present in `worldDependsOnWorlds`.
-    modifyCurGame fun game =>
-      pure {game with worlds := {game.worlds with edges := Array.empty}}
-
     for (dependentWorldId, worldIds) in worldDependsOnWorlds.toArray do
       modifyCurGame fun game =>
         pure {game with worlds := {game.worlds with
           edges := game.worlds.edges.append (worldIds.toArray.map fun wid => (wid, dependentWorldId))}}
 
-  -- Add the number of levels and worlds to the tile for the landing page
-  modifyCurGame fun game => pure {game with tile := {game.tile with
-    levels := nrLevels
-    worlds := nrWorlds }}
-
   -- Apparently we need to reload `game` to get the changes to `game.worlds` we just made
   let game ← getCurGame
 
-  let mut allItemsByType : HashMap InventoryType (HashSet Name) := {}
   -- Compute which inventory items are available in which level:
   for inventoryType in #[.Tactic, .Definition, .Lemma] do
 
@@ -837,7 +984,6 @@ elab "MakeGame" : command => do
               name := item
               displayName := data.displayName
               category := data.category
-              altTitle := data.statement
               hidden := hiddenItems.contains item })
 
 
@@ -857,7 +1003,6 @@ elab "MakeGame" : command => do
             displayName := data.displayName
             category := data.category
             locked := false
-            altTitle := data.statement
             hidden := hiddenItems.contains item }
       itemsInWorld := itemsInWorld.insert worldId items
 
@@ -877,8 +1022,7 @@ elab "MakeGame" : command => do
             displayName := data.displayName
             category := data.category
             locked := false
-            altTitle := data.statement
-            hidden := hiddenItems.contains item }
+            hidden := levelInfo.hidden.contains item }
 
         -- add the exercise statement from the previous level
         -- if it was named
@@ -891,7 +1035,6 @@ 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
@@ -909,18 +1052,17 @@ elab "MakeGame" : command => do
 
         modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
           return level.setComputedInventory inventoryType itemsArray
-    allItemsByType := allItemsByType.insert inventoryType allItems
 
-  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
-  }
+/-! # Debugging tools -/
 
-  saveGameData allItemsByType inventory
+-- /-- Print current game for debugging purposes. -/
+-- elab "PrintCurGame" : command => do
+--   logInfo (toJson (← getCurGame))
+
+/-- Print current level for debugging purposes. -/
+elab "PrintCurLevel" : command => do
+  logInfo (repr (← getCurLevel))
+
+/-- Print levels for debugging purposes. -/
+elab "PrintLevels" : command => do
+  logInfo $ repr $ (← getCurWorld).levels.toArray

server/GameServer/EnvExtensions.lean

@@ -106,16 +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 := {
-      name := item.name,
-      displayName := item.displayName
-      category := item.category
-}
-
 /-- The extension that stores the doc templates. Note that you can only add, but never modify
 entries! -/
 initialize inventoryTemplateExt :
@@ -143,18 +135,7 @@ def getInventoryItem? [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
     m (Option InventoryItem) := do
   return (inventoryExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
 
-structure InventoryOverview where
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  lemmaTab : Option String
-deriving ToJson, FromJson
 
--- TODO: Reuse the following code for checking available tactics in user code:
-structure UsedInventory where
-(tactics : HashSet Name := {})
-(definitions : HashSet Name := {})
-(lemmas : HashSet Name := {})
 
 /-! ## Environment extensions for game specification -/
 
@@ -273,63 +254,8 @@ structure GameLevel where
   lemmas: InventoryInfo := default
   /-- A proof template that is printed in an empty editor. -/
   template: Option String := none
-  /-- The image for this level. -/
-  image : String := default
-deriving Inhabited, Repr
+  deriving Inhabited, Repr
 
-/-- Json-encodable version of `GameLevel`
-Fields:
-- description: Lemma in mathematical language.
-- descriptionGoal: Lemma printed as Lean-Code.
--/
-structure LevelInfo where
-  index : Nat
-  title : String
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  introduction : String
-  conclusion : String
-  descrText : Option String := none
-  descrFormat : String := ""
-  lemmaTab : Option String
-  module : Name
-  displayName : Option String
-  statementName : Option String
-  template : Option String
-  image: Option String
-deriving ToJson, FromJson
-
-def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
-  { index := lvl.index,
-    title := lvl.title,
-    tactics := lvl.tactics.tiles,
-    lemmas := lvl.lemmas.tiles,
-    definitions := lvl.definitions.tiles,
-    descrText := lvl.descrText,
-    descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
-    introduction := lvl.introduction
-    conclusion := lvl.conclusion
-    lemmaTab := match lvl.lemmaTab with
-    | some tab => tab
-    | none =>
-      -- Try to set the lemma tab to the category of the first added lemma
-      match lvl.lemmas.tiles.find? (·.new) with
-      | 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?
-          (fun x => x.name == name && x.type == .Lemma) with
-        | some n => n.displayName
-        | none => name.toString
-        -- Note: we could call `.find!` because we check in `Statement` that the
-        -- lemma doc must exist.
-    template := lvl.template
-    image := lvl.image
-  }
 
 /-! ## World -/
 
@@ -345,46 +271,17 @@ structure World where
   conclusion : String := default
   /-- The levels of the world. -/
   levels: HashMap Nat GameLevel := default
-  /-- The introduction image of the world. -/
-  image: String := default
 deriving Inhabited
 
 instance : ToJson World := ⟨
   fun world => Json.mkObj [
     ("name", toJson world.name),
     ("title", world.title),
-    ("introduction", world.introduction),
-    ("image", world.image)]
+    ("introduction", world.introduction)]
 ⟩
 
 /-! ## Game -/
 
-/-- A tile as they are displayed on the servers landing page. -/
-structure GameTile where
-  /-- The title of the game -/
-  title: String
-  /-- One catch phrase about the game -/
-  short: String := default
-  /-- One paragraph description what the game is about -/
-  long: String := default
-  /-- List of languages the game supports
-
-  TODO: What's the expectected format
-  TODO: Must be a list with a single language currently
-   -/
-  languages: List String := default
-  /-- A list of games which this one builds upon -/
-  prerequisites: List String := default
-  /-- Number of worlds in the game -/
-  worlds: Nat := default
-  /-- Number of levels in the game -/
-  levels: Nat := default
-  /-- A cover image of the game
-
-  TODO: What's the format? -/
-  image: String := default
-deriving Inhabited, ToJson, FromJson
-
 structure Game where
   /-- Internal name of the game. -/
   name : Name
@@ -399,18 +296,7 @@ structure Game where
   /-- TODO: currently unused. -/
   authors : List String := default
   worlds : Graph Name World := default
-  /-- The tile displayed on the server's landing page. -/
-  tile : GameTile := default
-  /-- The path to the background image of the world. -/
-  image : String := default
-deriving Inhabited, ToJson, FromJson
-
-def getGameJson (game : «Game») : Json := Id.run do
-  let gameJson : Json := toJson game
-  -- Add world sizes to Json object
-  let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
-  let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
-  return gameJson
+deriving Inhabited, ToJson
 
 /-! ## Game environment extension -/
 

server/GameServer/FileWorker.lean

@@ -1,8 +1,6 @@
-/- This file is adapted from `Lean/Server/FileWorker.lean`. -/
+/- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/
 import Lean.Server.FileWorker
 import GameServer.Game
-import GameServer.ImportModules
-import GameServer.SaveData
 
 namespace MyModule
 open Lean
@@ -18,7 +16,7 @@ private def mkEOI (pos : String.Pos) : Syntax :=
   mkNode ``Command.eoi #[atom]
 
 partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
-  (mps : ModuleParserState) (messages : MessageLog) :
+  (mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) :
     Syntax × ModuleParserState × MessageLog × String.Pos := Id.run do
   let mut pos := mps.pos
   let mut recovering := mps.recovering
@@ -57,20 +55,6 @@ open IO
 open Snapshots
 open JsonRpc
 
-structure GameWorkerState :=
-  inventory : Array String
-  /--
-  Check for tactics/theorems that are not unlocked.
-  0: no check
-  1: give warnings
-  2: give errors
-  -/
-  difficulty : Nat
-  levelInfo : LevelInfo
-  deriving ToJson, FromJson
-
-abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
-
 section Elab
 
 def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
@@ -88,30 +72,29 @@ def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : Me
 /-- Find all tactics in syntax object that are forbidden according to a
 set `allowed` of allowed tactics. -/
 partial def findForbiddenTactics (inputCtx : Parser.InputContext)
-    (gameWorkerState : GameWorkerState) (stx : Syntax) :
+    (levelParams : Game.DidOpenLevelParams) (stx : Syntax) :
     Elab.Command.CommandElabM Unit := do
-  let levelInfo := gameWorkerState.levelInfo
   match stx with
   | .missing => return ()
   | .node _info _kind args =>
     for arg in args do
-      findForbiddenTactics inputCtx gameWorkerState arg
+      findForbiddenTactics inputCtx levelParams arg
   | .atom info val =>
     -- ignore syntax elements that do not start with a letter
     -- and ignore "with" keyword
     let allowed := ["with", "fun", "at", "only", "by", "to"]
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      match levelInfo.tactics.find? (·.name.toString == val) with
+      match levelParams.tactics.find? (·.name.toString == val) with
       | none =>
         -- Note: This case means that the tactic will never be introduced in the game.
-        match gameWorkerState.inventory.find? (· == val) with
+        match levelParams.inventory.find? (· == val) with
         | none =>
           addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
         | some _ => pure () -- tactic is in the inventory, allow it.
       | some tac =>
         if tac.locked then
-          match gameWorkerState.inventory.find? (· == val) with
+          match levelParams.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.
@@ -125,10 +108,10 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
         let some (.thmInfo ..) := (← getEnv).find? n
           | return () -- not a theorem -> ignore
         -- Forbid the theorem we are proving currently
-        if some n = levelInfo.statementName then
+        if n = levelParams.statementName then
           addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
 
-        let lemmasAndDefs := levelInfo.lemmas ++ levelInfo.definitions
+        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 =>
@@ -137,7 +120,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
           else if lem.disabled then
             addWarningMessage info s!"The lemma/definition '{n}' is disabled in this level!"
 where addWarningMessage (info : SourceInfo) (s : MessageData) :=
-  let difficulty := gameWorkerState.difficulty
+  let difficulty := levelParams.difficulty
   if difficulty > 0 then
     modify fun st => { st with
       messages := st.messages.add {
@@ -153,7 +136,7 @@ where addWarningMessage (info : SourceInfo) (s : MessageData) :=
 
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
-    (couldBeEndSnap : Bool) (gameWorkerState : GameWorkerState)
+    (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams)
     (initParams : Lsp.InitializeParams) : IO Snapshot := do
   -- Recognize end snap
   if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
@@ -184,7 +167,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
     Elab.Command.catchExceptions
       (getResetInfoTrees *> do
         let some level ← GameServer.getLevelByFileName? initParams inputCtx.fileName
-          | panic! s!"Level not found: {inputCtx.fileName} / {GameServer.levelIdFromFileName? initParams inputCtx.fileName}"
+          | throwError "Level not found: {inputCtx.fileName}"
         let scope := level.scope
 
         -- use open namespaces and options as in the level file
@@ -202,12 +185,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
+            MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap
           modify (fun s => { s with messages := msgLog })
           parseResultRef.set (tacticStx, cmdParserState)
 
           -- Check for forbidden tactics
-          findForbiddenTactics inputCtx gameWorkerState tacticStx
+          findForbiddenTactics inputCtx levelParams 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 #[]
@@ -235,7 +218,6 @@ 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
@@ -287,7 +269,7 @@ where
 
   /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
   private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-      (gameWorkerState : GameWorkerState) (initParams : Lsp.InitializeParams)
+      (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams)
       : AsyncElabM (Option Snapshot) := do
     cancelTk.check
     let s ← get
@@ -305,7 +287,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
-      gameWorkerState initParams
+      levelParams initParams
     set { s with snaps := s.snaps.push snap }
     -- TODO(MH): check for interrupt with increased precision
     cancelTk.check
@@ -327,7 +309,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) (gameWorkerState : GameWorkerState)
+      (startAfterMs : UInt32) (levelParams : Game.DidOpenLevelParams)
       : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
     let ctx ← read
     let some headerSnap := snaps[0]? | panic! "empty snapshots"
@@ -343,15 +325,21 @@ 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 gameWorkerState ctx.initParams) { snaps })
+        AsyncList.unfoldAsync (nextSnap ctx m cancelTk levelParams ctx.initParams) { snaps })
 
 end Elab
 
+structure GameWorkerState :=
+(levelParams : Game.DidOpenLevelParams)
+
+abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
+
 section Updates
 
 /-- Given the new document, updates editable doc state. -/
   def updateDocument (newMeta : DocumentMeta) : GameWorkerM Unit := do
     let s ← get
+    let levelParams := s.levelParams
     let ctx ← read
     let oldDoc := (← StateT.lift get).doc
     oldDoc.cancelTk.set
@@ -393,7 +381,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 s ctx
+      unfoldSnaps newMeta validSnaps.toArray cancelTk levelParams ctx
         (startAfterMs := ctx.initParams.editDelay.toUInt32)
     StateT.lift <| modify fun st => { st with
       doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
@@ -408,23 +396,24 @@ section Initialization
     fileMap  := default
 
   def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-      (gameDir : String) (module : Name):
+      (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) :
       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 := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
+      { cwd := levelParams.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
+    let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p
 
     -- Set the search path
     Lean.searchPathRef.set paths
 
-    let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }]
+    let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
+    -- return (env, paths)
 
     -- use empty header
     let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
@@ -468,11 +457,10 @@ section Initialization
       return (headerSnap, srcSearchPath)
 
   def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
-      (gameDir : String) (gameWorkerState : GameWorkerState) : IO (WorkerContext × WorkerState) := do
+       (levelParams : Game.DidOpenLevelParams) : IO (WorkerContext × WorkerState) := do
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
-
     let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-      gameDir gameWorkerState.levelInfo.module
+      levelParams initParams
     let cancelTk ← CancelToken.new
     let ctx :=
       { hIn  := i
@@ -483,7 +471,7 @@ section Initialization
         clientHasWidgets
       }
     let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
+      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk levelParams ctx (startAfterMs := 0)
       | Except.error e   => throw (e : ElabTaskError))
     let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
     return (ctx,
@@ -508,7 +496,7 @@ section NotificationHandling
       IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
     else if ¬ changes.isEmpty then
       let newDocText := foldDocumentChanges changes oldDoc.meta.text
-      updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
+      updateDocument ⟨docId.uri, newVersion, newDocText⟩
 
 end NotificationHandling
 
@@ -520,7 +508,6 @@ section MessageHandling
     match method with
     | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
     | "$/cancelRequest"        => handle CancelParams (handleCancelRequest ·)
-    | "$/setTrace"        => pure ()
     | "$/lean/rpc/release"     => handle RpcReleaseParams (handleRpcRelease ·)
     | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
     | _                        => throwServerError s!"Got unsupported notification method: {method}"
@@ -559,32 +546,26 @@ section MainLoop
       let doc := st.doc
       doc.cancelTk.set
       return ()
-    | Message.request id "shutdown" none =>
-      ctx.hOut.writeLspResponse ⟨id, Json.null⟩
+    | 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) =>
       handleNotification method (toJson params)
       mainLoop
-    | _ => throwServerError s!"Got invalid JSON-RPC message: {toJson msg}"
+    | _ => throwServerError "Got invalid JSON-RPC message"
 end MainLoop
 
-def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
+def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
-  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 initParams ← i.readLspRequestAs "initialize" InitializeParams
   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
@@ -592,28 +573,13 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
     This is because LSP always refers to characters by (line, column),
     so if we get the line number correct it shouldn't matter that there
     is a CR there. -/
-  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
+  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
-    let game ← loadGameData gameDir
-    -- TODO: We misuse the `rootUri` field to the gameName
-    let rootUri? : Option String := some (toString game.name)
-    let initParams := {initRequest.param.toLeanInternal with rootUri?}
-    let some (levelId : LevelId) := GameServer.levelIdFromFileName?
-        initParams meta.mkInputContext.fileName
-      | throwServerError s!"Could not determine level ID: {meta.mkInputContext.fileName}"
-    let levelInfo ← loadLevelData gameDir levelId.world levelId.level
-    let some initializationOptions := initRequest.param.initializationOptions?
-      | throwServerError "no initialization options found"
-    let gameWorkerState : GameWorkerState:= {
-      inventory := initializationOptions.inventory
-      difficulty := initializationOptions.difficulty
-      levelInfo
-    }
-    let (ctx, st) ← initializeWorker meta i o e initParams opts gameDir gameWorkerState
+    let (ctx, st) ← initializeWorker meta i o e initParams.param opts levelParams
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
-      StateT.run (s := gameWorkerState) <| (mainLoop)
+      StateT.run (s := {levelParams := levelParams}) <| (mainLoop)
     return (0 : UInt32)
   catch e =>
     IO.eprintln e
@@ -623,13 +589,12 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
       message := e.toString }] o
     return (1 : UInt32)
 
-def workerMain (opts : Options) (args : List String): IO UInt32 := do
+def workerMain (opts : Options) : IO UInt32 := do
   let i ← IO.getStdin
   let o ← IO.getStdout
   let e ← IO.getStderr
   try
-    let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
-    let exitCode ← initAndRunWorker i o e opts gameDir
+    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
     o.flush

server/GameServer/Game.lean

@@ -25,56 +25,227 @@ open Lsp
 open JsonRpc
 open IO
 
-/- Game-specific version of `InitializeParams` that allows for extra options: -/
+def getGame (game : Name): GameServerM Json := do
+  let some game ← getGame? game
+    | throwServerError "Game not found"
+  let gameJson : Json := toJson game
+  -- Add world sizes to Json object
+  let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
+  let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
+  return gameJson
 
-structure InitializationOptions extends Lean.Lsp.InitializationOptions :=
-  difficulty : Nat
-  inventory : Array String
+/--
+Fields:
+- description: Lemma in mathematical language.
+- descriptionGoal: Lemma printed as Lean-Code.
+-/
+structure LevelInfo where
+  index : Nat
+  title : String
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
+  introduction : String
+  conclusion : String
+  descrText : Option String := none
+  descrFormat : String := ""
+  lemmaTab : Option String
+  displayName : Option String
+  statementName : Option String
+  template : Option String
+deriving ToJson, FromJson
+
+structure InventoryOverview where
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
+  lemmaTab : Option String
+deriving ToJson, FromJson
+
+structure LoadLevelParams where
+  world : Name
+  level : 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
+-- structure LoadTemplateParams where
+--   world : Name
+--   level : Nat
+--   deriving ToJson, FromJson
 
-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⟩
+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
+  -/
+  difficulty : Nat
+  /-- The name of the theorem to be proven in this level. -/
+  statementName : Name
+  deriving ToJson, FromJson
 
-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?
+structure LoadDocParams where
+  name : Name
+  type : InventoryType
+deriving ToJson, FromJson
+
+structure SetInventoryParams where
+  inventory : Array String
+  difficulty : Nat
+deriving ToJson, FromJson
+
+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
+    }
   }
-  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.request id "info" _ =>
+      let s ← get
+      let c ← read
+      c.hOut.writeLspResponse ⟨id, (← getGame s.game)⟩
+      return true
+    | Message.request id "loadLevel" params =>
+      let p ← parseParams LoadLevelParams (toJson params)
+      let s ← get
+      let c ← read
+      let some lvl ← getLevel? {game := s.game, world := p.world, level := p.level}
+        | do
+          c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩
+          return true
+
+      let env ← getEnv
+
+      let levelInfo : LevelInfo :=
+          { index := lvl.index,
+            title := lvl.title,
+            tactics := lvl.tactics.tiles,
+            lemmas := lvl.lemmas.tiles,
+            definitions := lvl.definitions.tiles,
+            descrText := lvl.descrText,
+            descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
+            introduction := lvl.introduction
+            conclusion := lvl.conclusion
+            lemmaTab := match lvl.lemmaTab with
+            | some tab => tab
+            | none =>
+              -- Try to set the lemma tab to the category of the first added lemma
+              match lvl.lemmas.tiles.find? (·.new) with
+              | some tile => tile.category
+              | none => none
+            statementName := lvl.statementName.toString
+            displayName := match lvl.statementName with
+              | .anonymous => none
+              | name => match (inventoryExt.getState env).find?
+                  (fun x => x.name == name && x.type == .Lemma) with
+                | some n => n.displayName
+                | none => name.toString
+                -- Note: we could call `.find!` because we check in `Statement` that the
+                -- lemma doc must exist.
+            template := lvl.template
+            }
+      c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩
+      return true
+    -- | Message.request id "loadTemplate" params =>
+    --   let p ← parseParams LoadTemplateParams (toJson params)
+    --   let s ← get
+    --   let c ← read
+
+    --   let some game ← getGame? s.game
+    --     | throwServerError "Game not found"
+    --   let some world := game.worlds.nodes.find? p.world
+    --     | throwServerError "World not found"
+
+    --   let mut templates : Array <| Option String := #[]
+    --   for (_, level) in world.levels.toArray do
+    --     templates := templates.push level.template
+    --   c.hOut.writeLspResponse ⟨id, ToJson.toJson templates⟩
+    --   return true
+    | Message.request id "loadDoc" params =>
+      let p ← parseParams LoadDocParams (toJson params)
+      let c ← read
+      let some doc ← getInventoryItem? p.name p.type
+        | do
+            c.hOut.writeLspResponseError ⟨id, .invalidParams,
+              s!"Documentation not found: {p.name}", none⟩
+            return true
+      -- TODO: not necessary at all?
+      -- Here we only need to convert the fields that were not `String` in the `InventoryDocEntry`
+      -- let doc : InventoryItem := { doc with
+      --   name := doc.name.toString }
+      c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩
+      return true
+    | 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
+    | Message.request id "loadInventoryOverview" _ =>
+      let s ← get
+      let some game ← getGame? s.game
+        | return false
+      -- All Levels have the same tiles, so we just load them from level 1 of an arbitrary world
+      -- and reset `new`, `disabled` and `unlocked`.
+      -- Note: as we allow worlds without any levels (for developing), we might need
+      -- to try until we find the first world with levels.
+      for ⟨worldId, _⟩ in game.worlds.nodes.toList do
+        let some lvl ← getLevel? {game := s.game, world := worldId, level := 1}
+          | do continue
+        let inventory : InventoryOverview := {
+          tactics := lvl.tactics.tiles.map
+            ({ · with locked := true, disabled := false, new := false }),
+          lemmas := lvl.lemmas.tiles.map
+            ({ · with locked := true, disabled := false, new := false }),
+          definitions := lvl.definitions.tiles.map
+            ({ · with locked := true, disabled := false, new := false }),
+          lemmaTab := none
+        }
+        let c ← read
+        c.hOut.writeLspResponse ⟨id, ToJson.toJson inventory⟩
+        return true
+      return false
+    | _ => return false
+  | _ => return false
 
 end Game

server/GameServer/Graph.lean

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

server/GameServer/Helpers.lean

@@ -1,190 +0,0 @@
-import Lean
-
-/-! This document contains various things which cluttered `Commands.lean`. -/
-
-open Lean Meta Elab Command
-
-syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
-
-/-! ## Doc Comment Parsing -/
-
-/-- Read a doc comment and get its content. Return `""` if no doc comment available. -/
-def parseDocComment! (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
-    CommandElabM String := do
-  match doc with
-  | none =>
-    logWarning "Add a text to this command with `/-- yada yada -/ MyCommand`!"
-    pure ""
-  | some s => match s.raw[1] with
-    | .atom _ val => pure <| val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩))
-    | _           => pure "" --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}"
-
-/-- Read a doc comment and get its content. Return `none` if no doc comment available. -/
-def parseDocComment (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
-    CommandElabM <| Option String := do
-  match doc with
-  | none => pure none
-  | some _ => parseDocComment! doc
-
-
-/-- TODO: This is only used to provide some backwards compatibility and you can
-replace `parseDocCommentLegacy` with `parseDocComment` in the future. -/
-def parseDocCommentLegacy (doc: Option (TSyntax `Lean.Parser.Command.docComment))
-    (t : Option (TSyntax `str)) : CommandElabM <| String := do
-  match doc with
-  | none =>
-    match t with
-    | none =>
-      pure <| ← parseDocComment! doc
-    | some t =>
-      logWarningAt t "You should use the new Syntax:
-
-      /-- yada yada -/
-      YourCommand
-
-      instead of
-
-      YourCommand \"yada yada\"
-      "
-      pure t.getString
-  | some _ =>
-    match t with
-      | none =>
-        pure <| ← parseDocComment! doc
-      | some t =>
-        logErrorAt t "You must not provide both, a docstring and a string following the command!
-        Only use
-
-        /-- yada yada -/
-        YourCommand
-
-        and remove the string following it!"
-        pure <| ← parseDocComment! doc
-
-/-! ## Statement string -/
-
-def getStatement (name : Name) : CommandElabM MessageData := do
-  return ← addMessageContextPartial (.ofPPFormat { pp := fun
-    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
-    | none     => return "that's a bug." })
-
--- Note: We use `String` because we can't send `MessageData` as json, but
--- `MessageData` might be better for interactive highlighting.
-/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`.
-
-Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
-`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
-def getStatementString (name : Name) : CommandElabM String := do
-  try
-    return ← (← getStatement name).toString
-  catch
-  | _ => throwError m!"Could not find {name} in context."
-  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.
-
-/-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
-syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
--- TODO
-
-
-/-- Remove any spaces at the beginning of a new line -/
-partial def removeIndentation (s : String) : String :=
-  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
-    let c := s.get i
-    let i := s.next i
-    if s.atEnd i then
-      acc.push c
-    else if removeSpaces && c == ' ' then
-      loop i acc (removeSpaces := true)
-    else if c == '\n' then
-      loop i (acc.push c) (removeSpaces := true)
-    else
-      loop i (acc.push c)
-  loop ⟨0⟩ ""
-
-
-/-! ## Loops in Graph-like construct
-
-TODO: Why are we not using graphs here but our own construct `HashMap Name (HashSet Name)`?
--/
-
-partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name))
-      (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) :
-    HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do
-  match (newArrows.find? id, decendants.find? id) with
-  | (some _, some _) => return (newArrows, decendants)
-  | _ =>
-    let mut newArr := newArrows
-    let mut desc := decendants
-    desc := desc.insert id {} -- mark as worked in case of loops
-    newArr := newArr.insert id {} -- mark as worked in case of loops
-    let children := arrows.findD id {}
-    let mut trimmedChildren := children
-    let mut theseDescs := children
-    for child in children do
-      (newArr, desc) := removeTransitiveAux child arrows newArr desc
-      let childDescs := desc.findD child {}
-      theseDescs := theseDescs.insertMany childDescs
-      for d in childDescs do
-        trimmedChildren := trimmedChildren.erase d
-    desc := desc.insert id theseDescs
-    newArr := newArr.insert id trimmedChildren
-    return (newArr, desc)
-
-
-def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do
-  let mut newArr := {}
-  let mut desc := {}
-  for id in arrows.toArray.map Prod.fst do
-    (newArr, desc) := removeTransitiveAux id arrows newArr desc
-    if (desc.findD id {}).contains id then
-      logError <| m!"Loop at {id}. " ++
-        m!"This should not happen and probably means that `findLoops` has a bug."
-      -- DEBUG:
-      -- for ⟨x, hx⟩ in desc.toList do
-      --   m := m ++ m!"{x}: {hx.toList}\n"
-      -- logError m
-
-  return newArr
-
-/-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`.
-
-For performance reason it returns a HashSet of visited
-nodes as well. This is filled with all nodes ever looked at as they cannot be
-part of a loop anymore. -/
-partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name)
-    (path : Array Name := #[]) (visited : HashSet Name := {}) :
-    Array Name × HashSet Name := Id.run do
-  let mut visited := visited
-  match path.getIdx? node with
-  | some i =>
-    -- Found a loop: `node` is already the iᵗʰ element of the path
-    return (path.extract i path.size, visited.insert node)
-  | none =>
-    for successor in arrows.findD node {} do
-      -- If we already visited the successor, it cannot be part of a loop anymore
-      if visited.contains successor then
-        continue
-      -- Find any loop involving `successor`
-      let (loop, _) := findLoopsAux arrows successor (path.push node) visited
-      visited := visited.insert successor
-      -- No loop found in the dependants of `successor`
-      if loop.isEmpty then
-        continue
-      -- Found a loop, return it
-      return (loop, visited)
-  return (#[], visited.insert node)
-
-/-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/
-partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do
-  let mut visited : HashSet Name := {}
-  for node in arrows.toArray.map (·.1) do
-    -- Skip a node if it was already visited
-    if visited.contains node then
-      continue
-    -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its
-    -- search starting from `node`
-    let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited))
-    visited := moreVisited
-    if !loop.isEmpty then
-      return loop.toList
-  return []

server/GameServer/ImportModules.lean

@@ -1,108 +0,0 @@
-import Lean.Environment
-import Std.Tactic.OpenPrivate
-import Lean.Data.Lsp.Communication
-
-open Lean
-
-inductive LoadingKind := | finalizeExtensions | loadConstants
-  deriving ToJson
-
-structure LoadingParams : Type where
-  counter : Nat
-  kind : LoadingKind
-  deriving ToJson
-
--- Code adapted from `Lean/Environment.lean`
-
-partial def importModulesCore' (imports : Array Import) : ImportStateM Unit := do
-  for i in imports do
-    if i.runtimeOnly || (← get).moduleNameSet.contains i.module then
-      continue
-    modify fun s => { s with moduleNameSet := s.moduleNameSet.insert i.module }
-    let mFile ← findOLean i.module
-    unless (← mFile.pathExists) do
-      throw <| IO.userError s!"object file '{mFile}' of module {i.module} does not exist"
-    let (mod, region) ← readModuleData mFile
-    importModulesCore' mod.imports
-    modify fun s => { s with
-      moduleData  := s.moduleData.push mod
-      regions     := s.regions.push region
-      moduleNames := s.moduleNames.push i.module
-    }
-
-open private mkInitialExtensionStates Environment.mk setImportedEntries finalizePersistentExtensions
-  ensureExtensionsArraySize from Lean.Environment
-
-private partial def finalizePersistentExtensions' (env : Environment) (mods : Array ModuleData) (opts : Options) : IO Environment := do
-  loop 0 env
-where
-  loop (i : Nat) (env : Environment) : IO Environment := do
-    (← IO.getStdout).writeLspNotification {
-      method := "$/game/loading",
-      param := {counter := i, kind := .finalizeExtensions : LoadingParams} }
-    -- Recall that the size of the array stored `persistentEnvExtensionRef` may increase when we import user-defined environment extensions.
-    let pExtDescrs ← persistentEnvExtensionsRef.get
-    if i < pExtDescrs.size then
-      let extDescr := pExtDescrs[i]!
-      let s := extDescr.toEnvExtension.getState env
-      let prevSize := (← persistentEnvExtensionsRef.get).size
-      let prevAttrSize ← getNumBuiltinAttributes
-      let newState ← extDescr.addImportedFn s.importedEntries { env := env, opts := opts }
-      let mut env := extDescr.toEnvExtension.setState env { s with state := newState }
-      env ← ensureExtensionsArraySize env
-      if (← persistentEnvExtensionsRef.get).size > prevSize || (← getNumBuiltinAttributes) > prevAttrSize then
-        -- This branch is executed when `pExtDescrs[i]` is the extension associated with the `init` attribute, and
-        -- a user-defined persistent extension is imported.
-        -- Thus, we invoke `setImportedEntries` to update the array `importedEntries` with the entries for the new extensions.
-        env ← setImportedEntries env mods prevSize
-        -- See comment at `updateEnvAttributesRef`
-        env ← updateEnvAttributes env
-      loop (i + 1) env
-    else
-      return env
-
-def finalizeImport' (s : ImportState) (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := do
-  let numConsts := s.moduleData.foldl (init := 0) fun numConsts mod =>
-    numConsts + mod.constants.size + mod.extraConstNames.size
-  let mut const2ModIdx : HashMap Name ModuleIdx := mkHashMap (capacity := numConsts)
-  let mut constantMap : HashMap Name ConstantInfo := mkHashMap (capacity := numConsts)
-  for h:modIdx in [0:s.moduleData.size] do
-    if modIdx % 100 = 0 then
-      let percentage := modIdx * 100 / s.moduleData.size
-      (← IO.getStdout).writeLspNotification {
-        method := "$/game/loading",
-        param := {counter := percentage, kind := .loadConstants : LoadingParams} }
-    let mod := s.moduleData[modIdx]'h.upper
-    for cname in mod.constNames, cinfo in mod.constants do
-      match constantMap.insert' cname cinfo with
-      | (constantMap', replaced) =>
-        constantMap := constantMap'
-        if replaced then
-          throwAlreadyImported s const2ModIdx modIdx cname
-      const2ModIdx := const2ModIdx.insert cname modIdx
-    for cname in mod.extraConstNames do
-      const2ModIdx := const2ModIdx.insert cname modIdx
-  let constants : ConstMap := SMap.fromHashMap constantMap false
-  let exts ← mkInitialExtensionStates
-  let env : Environment := Environment.mk
-    (const2ModIdx    := const2ModIdx)
-    (constants       := constants)
-    (extraConstNames := {})
-    (extensions      := exts)
-    (header          := {
-      quotInit     := !imports.isEmpty -- We assume `core.lean` initializes quotient module
-      trustLevel   := trustLevel
-      imports      := imports
-      regions      := s.regions
-      moduleNames  := s.moduleNames
-      moduleData   := s.moduleData
-    })
-
-  let env ← setImportedEntries env s.moduleData
-  finalizePersistentExtensions' env s.moduleData opts
-
-def importModules' (imports : Array Import) : IO Environment := do
-  withImporting do
-    let (_, s) ← importModulesCore' imports |>.run
-    let env ← finalizeImport' s imports {} 0
-    return env

server/GameServer/Inventory.lean

@@ -1,152 +0,0 @@
-import Lean
-import GameServer.EnvExtensions
-
-open Lean Elab Command
-
-/-- Copied from `Mathlib.Tactic.HelpCmd`.
-
-Gets the initial string token in a parser description. For example, for a declaration like
-`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations
-that don't start with a string constant. -/
-partial def getHeadTk (e : Expr) : Option String :=
-  match (Expr.withApp e λ e a => (e.constName?.getD Name.anonymous, a)) with
-  | (``ParserDescr.node, #[_, _, p]) => getHeadTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getHeadTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getHeadTk p
-  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getHeadTk p
-  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
-  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => some tk
-  | (``Parser.withAntiquot, #[_, p]) => getHeadTk p
-  | (``Parser.leadingNode, #[_, _, p]) => getHeadTk p
-  | (``HAndThen.hAndThen, #[_, _, _, _, p, _]) => getHeadTk p
-  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
-  | (``Parser.symbol, #[.lit (.strVal tk)]) => some tk
-  | _ => none
-
-/-! ## Doc entries -/
-
-/-- Modified from `#help` in `Mathlib.Tactic.HelpCmd` -/
-def getTacticDocstring (env : Environment) (name: Name) : CommandElabM (Option String) := do
-  let name := name.toString (escape := false)
-  let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {}
-
-  let catName : Name := `tactic
-  let catStx : Ident := mkIdent catName -- TODO
-  let some cat := (Parser.parserExtension.getState env).categories.find? catName
-    | throwErrorAt catStx "{catStx} is not a syntax category"
-  liftTermElabM <| Term.addCategoryInfo catStx catName
-  for (k, _) in cat.kinds do
-    let mut used := false
-    if let some tk := do getHeadTk (← (← env.find? k).value?) then
-      let tk := tk.trim
-      if name ≠ tk then -- was `!name.isPrefixOf tk`
-        continue
-      used := true
-      decls := decls.insert tk ((decls.findD tk #[]).push k)
-  for (_name, ks) in decls do
-    for k in ks do
-      if let some doc ← findDocString? env k then
-        return doc
-
-  logWarning <| m!"Could not find a docstring for tactic {name}, consider adding one " ++
-    m!"using `TacticDoc {name} \"some doc\"`"
-  return none
-
-/-- Retrieve the docstring associated to an inventory item. For Tactics, this
-is not guaranteed to work. -/
-def getDocstring (env : Environment) (name : Name) (type : InventoryType) :
-    CommandElabM (Option String) :=
-  match type with
-  -- for tactics it's a lookup following mathlib's `#help`. not guaranteed to be the correct one.
-  | .Tactic => getTacticDocstring env name
-  | .Lemma => findDocString? env name
-  -- TODO: for definitions not implemented yet, does it work?
-  | .Definition => findDocString? env name
-
-/-- Checks if `inventoryTemplateExt` contains an entry with `(type, name)` and yields
-a warning otherwise. If `template` is provided, it will add such an entry instead of yielding a
-warning.
-
-`ref` is the syntax piece. If `name` is not provided, it will use `ident.getId`.
-I used this workaround, because I needed a new name (with correct namespace etc)
-to be used, and I don't know how to create a new ident with same position but different name.
--/
-def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.getId)
-    (template : Option String := none) : CommandElabM Unit := do
-  -- note: `name` is an `Ident` (instead of `Name`) for the log messages.
-  let env ← getEnv
-  let n := name
-  -- Find a key with matching `(type, name)`.
-  match (inventoryTemplateExt.getState env).findIdx?
-    (fun x => x.name == n && x.type == type) with
-  -- Nothing to do if the entry exists
-  | some _ => pure ()
-  | none =>
-    match template with
-    -- Warn about missing documentation
-    | none =>
-      let docstring ← match (← getDocstring env name type) with
-      | some ds =>
-        logInfoAt ref (m!"Missing {type} Documentation. Using existing docstring. " ++
-        m!"Add {name}\nAdd `{type}Doc {name}` somewhere above this statement.")
-        pure s!"*(lean docstring)*\\\n{ds}"
-      | none =>
-        logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
-        m!"somewhere above this statement.")
-        pure "(missing)"
-
-      -- We just add a dummy entry
-      modifyEnv (inventoryTemplateExt.addEntry · {
-        type := type
-        name := name
-        category := if type == .Lemma then s!"{n.getPrefix}" else ""
-        content := docstring})
-    -- Add the default documentation
-    | some s =>
-      modifyEnv (inventoryTemplateExt.addEntry · {
-        type := type
-        name := name
-        category := if type == .Lemma then s!"{n.getPrefix}" else ""
-        content := s })
-      logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++
-        m!"docstring) instead. If you want to write a different description, add " ++
-        m!"`{type}Doc {name}` somewhere above this statement.")
-
-partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : CommandElabM UsedInventory := do
-  match stx with
-  | .missing => return acc
-  | .node _info kind args =>
-    if kind == `GameServer.Tactic.Hint || kind == `GameServer.Tactic.Branch then return acc
-    return ← args.foldlM (fun acc arg => collectUsedInventory arg acc) acc
-  | .atom _info val =>
-    -- ignore syntax elements that do not start with a letter
-    -- and ignore some standard keywords
-    let allowed := ["with", "fun", "at", "only", "by"]
-    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`
-      return {acc with tactics := acc.tactics.insert val}
-    else
-      return acc
-  | .ident _info _rawVal val _preresolved =>
-      let ns ←
-        try resolveGlobalConst (mkIdent val)
-        catch | _ => pure [] -- catch "unknown constant" error
-      return ← ns.foldlM (fun acc n => do
-        if let some (.thmInfo ..) := (← getEnv).find? n then
-          return {acc with lemmas := acc.lemmas.insertMany ns}
-        else
-          return {acc with definitions := acc.definitions.insertMany ns}
-      ) acc
-
--- #check expandOptDocComment?
-
-def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
-| .Tactic => level.tactics
-| .Definition => level.definitions
-| .Lemma => level.lemmas
-
-def GameLevel.setComputedInventory (level : GameLevel) :
-    InventoryType → Array InventoryTile → GameLevel
-| .Tactic, v =>     {level with tactics     := {level.tactics     with tiles := v}}
-| .Definition, v => {level with definitions := {level.definitions with tiles := v}}
-| .Lemma, v =>      {level with lemmas      := {level.lemmas      with tiles := v}}

server/GameServer/Options.lean

@@ -1,17 +0,0 @@
-import Lean
-
-/-! This document contains custom options available in the game. -/
-
-/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
-register_option lean4game.showDependencyReasons : Bool := {
-  defValue := false
-  descr := "show reasons for calculated world dependencies."
-}
-
-/-- Let `MakeGame` print the reasons why the worlds depend on each other.
-
-Note: currently unused in favour of setting `set_option trace.debug true`. -/
-register_option lean4game.verbose : Bool := {
-  defValue := false
-  descr := "display more info messages to help developing the game."
-}

server/GameServer/RpcHandlers.lean

@@ -46,8 +46,8 @@ partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) :
   | .bvar i1, .bvar i2 => if i1 == i2 then bij else none
   | .fvar i1, .fvar i2 => bij.insert? i1 i2
   | .mvar _, .mvar _ => bij
-  | .sort _u1, .sort _u2 => bij -- TODO?
-  | .const n1 _ls1, .const n2 _ls2 =>
+  | .sort u1, .sort u2 => bij -- TODO?
+  | .const n1 ls1, .const n2 ls2 =>
     if n1 == n2 then bij else none -- && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
   | .app f1 a1, .app f2 a2 =>
     some bij
@@ -78,7 +78,7 @@ partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) :
   | _, _ => none
 
 /-- Check if each fvar in `patterns` has a matching fvar in `fvars` -/
-def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM (Option FVarBijection) := do
+def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM Bool := do
   -- We iterate through the array backwards hoping that this will find us faster results
   -- TODO: implement backtracking
   let mut bij := initBij
@@ -97,11 +97,11 @@ def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (in
         -- usedFvars := usedFvars.set! (fvars.size - j - 1) true
         bij := bij'.insert pattern.fvarId! fvar.fvarId!
         break
-    if ! bij.forward.contains pattern.fvarId! then return none
+    if ! bij.forward.contains pattern.fvarId! then return false
 
-  if !strict || fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
-  then return some bij
-  else return none
+  if strict then
+    return fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
+  return true
 
 unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
   evalExpr (Array Expr → MessageData)
@@ -122,11 +122,10 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams :
         if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
         then
           let lctx := (← goal.getDecl).lctx
-          if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
+          if ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
           then
-            let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
-            let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
-            let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := lctx, opts := {}}
+            let text := (← evalHintMessage hint.text) hintFVars
+            let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
             let text ← (MessageData.withContext ctx text).toString
             return some { text := text, hidden := hint.hidden }
           else return none

server/GameServer/SaveData.lean

@@ -1,78 +0,0 @@
-import GameServer.EnvExtensions
-
-open Lean Meta Elab Command
-
-
-/-! ## Copy images -/
-
-open IO.FS System FilePath in
-/-- Copies the folder `images/` to `.lake/gamedata/images/` -/
-def copyImages : IO Unit := do
-  let target : FilePath := ".lake" / "gamedata"
-  if ← FilePath.pathExists "images" then
-    for file in ← walkDir "images" do
-      let outFile := target.join file
-      -- create the directories
-      if ← file.isDir then
-        createDirAll outFile
-      else
-        if let some parent := outFile.parent then
-          createDirAll parent
-        -- copy file
-        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
-
-open GameData in
--- TODO: register all of this as ToJson instance?
-def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
-    (inventory : InventoryOverview): CommandElabM Unit := do
-  let game ← getCurGame
-  let env ← getEnv
-  let path := (← IO.currentDir) / gameDataPath
-
-  if ← path.isDir then
-    IO.FS.removeDirAll path
-  IO.FS.createDirAll path
-
-  -- copy the images folder
-  copyImages
-
-  for (worldId, world) in game.worlds.nodes.toArray do
-    for (levelId, level) in world.levels.toArray do
-      IO.FS.writeFile (path / levelFileName worldId levelId) (toString (toJson (level.toInfo env)))
-
-  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 / docFileName inventoryType name) (toString (toJson item))
-
-  IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
-
-open GameData
-
-def loadData (f : System.FilePath) (α : Type) [FromJson α] : IO α := do
-  let str ← IO.FS.readFile f
-  let json ← match Json.parse str with
-  | .ok v => pure v
-  | .error e => throw (IO.userError e)
-  let data ← match fromJson? json with
-  | .ok v => pure v
-  | .error e => throw (IO.userError e)
-  return data
-
-def loadGameData (gameDir : System.FilePath) : IO Game :=
-  loadData (gameDir / gameDataPath / gameFileName) Game
-
-def loadLevelData (gameDir : System.FilePath) (worldId : Name) (levelId : Nat) : IO LevelInfo :=
-  loadData (gameDir / gameDataPath / levelFileName worldId levelId) LevelInfo

server/GameServer/Watchdog.lean

@@ -0,0 +1,158 @@
+/- 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

server/Main.lean

@@ -0,0 +1,18 @@
+import GameServer.FileWorker
+import GameServer.Watchdog
+
+unsafe def main : List String → IO UInt32 := fun args => do
+  let e ← IO.getStderr
+
+  Lean.enableInitializersExecution
+
+  if args[0]? == some "--server" then
+    MyServer.Watchdog.watchdogMain args
+  else if args[0]? == some "--worker" then
+    MyServer.FileWorker.workerMain {}
+  else
+    e.putStrLn s!"Expected `--server` or `--worker`"
+    return 1
+
+
+-- TODO: Potentially it could be useful to pass in the `gameName` via the websocket connection

server/bubblewrap.sh

@@ -1,17 +1,12 @@
 #/bin/bash
 
-# Note: This fails if there is no default toolchain installed
 ELAN_HOME=$(lake env printenv ELAN_HOME)
 
-# $1 : the game directory
-# $2 : the lean4game folder
-# $3 : the gameserver executable
-
 (exec bwrap\
-  --bind $2 /lean4game \
-  --bind $1 /game \
-  --bind $ELAN_HOME /elan \
-  --bind /usr /usr \
+  --ro-bind ../../lean4game /lean4game \
+  --ro-bind ../../$1 /game \
+  --ro-bind $ELAN_HOME /elan \
+  --ro-bind /usr /usr \
   --dev /dev \
   --proc /proc \
   --symlink usr/lib /lib\
@@ -27,6 +22,6 @@ ELAN_HOME=$(lake env printenv ELAN_HOME)
   --unshare-uts  \
   --unshare-cgroup \
   --die-with-parent \
-  --chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \
+  --chdir "/lean4game/server/build/bin/" \
   ./gameserver --server /game
 )

server/import.mjs

@@ -11,7 +11,6 @@ const __filename = fileURLToPath(import.meta.url);
 const __dirname = path.dirname(__filename);
 
 const TOKEN = process.env.LEAN4GAME_GITHUB_TOKEN
-const USERNAME = process.env.LEAN4GAME_GITHUB_USER
 const octokit = new Octokit({
   auth: TOKEN
 })
@@ -42,10 +41,9 @@ async function download(id, url, dest) {
     requestProgress(request({
       url,
       headers: {
-        'accept': 'application/vnd.github+json',
-        'User-Agent': USERNAME,
+        'User-Agent': 'abentkamp',
         'X-GitHub-Api-Version': '2022-11-28',
-        'Authorization': 'Bearer ' + TOKEN
+        'Authorization': 'Bearer '+TOKEN
       }
     }))
     .on('progress', function (state) {
@@ -78,44 +76,35 @@ async function doImport (owner, repo, id) {
       .reduce((acc, cur) => acc.created_at < cur.created_at ? cur : acc)
     artifactId = artifact.id
     const url = artifact.archive_download_url
-    // Make sure the download folder exists
-    if (!fs.existsSync(path.join(__dirname, "..", "games"))){
-      fs.mkdirSync(path.join(__dirname, "..", "games"));
-    }
-    if (!fs.existsSync(path.join(__dirname, "..", "games", "tmp"))){
-      fs.mkdirSync(path.join(__dirname, "..", "games", "tmp"));
+    if (!fs.existsSync("tmp")){
+      fs.mkdirSync("tmp");
     }
     progress[id].output += `Download from ${url}\n`
-    await download(id, url, path.join(__dirname, "..", "games", "tmp", `${owner.toLowerCase()}_${repo.toLowerCase()}_${artifactId}.zip`))
+    await download(id, url, `tmp/artifact_${artifactId}.zip`)
     progress[id].output += `Download finished.\n`
-
-    await runProcess(id, "/bin/bash", [path.join(__dirname, "unpack.sh"), artifactId, owner.toLowerCase(), repo.toLowerCase()], path.join(__dirname, ".."))
-
-
-    // let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
-    // manifest = JSON.parse(manifest);
-    // if (manifest.length !== 1) {
-    //   throw `Unexpected manifest: ${JSON.stringify(manifest)}`
-    // }
-    // manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`]
-    // fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest));
-    // await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`)
-    // // await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`])
-
+    await runProcess(id, "/bin/bash", [`${__dirname}/unpack.sh`, artifactId],".")
+    let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
+    manifest = JSON.parse(manifest);
+    if (manifest.length !== 1) {
+      throw `Unexpected manifest: ${JSON.stringify(manifest)}`
+    }
+    manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`]
+    fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest));
+    await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`)
+    await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`])
     progress[id].done = true
-    progress[id].output += `Done!\n`
-    progress[id].output += `Play the game at: {your website}/#/g/${owner}/${repo}\n`
+    progress[id].output += `Done.\n`
   } catch (e) {
     progress[id].output += `Error: ${e.toString()}\n${e.stack}`
   } finally {
-    // clean-up temp. files
     if (artifactId) {
-      fs.rmSync(path.join(__dirname, "..", "games", "tmp", `${owner}_${repo}_${artifactId}.zip`), {force: true, recursive: false});
-      fs.rmSync(path.join(__dirname, "..", "games", "tmp", `${owner}_${repo}_${artifactId}`), {force: true, recursive: true});
+      fs.rmSync(`tmp/artifact_${artifactId}.zip`, {force: true, recursive: true});
+      fs.rmSync(`tmp/artifact_${artifactId}`, {force: true, recursive: true});
+      fs.rmSync(`tmp/artifact_${artifactId}_inner`, {force: true, recursive: true});
+      fs.rmSync(`tmp/archive_${artifactId}.tar`, {force: true, recursive: true});
     }
     progress[id].done = true
   }
-  await new Promise(resolve => setTimeout(resolve, 10000))
 }
 
 export const importTrigger = (req, res) => {

server/index.mjs

@@ -6,20 +6,25 @@ import * as url from 'url';
 import * as rpc from 'vscode-ws-jsonrpc';
 import * as jsonrpcserver from 'vscode-ws-jsonrpc/server';
 import os from 'os';
-import fs from 'fs';
 import anonymize from 'ip-anonymize';
-import { importTrigger, importStatus } from './import.mjs'
+// import { importTrigger, importStatus } from './import.mjs'
 // import fs from 'fs'
 
 /**
- * Add a game here if the server should keep a queue of pre-loaded games ready at all times.
- *
- * IMPORTANT! Tags here need to be lower case!
 */
-const queueLength = {
-  "g/hhu-adam/robo": 2,
-  "g/hhu-adam/nng4": 5,
-  "g/djvelleman/stg4": 2,
+const games = {
+    "g/hhu-adam/robo": {
+        dir: "Robo",
+        queueLength: 5
+    },
+    "g/hhu-adam/nng4": {
+        dir: "NNG4",
+        queueLength: 5
+    },
+    "g/hhu-adam/nng4-old": {
+        dir: "NNG4-OLD",
+        queueLength: 0
+    }
 }
 
 const __filename = url.fileURLToPath(import.meta.url);
@@ -31,18 +36,11 @@ const PORT = process.env.PORT || 8080;
 
 var router = express.Router();
 
-router.get('/import/status/:owner/:repo', importStatus)
-router.get('/import/trigger/:owner/:repo', importTrigger)
+// router.get('/import/status/:owner/:repo', importStatus)
+// router.get('/import/trigger/:owner/:repo', importTrigger)
 
 const server = app
-  .use(express.static(path.join(__dirname, '..', 'client', 'dist'))) // TODO: add a dist folder from inside the game
-  .use('/data/g/:owner/:repo/*', (req, res, next) => {
-    const owner = req.params.owner;
-    const repo = req.params.repo
-    const filename = req.params[0];
-    req.url = filename;
-    express.static(path.join(getGameDir(owner,repo),".lake","gamedata"))(req, res, next);
-  })
+  .use(express.static(path.join(__dirname, '../client/dist/')))
   .use('/', router)
   .listen(PORT, () => console.log(`Listening on ${PORT}`));
 
@@ -56,61 +54,41 @@ const isDevelopment = environment === 'development'
 /** We keep queues of started Lean Server processes to be ready when a user arrives */
 const queue = {}
 
-function getTag(owner, repo) {
+function tag(owner, repo) {
   return `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
 }
 
-function getGameDir(owner, repo) {
-  owner = owner.toLowerCase()
+function startServerProcess(owner, repo) {
+  let game_dir = (owner == 'local') ?
+    repo : games[tag(owner, repo)]?.dir
+
   if (owner == 'local') {
     if(!isDevelopment) {
       console.error(`No local games in production mode.`)
-      return ""
-    }
-  } else {
-    if(!fs.existsSync(path.join(__dirname, '..', 'games'))) {
-      console.error(`Did not find the following folder: ${path.join(__dirname, '..', 'games')}`)
-      console.error('Did you already import any games?')
-      return ""
+      return
     }
+    // TODO: This test does not work
+    // if (!fs.existsSync(path.join("../", game_dir))) {
+    //   console.error(`Game folder does not exists: ${game_dir}`)
+    //   return
+    // }
   }
 
-  let game_dir = (owner == 'local') ?
-    path.join(__dirname, '..', '..', repo) : // note: here we need `repo` to be case sensitive
-    path.join(__dirname, '..', 'games', `${owner}`, `${repo.toLowerCase()}`)
-
-  if(!fs.existsSync(game_dir)) {
-    console.error(`Game '${game_dir}' does not exist!`)
-    return ""
+  if (!game_dir) {
+    console.error(`Unknown game: ${tag(owner, repo)}`)
+    return
   }
 
-  return game_dir;
-}
-
-function startServerProcess(owner, repo) {
-
-  let game_dir = getGameDir(owner, repo)
-  if (!game_dir) return;
-
   let serverProcess
   if (isDevelopment) {
-    let args = ["--server", game_dir]
-    let binDir = path.join(game_dir, ".lake", "packages", "GameServer", "server", ".lake", "build", "bin")
-    // Note: `cwd` is important to be the `bin` directory as `Watchdog` calls `./gameserver` again
-    if (fs.existsSync(binDir)) {
-      // Try to use the game's own copy of `gameserver`.
-      serverProcess = cp.spawn("./gameserver", args, { cwd: binDir })
-    } else {
-      // If the game is built with `-Klean4game.local` there is no copy in the lake packages.
-      serverProcess = cp.spawn("./gameserver", args,
-        { cwd: path.join(__dirname, "..", "server", ".lake", "build", "bin") })
-    }
+    let args = ["--server", path.join("../../../../", game_dir)]
+    serverProcess = cp.spawn("./gameserver", args,
+        { cwd: path.join(__dirname, "./build/bin/") })
   } else {
     serverProcess =  cp.spawn("./bubblewrap.sh",
-      [ game_dir, path.join(__dirname, '..')],
+      [game_dir],
       { cwd: __dirname })
   }
-
   serverProcess.on('error', error =>
     console.error(`Launching Lean Server failed: ${error}`)
   )
@@ -123,21 +101,15 @@ function startServerProcess(owner, repo) {
 }
 
 /** start Lean Server processes to refill the queue */
-function fillQueue(tag) {
-  while (queue[tag].length < queueLength[tag]) {
-    let serverProcess
-    serverProcess = startServerProcess(tag)
-    if (serverProcess == null) {
-      console.error('serverProcess was undefined/null')
-      return
+function fillQueue(owner, repo) {
+    while (queue[tag(owner, repo)].length < games[tag(owner, repo)].queueLength) {
+      const serverProcess = startServerProcess(tag(owner, repo))
+      queue[tag(owner, repo)].push(serverProcess)
     }
-    queue[tag].push(serverProcess)
-  }
 }
 
-// // TODO: We disabled queue for now
 // if (!isDevelopment) { // Don't use queue in development
-//   for (let tag in queueLength) {
+//   for (let tag in games) {
 //     queue[tag] = []
 //     fillQueue(tag)
 //   }
@@ -150,21 +122,19 @@ wss.addListener("connection", function(ws, req) {
     if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; }
     const owner = reRes[1]
     const repo = reRes[2]
+    // const tag = `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
 
-    const tag = getTag(owner, repo)
+    // // TODO
+    // if (isDevelopment && process.env.DEV_CONTAINER) {
+    //     tag = `g/local/game`
+    // }
 
-    let ps
-    if (!queue[tag] || queue[tag].length == 0) {
-      ps = startServerProcess(owner, repo)
+    let ps;
+    if (!queue[tag(owner, repo)] || queue[tag(owner, repo)].length == 0) {
+        ps = startServerProcess(owner, repo)
     } else {
-        console.info('Got process from the queue')
-        ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately
-        fillQueue(tag)
-    }
-
-    if (ps == null) {
-      console.error('server process is undefined/null')
-      return
+        ps = queue[tag(owner, repo)].shift() // Pick the first Lean process; it's likely to be ready immediately
+        fillQueue(owner, repo)
     }
 
     socketCounter += 1;
@@ -177,14 +147,14 @@ wss.addListener("connection", function(ws, req) {
         onClose: (cb) => { ws.on("close", cb) },
         send: (data, cb) => { ws.send(data,cb) }
     }
-    const reader = new rpc.WebSocketMessageReader(socket)
-    const writer = new rpc.WebSocketMessageWriter(socket)
+    const reader = new rpc.WebSocketMessageReader(socket);
+    const writer = new rpc.WebSocketMessageWriter(socket);
     const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
-    const serverConnection = jsonrpcserver.createProcessStreamConnection(ps)
+    const serverConnection = jsonrpcserver.createProcessStreamConnection(ps);
     socketConnection.forward(serverConnection, message => {
         if (isDevelopment) {console.log(`CLIENT: ${JSON.stringify(message)}`)}
         return message;
-    })
+    });
     serverConnection.forward(socketConnection, message => {
       if (isDevelopment) {console.log(`SERVER: ${JSON.stringify(message)}`)}
         return message;
@@ -195,9 +165,9 @@ wss.addListener("connection", function(ws, req) {
 
     ws.on('close', () => {
       console.log(`[${new Date()}] Socket closed - ${ip}`)
-      socketCounter -= 1
+      socketCounter -= 1;
     })
 
-    socketConnection.onClose(() => serverConnection.dispose())
-    serverConnection.onClose(() => socketConnection.dispose())
+    socketConnection.onClose(() => serverConnection.dispose());
+    serverConnection.onClose(() => socketConnection.dispose());
 })

server/lake-manifest.json

@@ -1,14 +1,4 @@
-{"version": 7,
- "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/leanprover/std4.git",
-   "type": "git",
-   "subDir": null,
-   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
-   "name": "std",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
- "name": "GameServer",
- "lakeDir": ".lake"}
+{"version": 6,
+ "packagesDir": "lake-packages",
+ "packages": [],
+ "name": "GameServer"}

server/lakefile.lean

@@ -3,25 +3,10 @@ open Lake DSL
 
 package GameServer
 
--- Using this assumes that each dependency has a tag of the form `v4.X.0`.
-def leanVersion : String := s!"v{Lean.versionString}"
-
-require std from git "https://github.com/leanprover/std4.git" @ leanVersion
-
 lean_lib GameServer
 
 @[default_target]
 lean_exe gameserver {
-  root := `GameServer
+  root := `Main
   supportInterpreter := true
 }
-
-/--
-When a package depending on GameServer updates its dependencies,
-build the `gameserver` executable.
--/
-post_update pkg do
-  let rootPkg ← getRootPackage
-  if rootPkg.name = pkg.name then
-    return -- do not run in GameServer itself
-  discard <| runBuild gameserver.build >>= (·.await)

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0
+leanprover/lean4:v4.1.0

server/unpack.sh

@@ -0,0 +1,13 @@
+#/bin/bash
+
+ARTIFACT_ID=$1
+
+echo "Unpacking ZIP."
+unzip -o tmp/artifact_${ARTIFACT_ID}.zip -d tmp/artifact_${ARTIFACT_ID}
+echo "Unpacking TAR."
+for f in tmp/artifact_${ARTIFACT_ID}/* #Should only be one file
+do
+  echo "Unpacking $f"
+  mkdir tmp/artifact_${ARTIFACT_ID}_inner
+  tar -xvf $f -C tmp/artifact_${ARTIFACT_ID}_inner
+done

tsconfig.json

@@ -12,5 +12,5 @@
     "experimentalDecorators": true,
     "allowSyntheticDefaultImports": true,
   },
-  "exclude": ["server", "relay"]
+  "exclude": ["server"]
 }

vite.config.ts

@@ -1,54 +0,0 @@
-import { defineConfig } from 'vite'
-import react from '@vitejs/plugin-react-swc'
-import { viteStaticCopy } from 'vite-plugin-static-copy'
-import svgr from "vite-plugin-svgr"
-
-// https://vitejs.dev/config/
-export default defineConfig({
-  //root: 'client/src',
-  build: {
-    // Relative to the root
-    // Note: This has to match the path in `relay/index.mjs`
-    outDir: 'client/dist',
-  },
-  plugins: [
-    react(),
-    svgr({
-      svgrOptions: {
-        // svgr options
-      },
-    }),
-    viteStaticCopy({
-      targets: [
-        {
-          src: 'node_modules/@leanprover/infoview/dist/*.production.min.js',
-          dest: '.'
-        }
-      ]
-    })
-  ],
-  publicDir: "client/public",
-  optimizeDeps: {
-    exclude: ['games']
-  },
-  server: {
-    port: 3000,
-    proxy: {
-      '/websocket': {
-        target: 'ws://localhost:8080',
-        ws: true
-      },
-      '/import': {
-        target: 'http://localhost:8080',
-      },
-      '/data': {
-        target: 'http://localhost:8080',
-      },
-    }
-  },
-  resolve: {
-    alias: {
-      path: "path-browserify",
-    },
-  },
-})

webpack.config.js

@@ -0,0 +1,106 @@
+const path = require("path");
+const webpack = require('webpack');
+const ReactRefreshWebpackPlugin = require('@pmmmwh/react-refresh-webpack-plugin');
+const WebpackShellPluginNext = require('webpack-shell-plugin-next');
+
+module.exports = env => {
+
+  const single_game = process.env.LEAN4GAME_SINGLE_GAME
+
+
+  const environment = process.env.NODE_ENV
+  const isDevelopment = environment === 'development'
+
+  const babelOptions = {
+      presets: ['@babel/preset-env', '@babel/preset-react', '@babel/preset-typescript'],
+    plugins: [
+      isDevelopment && require.resolve('react-refresh/babel'),
+    ].filter(Boolean),
+  };
+
+  global.$RefreshReg$ = () => {};
+  global.$RefreshSig$ = () => () => {};
+
+  return {
+    entry: [single_game ? "./client/src/index_local.tsx" : "./client/src/index.tsx"],
+    mode: isDevelopment ? 'development' : 'production',
+    module: {
+      rules: [
+        {
+          test: /\.(js|jsx)$/,
+          exclude: [/server/, /node_modules/],
+          use: [{
+            loader: require.resolve('babel-loader'),
+            options: babelOptions,
+          }]
+        },
+        {
+          test: /\.tsx?$/,
+          use: [{
+            loader: 'ts-loader',
+            options: { allowTsInNodeModules: true }
+          }],
+          // exclude: /node_modules(?!\/(lean4web|lean4|lean4-infoview))/,
+          // Allow .ts imports from node_modules/lean4web and node_modules/lean4
+        },
+        {
+          test: /\.css$/,
+          use: ["style-loader", "css-loader"]
+        },
+        {
+          test: /\.(jpg|png)$/,
+          use: {
+            loader: 'file-loader',
+          },
+        },
+      ]
+    },
+    resolve: {
+      extensions: ["*", ".js", ".jsx", ".tsx", ".ts"],
+      fallback: {
+        "http": require.resolve("stream-http") ,
+        "path": require.resolve("path-browserify")
+      },
+    },
+    output: {
+      path: path.resolve(__dirname, "client/dist/"),
+      filename: "bundle.js",
+    },
+    devServer: {
+      proxy: {
+        '/websocket': {
+           target: 'ws://localhost:8080',
+           ws: true
+        },
+        '/import': {
+          target: 'http://localhost:3000',
+          router: () => 'http://localhost:8080',
+        },
+      },
+      static: path.join(__dirname, 'client/public/'),
+      port: 3000,
+      hot: true,
+    },
+    devtool: "source-map",
+    plugins: [
+      !isDevelopment && new WebpackShellPluginNext({
+        onBuildEnd:{
+          scripts: [
+            // It's hard to set up webpack to copy the index.html correctly,
+            // so we copy it explicitly after every build:
+            'cp client/public/index.html client/dist/',
+            // Similarly, I haven't been able to load `onigasm.wasm` properly:
+            'cp client/public/onigasm.wasm client/dist/',],
+          blocking: false,
+          parallel: true
+        }
+      }),
+      isDevelopment && new ReactRefreshWebpackPlugin(),
+    ].filter(Boolean),
+
+    // Webpack is not happy about the dynamically loaded widget code in the function
+    // `dynamicallyLoadComponent` in `infoview/userWidget.tsx`. If we want to support
+    // dynamically loaded widget code, we need to make sure that the files are available.
+    ignoreWarnings: [/Critical dependency: the request of a dependency is an expression/]
+  };
+}