work on network interruption errors

improve loading of inventory doc popups #138
2023-10-27 21:02:20 +02:00 · 2023-10-27 18:48:02 +02:00
44 changed files with 1337 additions and 2782 deletions
@@ -0,0 +1 @@
+LEAN4GAME_SINGLE_GAME=false
@@ -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
@@ -1,6 +1,4 @@
 node_modules
-games/
 client/dist
-games/
-server/.lake
-**/.DS_Store
+server/build
+**/lake-packages/
@@ -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
@@ -2,13 +2,15 @@

 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:
-
-* 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)
+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).

 ### Publishing a Game

@@ -32,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/)
-of Kevin Buzzard and Mohammad Pedramfar.
-The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
@@ -33,7 +33,7 @@
      </p>
    </div>
  </noscript>
-  <script type="module" src="/client/src/index.tsx"></script>
+  <script src="bundle.js"></script>
 </body>

 </html>
@@ -10,7 +10,6 @@ import './css/reset.css';
 import './css/app.css';
 import { MobileContext } from './components/infoview/context';
 import { useWindowDimensions } from './window_width';
-import { connection } from './connection';

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

@@ -20,10 +19,6 @@ function App() {
  const {width, height} = useWindowDimensions()
  const [mobile, setMobile] = React.useState(width < 800)

-  React.useEffect(() => {
-    connection.startLeanClient(gameId);
-  }, [gameId])
-
  return (
    <div className="app">
      <GameIdContext.Provider value={gameId}>
@@ -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';
@@ -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> = []
-      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 },
-          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">
@@ -533,7 +541,7 @@ export function TypewriterInterface({props}) {
                }
              </div>
            }
-          </> : <CircularProgress variant="determinate" value={loadingProgress} />
+          </> : <CircularProgress />
        }
      </div>
    </div>
@@ -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) => {
@@ -6,6 +6,7 @@ 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';
@@ -114,16 +115,32 @@ function InventoryItem({name, displayName, locked, disabled, newly, showDoc, ena
  return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>{icon} {displayName}</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}) {
  const gameId = React.useContext(GameIdContext)
  const doc = useLoadDocQuery({game: gameId, type: type, name: name})

  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>
 }

@@ -8,7 +8,6 @@ import '@fontsource/roboto/700.css';

 import '../css/landing_page.css'
 import coverRobo from '../assets/covers/formaloversum.png'
-import coverNNG from '../assets/covers/nng.png'
 import bgImage from '../assets/bg.jpg'

 import Markdown from './markdown';
@@ -114,18 +113,7 @@ function LandingPage() {
 learning the basics about theorem proving in Lean.

 This is a good first introduction to Lean!"
-        worlds="8"
-        levels="67"
-        image={coverNNG}
-        language="English"
-        />
-
-      <GameTile
-        title="Set Theory Game"
-        gameId="g/djvelleman/STG4"
-        intro="A game about set theory"
-        description=""
-        worlds="5"
+        worlds="4"
        levels="30"
        language="English"
        />
@@ -48,6 +48,7 @@ function Level() {
  const params = useParams()
  const levelId = parseInt(params.levelId)
  const worldId = params.worldId
+  // useLoadWorldFiles(worldId)

  const [impressum, setImpressum] = React.useState(false)

@@ -236,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}))
  }
@@ -253,30 +252,30 @@ 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
@@ -295,28 +294,31 @@ function PlayableLevel({impressum, setImpressum}) {
      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 {
@@ -334,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) {
-      // 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
@@ -362,33 +396,6 @@ function PlayableLevel({impressum, setImpressum}) {
    }
  }, [showHelp])

-  // Effect when command line mode gets enabled
-  useEffect(() => {
-    if (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])
-
  return <>
    <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
    <DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
@@ -482,33 +489,9 @@ function Introduction({impressum, setImpressum}) {
          <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)
@@ -603,18 +586,19 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
      if (!model) {
        model = monaco.editor.createModel(initialCode, 'lean4', uri)
      }
-      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
-      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
-      editor.setModel(model)
-      if (initialSelections) {
-        console.debug("Initial Selection: ", initialSelections)
-        // BUG: Somehow I get an `invalid arguments` bug here
-        // editor.setSelections(initialSelections)
-      }
+      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();
+        return () => {
+          editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
+          model.dispose(); }
      }
    }
  }, [editor, levelId, connection, leanClientStarted])
