work on network interruption errors

.env

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

.github/workflows/build.yml

@@ -5,17 +5,7 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-      - name: install elan
+      - uses: actions/checkout@v3
-        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/setup-node@v3
-      - name: print lean and lake versions
-        run: |
-          lean --version
-          lake --version
       - run: npm install
       - run: npm run build

.gitignore

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

NOTES.md

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

README.md

@@ -2,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:
+Please follow the tutorial [Creating a Game](doc/create_game.md).
-
+In particular step 5 thereof explains [How to Run Games Locally](doc/running_locally.md).
-* Step 5: [How to Run Games Locally](doc/running_locally.md)
-* Step 7: [How to Update an existing Game](doc/update_game.md)
-* Step 8: [How to Publishing a Game](doc/publish_game.md)
 
 ### Publishing a Game
 
@@ -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).

client/public/index.html

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

client/src/app.tsx

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

client/src/components/infoview/main.tsx

@@ -1,6 +1,7 @@
 /* Partly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/main.tsx */
 
 import * as React from 'react';
+import {useEffect} from 'react';
 import type { DidCloseTextDocumentParams, DidChangeTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol';
 
 import 'tachyons/css/tachyons.css';
@@ -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 { showHelp, setShowHelp } = React.useContext(DeletedChatContext)
-  const { setDeletedChat, 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})
+  // rpc session
-
+  // editor, model or uri might be null if connection is broken
-  /** Delete all proof lines starting from a given line.
+  const rpcSess = useRpcSessionAtPos({uri: editor?.getModel()?.uri?.toString() ?? '', line: 0, character: 0})
-  * 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()
-    }
-  }
 
   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.
+  // Scroll to the end of the proof if it is updated.
-   React.useEffect(() => {
+  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>

client/src/components/infoview/typewriter.tsx

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

client/src/components/inventory.tsx

@@ -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>
+      <DocContent doc={doc} />
-    <p><code>{doc.data?.statement}</code></p>
-    {/* <code>docstring: {doc.data?.docstring}</code> */}
-    <Markdown>{doc.data?.content}</Markdown>
   </div>
 }
 

client/src/components/landing_page.tsx

@@ -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"
+        worlds="4"
-        levels="67"
-        image={coverNNG}
-        language="English"
-        />
-
-      <GameTile
-        title="Set Theory Game"
-        gameId="g/djvelleman/STG4"
-        intro="A game about set theory"
-        description=""
-        worlds="5"
         levels="30"
         language="English"
         />

client/src/components/level.tsx