@@ -624,16 +608,42 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
    if (editor && leanClientStarted) {

      let model = monaco.editor.getModel(uri)
-      infoviewApi.serverRestarted(leanClient.initializeResult)
+      if (model) {
+        infoviewApi.serverRestarted(leanClient.initializeResult)

-      infoProvider.openPreview(editor, infoviewApi)
+        infoProvider.openPreview(editor, infoviewApi)

-      const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
-      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+        const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
+        const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)

-      return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
+        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])
+}
@@ -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%;
@@ -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;
@@ -1,43 +1,31 @@
-import * as React from 'react'
-import { createRoot } from 'react-dom/client'
-import App from './app'
+import * as React from 'react';
+import { createRoot } from 'react-dom/client';
+import App from './app';
 import { ConnectionContext, connection } from './connection'
-import { store } from './state/store'
-import { Provider } from 'react-redux'
-import type { RouteObject } from "react-router"
-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 { monacoSetup } from 'lean4web/client/src/monacoSetup'
-
+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()

-
-// 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 />,
-}
-
 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",
@@ -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>
+);
@@ -2,6 +2,7 @@
 * @fileOverview Define API of the server-client communication
 */
 import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react'
+import { Connection } from '../connection'

 export interface GameInfo {
  title: null|string,
@@ -56,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 + "/api" }),
+  baseQuery: customBaseQuery,
  endpoints: (builder) => ({
    getGameInfo: builder.query<GameInfo, {game: string}>({
-      query: ({game}) => `${game}/game`,
+      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}`,
+      query: ({game, world, level}) => {return {game, method: "loadLevel", params: {world, level}}},
    }),
    loadInventoryOverview: builder.query<InventoryOverview, {game: string}>({
-      query: ({game}) => `${game}/inventory`,
+      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}`,
+      query: ({game, name, type}) => {return {game, method: "loadDoc", params: {name, type}}},
    }),
  }),
 })
@@ -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.

@@ -243,14 +243,6 @@ 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.

-## 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)
-
 ## Further Notes

 Here are some random further things you should consider designing a new game:
@@ -1,30 +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!
@@ -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,16 +73,16 @@ 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
 ```
@@ -96,7 +93,7 @@ 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
@@ -109,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`.
@@ -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.
@@ -1,53 +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: run
-  ```
-  lake update -R
-  lake build
-  ```
-  in your game folder.
-
-  * Additionally, if you have a local copy of the server `lean4game`,
-    you should update this one to the matching version, too:
-    ```
-    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 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.)
@@ -4,10 +4,8 @@ module.exports = {
    name   : "lean4game",
    script : "server/index.mjs",
    env: {
-      LEAN4GAME_GITHUB_USER: "",
-      LEAN4GAME_GITHUB_TOKEN: "",
-      NODE_ENV: "production",
-      PORT: 8002
+       NODE_ENV: "production",
+       PORT: 8002
    },
  }]
 }
@@ -1,10 +0,0 @@
-/// <reference types="vite/client" />
-
-interface ImportMetaEnv {
-  readonly VITE_LEAN4GAME_SINGLE: string
-  // more env variables...
-}
-
-interface ImportMeta {
-  readonly env: ImportMetaEnv
-}
@@ -1,7 +1,6 @@
 {
  "name": "lean4-game",
  "version": "0.1.0",
-  "type": "module",
  "private": true,
  "homepage": ".",
  "dependencies": {
@@ -16,7 +15,6 @@
    "@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",
@@ -37,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 && 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 server/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": [
@@ -1,3 +1,3 @@
-build/
-games/
-.lake
+build
+adam
+nng
@@ -644,44 +644,6 @@ elab "Template" tacs:tacticSeq : tactic => do

 /-! # Make Game -/

-#eval IO.FS.createDirAll ".lake/gamedata/"
-
-- TODO: register all of this as ToJson instance?
-def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit:= do
-  let game ← getCurGame
-  let env ← getEnv
-  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
-
-  if ← path.isDir then
-    IO.FS.removeDirAll path
-  IO.FS.createDirAll path
-
-  for (worldId, world) in game.worlds.nodes.toArray do
-    for (levelId, level) in world.levels.toArray do
-      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
-
-  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
-
-  for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
-    for name in allItemsByType.findD inventoryType {} do
-      let some item ← getInventoryItem? name inventoryType
-        | throwError "Expected item to exist: {name}"
-      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
-
-  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
-    (allItemsByType.findD type {}).toArray.mapM (fun name => do
-      let some item ← getInventoryItem? name type
-        | throwError "Expected item to exist: {name}"
-      return item.toTile)
-  let inventory : InventoryOverview := {
-    lemmas := ← getTiles .Lemma
-    tactics := ← getTiles .Tactic
-    definitions := ← getTiles .Definition
-    lemmaTab := none
-  }
-  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))
-
-
 def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
 | .Tactic => level.tactics
 | .Definition => level.definitions
@@ -961,7 +923,6 @@ elab "MakeGame" : command => do
  -- 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

@@ -1091,9 +1052,6 @@ elab "MakeGame" : command => do

        modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
          return level.setComputedInventory inventoryType itemsArray
-    allItemsByType := allItemsByType.insert inventoryType allItems
-
-  saveGameData allItemsByType

 /-! # Debugging tools -/

@@ -108,12 +108,6 @@ structure InventoryTile where
  hidden := false
 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 :
@@ -141,12 +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
+

 /-! ## Environment extensions for game specification -/

@@ -267,55 +256,6 @@ structure GameLevel where
  template: Option String := none
  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
-  displayName : Option String
-  statementName : Option String
-  template : 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
-    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
-  }

 /-! ## World -/

@@ -358,13 +298,6 @@ structure Game where
  worlds : Graph Name World := default
 deriving Inhabited, ToJson

-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
-
 /-! ## Game environment extension -/

 def HashMap.merge [BEq α] [Hashable α] (old : HashMap α β) (new : HashMap α β) (merge : β → β → β) :
@@ -1,7 +1,6 @@
 /- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/
 import Lean.Server.FileWorker
 import GameServer.Game
-import GameServer.ImportModules

 namespace MyModule
 open Lean
@@ -413,7 +412,7 @@ section Initialization
    -- Set the search path
    Lean.searchPathRef.set paths

-    let env ← importModules' #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }]
+    let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
    -- return (env, paths)

    -- use empty header
@@ -497,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

@@ -574,7 +573,7 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
    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
@@ -25,6 +25,53 @@ open Lsp
 open JsonRpc
 open IO

+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
+
+/--
+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 LoadTemplateParams where
+--   world : Name
+--   level : Nat
+--   deriving ToJson, FromJson
+
 structure DidOpenLevelParams where
  uri : String
  gameDir : String
@@ -44,6 +91,11 @@ structure DidOpenLevelParams where
  statementName : Name
  deriving ToJson, FromJson

+structure LoadDocParams where
+  name : Name
+  type : InventoryType
+deriving ToJson, FromJson
+
 structure SetInventoryParams where
  inventory : Array String
  difficulty : Nat
@@ -79,10 +131,86 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
    }
  }

+
 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
@@ -93,6 +221,30 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := 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

@@ -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
@@ -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,10 +122,9 @@ 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 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 }
@@ -1,9 +1,5 @@
 import GameServer.FileWorker
 import GameServer.Watchdog
-import GameServer.Commands
-
-- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`
-- should we have a different solution?

 unsafe def main : List String → IO UInt32 := fun args => do
  let e ← IO.getStderr
@@ -2,13 +2,11 @@

 ELAN_HOME=$(lake env printenv ELAN_HOME)

-
-
 (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\
@@ -24,6 +22,6 @@ ELAN_HOME=$(lake env printenv ELAN_HOME)
  --unshare-uts  \
  --unshare-cgroup \
  --die-with-parent \
-  --chdir "/lean4game/server/.lake/build/bin/" \
+  --chdir "/lean4game/server/build/bin/" \
  ./gameserver --server /game
 )