@@ -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
+  // /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside
-   * `TypewriterInterface`.
+  //  * `TypewriterInterface`.
-   */
+  //  */
-  const handleUndo = () => {
+  // const handleUndo = () => {
-    const endPos = editor.getModel().getFullModelRange().getEndPosition()
+  //   const endPos = editor.getModel().getFullModelRange().getEndPosition()
-    let range
+  //   let range
-    console.log(endPos.column)
+  //   console.log(endPos.column)
-    if (endPos.column === 1) {
+  //   if (endPos.column === 1) {
-      range = monaco.Selection.fromPositions(
+  //     range = monaco.Selection.fromPositions(
-        new monaco.Position(endPos.lineNumber - 1, 1),
+  //       new monaco.Position(endPos.lineNumber - 1, 1),
-        endPos
+  //       endPos
-      )
+  //     )
-    } else {
+  //   } else {
-      range = monaco.Selection.fromPositions(
+  //     range = monaco.Selection.fromPositions(
-        new monaco.Position(endPos.lineNumber, 1),
+  //       new monaco.Position(endPos.lineNumber, 1),
-        endPos
+  //       endPos
-      )
+  //     )
-    }
+  //   }
-    editor.executeEdits("undo-button", [{
+  //   editor.executeEdits("undo-button", [{
-      range,
+  //     range,
-      text: "",
+  //     text: "",
-      forceMoveMarkers: false
+  //     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. code: ${code}`)
-        // console.log(`insert. join: ${code.join('')}`)
+          // console.log(`insert. join: ${code.join('')}`)
-        // console.log(`insert. trim: ${code.join('').trim()}`)
+          // console.log(`insert. trim: ${code.join('').trim()}`)
-        // console.log(`insert. length: ${code.join('').trim().length}`)
+          // console.log(`insert. length: ${code.join('').trim().length}`)
-        // console.log(`insert. range: ${editor.getModel().getFullModelRange()}`)
+          // console.log(`insert. range: ${editor.getModel().getFullModelRange()}`)
 
 
-        // TODO: It does seem that the template is always indented by spaces.
+          // TODO: It does seem that the template is always indented by spaces.
-        // This is a hack, assuming there are exactly two.
+          // This is a hack, assuming there are exactly two.
-        if (!code.join('').trim().length) {
+          if (!code.join('').trim().length) {
-          console.debug(`inserting template:\n${level.data.template}`)
+            console.debug(`inserting template:\n${level.data.template}`)
-          // TODO: This does not work! HERE
+            // TODO: This does not work! HERE
-          // Probably overwritten by a query to the server
+            // Probably overwritten by a query to the server
-          editor.executeEdits("template-writer", [{
+            editor.executeEdits("template-writer", [{
-            range: editor.getModel().getFullModelRange(),
+              range: model.getFullModelRange(),
-            text: level.data.template + `\n`,
+              text: level.data.template + `\n`,
-            forceMoveMarkers: true
+              forceMoveMarkers: true
-          }])
+            }])
-        } else {
+          } else {
-          console.debug(`not inserting template.`)
+            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) {
+    if (editor) {
-      // Delete last input attempt from command line
+      let model = editor.getModel()
-      editor.executeEdits("typewriter", [{
+      if (model) {
-        range: editor.getSelection(),
+        if (typewriterMode) {
-        text: "",
+          // typewriter gets enabled
-        forceMoveMarkers: false
+          let code = model.getLinesContent().filter(line => line.trim())
-      }]);
+          editor.executeEdits("typewriter", [{
-      editor.focus()
+            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()))
+      if (model) { // in case of broken pipe, this remains null
-      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
+        model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
-      editor.setModel(model)
+        editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
-      if (initialSelections) {
+        editor.setModel(model)
-        console.debug("Initial Selection: ", initialSelections)
+        if (initialSelections) {
-        // BUG: Somehow I get an `invalid arguments` bug here
+          console.debug("Initial Selection: ", initialSelections)
-        // editor.setSelections(initialSelections)
+          // BUG: Somehow I get an `invalid arguments` bug here
-      }
+          // editor.setSelections(initialSelections)
+        }
 
-      return () => {
+        return () => {
-        editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
+          editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
-        model.dispose();
+          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 taskGutter = new LeanTaskGutter(infoProvider.client, editor)
-      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, 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])
+}

client/src/css/app.css

@@ -42,6 +42,12 @@ body {
   border-radius: .3em;
 }
 
+
+/* Hide monaco editor notifications */
+.monaco-workbench > .notifications-toasts.visible {
+  display: none !important;
+}
+
 .loading {
   margin: auto;
   height: 100%;

client/src/css/landing_page.css

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

client/src/index.tsx

@@ -1,43 +1,31 @@
-import * as React from 'react'
+import * as React from 'react';
-import { createRoot } from 'react-dom/client'
+import { createRoot } from 'react-dom/client';
-import App from './app'
+import App from './app';
 import { ConnectionContext, connection } from './connection'
-import { store } from './state/store'
+import { store } from './state/store';
-import { Provider } from 'react-redux'
+import { Provider } from 'react-redux';
-import type { RouteObject } from "react-router"
+import {
-import { createHashRouter, RouterProvider, Route, redirect } from "react-router-dom"
+  createHashRouter,
-import ErrorPage from './components/error_page'
+  RouterProvider,
-import Welcome from './components/welcome'
+  Route,
-import LandingPage from './components/landing_page'
+} from "react-router-dom";
-import Level from './components/level'
+import ErrorPage from './components/error_page';
-import { monacoSetup } from 'lean4web/client/src/monacoSetup'
+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: "/",
-    path: "/game/nng",
+    element: <LandingPage />,
-    loader: () => redirect("/g/hhu-adam/NNG4")
   },
   {
-    // For backwards compatibility
+    path: "/game/nng",
-    path: "/g/hhu-adam/NNG4",
+    loader: () => redirect("/g/hhu-adam/NNG4")
-    loader: () => redirect("/g/leanprover-community/NNG4")
   },
   {
     path: "/g/:owner/:repo",

client/src/index_local.tsx

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

client/src/state/api.ts

@@ -2,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}}},
     }),
   }),
 })

doc/create_game.md

@@ -4,7 +4,7 @@ This tutorial walks you through creating a new game for lean4. It covers from wr
 
 ## 1. Create the project
 
-1. Use the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
+1. Use the [NNG template](https://github.com/hhu-adam/NNG4) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
 2. Clone the game repo.
 3. Call `lake update && lake exe cache get && lake build` to build the Lean project.
 
@@ -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:

doc/publish_game.md

@@ -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!

doc/running_locally.md

@@ -4,15 +4,13 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
 
 There are several options to play a game locally:
 
-1. VSCode Dev Container: needs `docker` installed on your machine
+- VSCode Dev Container: needs `docker` installed on your machine
-2. Codespaces: Needs active internet connection and computing time is limited.
+- Codespaces: Needs active internet connection and computing time is limited.
-3. Gitpod: does not work yet (Is that true?)
+- Gitpod: does not work yet (I that true?)
-4. Manual installation: Needs `npm` installed on your system
+- 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
+git clone https://github.com/hhu-adam/NNG4.git
-# or: git clone git@github.com:hhu-adam/GameSkeleton.git
+# or: git clone git@github.com:hhu-adam/NNG4.git
 ```
 
 Download dependencies and build the game:
 ```bash
-cd GameSkeleton
+cd NNG4
-lake update -R
+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
+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`.
-`lake build` will then directly use this modified copy to build your game.

doc/server.md

@@ -1,28 +0,0 @@
-
-# Notes for Server maintainer
-
-In order to set up the server to allow imports, one needs to create a
-[Github Access token](https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens). A fine-grained access token with only reading rights for public
-repos will suffice.
-
-You need to set the environment variables `LEAN4GAME_GITHUB_USER` and `LEAN4GAME_GITHUB_TOKEN`
-with your user name and access token. For example, you can seet these in `ecosystem.config.cjs` if
-you're using `pm2`
-
-Then people can call:
-
-> https://{website}/import/trigger/{owner}/{repo}
-
-where you replace:
-- website: The website your server runs on, e.g. `localhost:3000`
-- owner, repo: The owner and repository name of the game you want to load from github.
-
- will trigger to download the latest version of your game from github onto your server.
- Once this import reports "Done", you should be able to play your game under:
-
-> https://{website}/#/g/{owner}/{repo}
-
-## data management
-Everything downloaded remains in the folder `lean4game/games`.
-the subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
-The other folders should only contain the built lean-games, sorted by owner and repo.

doc/update_game.md

@@ -1,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.)

ecosystem.config.js

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

env.d.ts

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

package.json

@@ -1,7 +1,6 @@
 {
   "name": "lean4-game",
   "version": "0.1.0",
-  "type": "module",
   "private": true,
   "homepage": ".",
   "dependencies": {
@@ -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",
+    "start_client": "cross-env NODE_ENV=development webpack-dev-server --hot",
-    "build": "npm run build_server && npm run build_client",
+    "build": "cross-env NODE_ENV=production webpack",
-    "preview": "vite preview",
+    "production": "cross-env NODE_ENV=production node server/index.mjs",
-    "build_server": "cd server && lake build",
+    "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_client": "cross-env NODE_ENV=production vite build",
+    "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",
-    "production": "cross-env NODE_ENV=production node server/index.mjs"
+    "update_lean": "./UPDATE_LEAN.sh"
   },
   "eslintConfig": {
     "extends": [

server/.gitignore

@@ -1,3 +1,3 @@
-build/
+build
-games/
+adam
-.lake
+nng

server/GameServer/Commands.lean

@@ -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 -/
 

server/GameServer/EnvExtensions.lean

@@ -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 : β → β → β) :

server/GameServer/FileWorker.lean

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

server/GameServer/Game.lean

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

server/GameServer/ImportModules.lean

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

server/GameServer/RpcHandlers.lean

@@ -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!)
+  if strict then
-  then return some bij
+    return fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
-  else return none
+  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) hintFVars
-            let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
             let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
             let text ← (MessageData.withContext ctx text).toString
             return some { text := text, hidden := hint.hidden }

server/Main.lean

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

server/bubblewrap.sh

@@ -2,13 +2,11 @@
 
 ELAN_HOME=$(lake env printenv ELAN_HOME)
 
-
-
 (exec bwrap\
-  --bind $2 /lean4game \
+  --ro-bind ../../lean4game /lean4game \
-  --bind $1 /game \
+  --ro-bind ../../$1 /game \
-  --bind $ELAN_HOME /elan \
+  --ro-bind $ELAN_HOME /elan \
-  --bind /usr /usr \
+  --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
 )

server/import.mjs

@@ -11,7 +11,6 @@ const __filename = fileURLToPath(import.meta.url);
 const __dirname = path.dirname(__filename);
 
 const TOKEN = process.env.LEAN4GAME_GITHUB_TOKEN
-const USERNAME = process.env.LEAN4GAME_GITHUB_USER
 const octokit = new Octokit({
   auth: TOKEN
 })
@@ -42,10 +41,9 @@ async function download(id, url, dest) {
     requestProgress(request({
       url,
       headers: {
-        'accept': 'application/vnd.github+json',
+        'User-Agent': 'abentkamp',
-        'User-Agent': USERNAME,
         '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("tmp")){
-    if (!fs.existsSync(`${__dirname}/../games`)){
+      fs.mkdirSync("tmp");
-      fs.mkdirSync(`${__dirname}/../games`);
-    }
-    if (!fs.existsSync(`${__dirname}/../games/tmp`)){
-      fs.mkdirSync(`${__dirname}/../games/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],".")
-    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) {
-    // let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
+      throw `Unexpected manifest: ${JSON.stringify(manifest)}`
-    // manifest = JSON.parse(manifest);
+    }
-    // if (manifest.length !== 1) {
+    manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`]
-    //   throw `Unexpected manifest: ${JSON.stringify(manifest)}`
+    fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest));
-    // }
+    await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`)
-    // manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`]
+    await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`])
-    // 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 += `Done.\n`
-    progress[id].output += `Play the game at: {your website}/#/g/${owner}/${repo}\n`
   } catch (e) {
     progress[id].output += `Error: ${e.toString()}\n${e.stack}`
   } finally {
-    // if (artifactId) {
+    if (artifactId) {
-    //   // fs.rmSync(`tmp/artifact_${artifactId}.zip`, {force: true, recursive: true});
+      fs.rmSync(`tmp/artifact_${artifactId}.zip`, {force: true, recursive: true});
-    //   // fs.rmSync(`tmp/artifact_${artifactId}`, {force: true, recursive: true});
+      fs.rmSync(`tmp/artifact_${artifactId}`, {force: true, recursive: true});
-    //   // fs.rmSync(`tmp/artifact_${artifactId}_inner`, {force: true, recursive: true});
+      fs.rmSync(`tmp/artifact_${artifactId}_inner`, {force: true, recursive: true});
-    //   // fs.rmSync(`tmp/archive_${artifactId}.tar`, {force: true, recursive: true});
+      fs.rmSync(`tmp/archive_${artifactId}.tar`, {force: true, recursive: true});
-    // }
+    }
     progress[id].done = true
   }