@@ -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,45 +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(`${__dirname}/../games`)){
-      fs.mkdirSync(`${__dirname}/../games`);
-    }
-    if (!fs.existsSync(`${__dirname}/../games/tmp`)){
-      fs.mkdirSync(`${__dirname}/../games/tmp`);
+    if (!fs.existsSync("tmp")){
+      fs.mkdirSync("tmp");
    }
    progress[id].output += `Download from ${url}\n`
-    await download(id, url, `${__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", [`${__dirname}/unpack.sh`, artifactId, owner.toLowerCase(), repo.toLowerCase()], `${__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 {
-    // if (artifactId) {
-    //   // 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});
-    // }
+    if (artifactId) {
+      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) => {
@@ -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,34 +36,8 @@ const PORT = process.env.PORT || 8080;

 var router = express.Router();

-router.get('/import/status/:owner/:repo', importStatus)
-router.get('/import/trigger/:owner/:repo', importTrigger)
-
-function loadJson(req, filename) {
-  const owner = req.params.owner;
-  const repo = req.params.repo
-  return JSON.parse(fs.readFileSync(path.join(getGameDir(owner,repo),".lake","gamedata",filename)))
-}
-
-router.get("/api/g/:owner/:repo/game", (req, res) => {
-  res.send(loadJson(req, `game.json`));
-});
-
-router.get("/api/g/:owner/:repo/inventory", (req, res) => {
-  res.send(loadJson(req, `inventory.json`));
-});
-
-router.get("/api/g/:owner/:repo/level/:world/:level", (req, res) => {
-  const world = req.params.world;
-  const level = req.params.level;
-  res.send(loadJson(req, `level__${world}__${level}.json`));
-});
-
-router.get("/api/g/:owner/:repo/doc/:type/:name", (req, res) => {
-  const type = req.params.type;
-  const name = req.params.name;
-  res.send(loadJson(req, `doc__${type}__${name}.json`));
-});
+// 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/')))
@@ -75,50 +54,39 @@ 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
-    }
+    // 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!`)
+  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 args = ["--server", path.join("../../../../", game_dir)]
    serverProcess = cp.spawn("./gameserver", args,
-        { cwd: path.join(__dirname, "./.lake/build/bin/") })
+        { 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 =>
@@ -133,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)
 //   }
@@ -160,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;
@@ -187,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;
@@ -205,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());
 })
@@ -1,14 +1,4 @@
-{"version": 7,
- "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/leanprover/std4.git",
-   "type": "git",
-   "subDir": null,
-   "rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50",
-   "name": "std",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0-rc2",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
- "name": "GameServer",
- "lakeDir": ".lake"}
+{"version": 6,
+ "packagesDir": "lake-packages",
+ "packages": [],
+ "name": "GameServer"}
@@ -3,11 +3,6 @@ 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]
@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc2
+leanprover/lean4:v4.1.0
@@ -1,30 +1,13 @@
 #/bin/bash

 ARTIFACT_ID=$1
-OWNER=$2
-REPO=$3
-
-# mkdir -p games
-cd games
-pwd
-# 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
+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"
-  #tar -xvzf $f -C games/${OWNER}/${REPO}
-  unzip -q -o $f -d ${OWNER}/${REPO}
+  mkdir tmp/artifact_${ARTIFACT_ID}_inner
+  tar -xvf $f -C tmp/artifact_${ARTIFACT_ID}_inner
 done
@@ -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 `server/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',
-      },
-      '/api': {
-        target: 'http://localhost:8080',
-      },
-    }
-  },
-  resolve: {
-    alias: {
-      path: "path-browserify",
-    },
-  },
-})
@@ -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/]
+  };
+}
Author	SHA1	Message	Date
joneugster	bea342b2c7	work on network interruption errors	2023-10-27 21:02:20 +02:00
joneugster	940663f640	improve loading of inventory doc popups #138	2023-10-27 18:48:02 +02:00