-  await new Promise(resolve => setTimeout(resolve, 10000))
 }
 
 export const importTrigger = (req, res) => {

server/index.mjs

@@ -6,20 +6,25 @@ import * as url from 'url';
 import * as rpc from 'vscode-ws-jsonrpc';
 import * as jsonrpcserver from 'vscode-ws-jsonrpc/server';
 import os from 'os';
-import fs from 'fs';
 import anonymize from 'ip-anonymize';
-import { importTrigger, importStatus } from './import.mjs'
+// import { importTrigger, importStatus } from './import.mjs'
 // import fs from 'fs'
 
 /**
- * Add a game here if the server should keep a queue of pre-loaded games ready at all times.
- *
- * IMPORTANT! Tags here need to be lower case!
 */
-const queueLength = {
+const games = {
-  "g/hhu-adam/robo": 2,
+    "g/hhu-adam/robo": {
-  "g/hhu-adam/nng4": 5,
+        dir: "Robo",
-  "g/djvelleman/stg4": 2,
+        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/status/:owner/:repo', importStatus)
-router.get('/import/trigger/:owner/:repo', importTrigger)
+// 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`));
-});
 
 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) {
+function startServerProcess(owner, repo) {
-  owner = owner.toLowerCase()
+  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 {
+    // TODO: This test does not work
-    if(!fs.existsSync(path.join(__dirname, '..', 'games'))) {
+    // if (!fs.existsSync(path.join("../", game_dir))) {
-      console.error(`Did not find the following folder: ${path.join(__dirname, '..', 'games')}`)
+    //   console.error(`Game folder does not exists: ${game_dir}`)
-      console.error('Did you already import any games?')
+    //   return
-      return
+    // }
-    }
   }
 
-  let game_dir = (owner == 'local') ?
+  if (!game_dir) {
-    path.join(__dirname, '..', '..', repo) : // note: here we need `repo` to be case sensitive
+    console.error(`Unknown game: ${tag(owner, repo)}`)
-    path.join(__dirname, '..', 'games', `${owner}`, `${repo.toLowerCase()}`)
-
-  if(!fs.existsSync(game_dir)) {
-    console.error(`Game '${game_dir}' does not exist!`)
     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) {
+function fillQueue(owner, repo) {
-  while (queue[tag].length < queueLength[tag]) {
+    while (queue[tag(owner, repo)].length < games[tag(owner, repo)].queueLength) {
-    let serverProcess
+      const serverProcess = startServerProcess(tag(owner, repo))
-    serverProcess = startServerProcess(tag)
+      queue[tag(owner, repo)].push(serverProcess)
-    if (serverProcess == null) {
-      console.error('serverProcess was undefined/null')
-      return
     }
-    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
+    let ps;
-    if (!queue[tag] || queue[tag].length == 0) {
+    if (!queue[tag(owner, repo)] || queue[tag(owner, repo)].length == 0) {
-      ps = startServerProcess(owner, repo)
+        ps = startServerProcess(owner, repo)
     } else {
-        console.info('Got process from the queue')
+        ps = queue[tag(owner, repo)].shift() // Pick the first Lean process; it's likely to be ready immediately
-        ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately
+        fillQueue(owner, repo)
-        fillQueue(tag)
-    }
-
-    if (ps == null) {
-      console.error('server process is undefined/null')
-      return
     }
 
     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 reader = new rpc.WebSocketMessageReader(socket);
-    const writer = new rpc.WebSocketMessageWriter(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())
+    socketConnection.onClose(() => serverConnection.dispose());
-    serverConnection.onClose(() => socketConnection.dispose())
+    serverConnection.onClose(() => socketConnection.dispose());
 })

server/lake-manifest.json

@@ -1,14 +1,4 @@
-{"version": 7,
+{"version": 6,
- "packagesDir": ".lake/packages",
+ "packagesDir": "lake-packages",
- "packages":
+ "packages": [],
- [{"url": "https://github.com/leanprover/std4.git",
+ "name": "GameServer"}
-   "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"}

server/lakefile.lean

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

server/lean-toolchain

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

server/unpack.sh

@@ -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}
+unzip -o tmp/artifact_${ARTIFACT_ID}.zip -d tmp/artifact_${ARTIFACT_ID}
-echo "Unpacking game."
+echo "Unpacking TAR."
-
+for f in tmp/artifact_${ARTIFACT_ID}/* #Should only be one file
-# exit the npm project to avoid reloading. TODO: Where should we actually save these?
-
-
-
-echo "Delete old version of the game"
-rm -rf ${OWNER}/${REPO}
-mkdir -p ${OWNER}/${REPO}
-
-for f in tmp/${OWNER}_${REPO}_${ARTIFACT_ID}/* #Should only be one file
 do
   echo "Unpacking $f"
-  #tar -xvzf $f -C games/${OWNER}/${REPO}
+  mkdir tmp/artifact_${ARTIFACT_ID}_inner
-  unzip -q -o $f -d ${OWNER}/${REPO}
+  tar -xvf $f -C tmp/artifact_${ARTIFACT_ID}_inner
 done

vite.config.ts

@@ -1,54 +0,0 @@
-import { defineConfig } from 'vite'
-import react from '@vitejs/plugin-react-swc'
-import { viteStaticCopy } from 'vite-plugin-static-copy'
-import svgr from "vite-plugin-svgr"
-
-// https://vitejs.dev/config/
-export default defineConfig({
-  //root: 'client/src',
-  build: {
-    // Relative to the root
-    // Note: This has to match the path in `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",
-    },
-  },
-})

webpack.config.js

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