work on network interruption errors

.gitignore

@@ -1,8 +1,4 @@
 node_modules
 client/dist
 server/build
-server/lakefile.olean
-server32bit
 **/lake-packages/
-**/.DS_Store
-client/public/server.*

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,12 +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)
 
 ### Publishing a Game
 
@@ -31,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,8 +33,7 @@
       </p>
     </div>
   </noscript>
-  <script src="coi-serviceworker.js"></script>
+  <script src="bundle.js"></script>
-  <script type="module" src="/client/src/index.tsx"></script>
 </body>
 
 </html>

client/public/worker.js

@@ -1,94 +0,0 @@
-
-var stderrBuffer = ""
-var messageBuffer = []
-var initialized = false;
-var flushing = false;
-
-var headerMode = true;
-var header="";
-var re = /Content-Length: (\d+)\r\n/i;
-var contentLength = 0;
-var content = []
-var utf8decoder = new TextDecoder();
-
-
-function flushMessageBuffer(){
-  if (initialized && !flushing) {
-    while(messageBuffer.length > 0) {
-      flushing = true;
-      var msg = messageBuffer.shift();
-      console.log(`Send message: ${msg}`);
-      Module.ccall('send_message', 'void', ['string'], [msg]);
-      console.log(`Message done: ${msg}`);
-    }
-    flushing = false;
-  }
-}
-
-var Module = {
-  "arguments": ["--worker"],
-  "preRun": [function() {
-    function stdin() {
-      return null;
-    }
-
-    function stdout(asciiCode) {
-      if (headerMode) {
-        header += String.fromCharCode(asciiCode)
-        if (header.endsWith('\r\n\r\n')) {
-          const found = header.match(re)
-          if (found == null) { console.error(`Invalid header: ${header}`) }
-          contentLength = parseInt(found[1])
-          content = []
-          headerMode = false
-        }
-      } else {
-        content.push(asciiCode)
-        if (content.length == contentLength) {
-          const message = utf8decoder.decode(new Uint8Array(content))
-          console.log(`Server: ${message}`)
-          postMessage(message);
-          headerMode = true
-          header = ''
-        }
-      }
-    }
-
-    function stderr(asciiCode) {
-      stderrBuffer += String.fromCharCode(asciiCode)
-    }
-
-    FS.init(stdin, stdout, stderr);
-  }],
-  "noInitialRun": true,
-  "onRuntimeInitialized": () => {
-    Module.ccall('main', 'void', [], []);
-    initialized = true;
-    if (stderrBuffer !== "") {
-      console.log(stderrBuffer);
-      stderrBuffer = ""
-    }
-    flushMessageBuffer();
-  }
-};
-
-importScripts("server.js")
-
-
-
-onmessage = (ev) => {
-  console.log(`Client: ${ev.data}`)
-  messageBuffer.push(ev.data);
-  flushMessageBuffer();
-}
-
-setInterval(() => {
-  if (stderrBuffer !== "") {
-    console.log(stderrBuffer);
-    stderrBuffer = ""
-  }
-}, 1000)
-
-setTimeout(() =>{
-
-},2000)

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,19 +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 { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
+  const { showHelp, setShowHelp } = React.useContext(DeletedChatContext)
   const {mobile} = React.useContext(MobileContext)
   const { proof } = React.useContext(ProofContext)
-  const { setTypewriterInput } = React.useContext(InputModeContext)
   const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
 
   const proofPanelRef = React.useRef<HTMLDivElement>(null)
@@ -358,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) => {
@@ -399,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 {

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/level.tsx

@@ -237,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}))
   }
@@ -254,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
@@ -296,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 {
@@ -335,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
@@ -363,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}}>
@@ -483,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)
@@ -604,17 +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(); }
       }
     }
   }, [editor, levelId, connection, leanClientStarted])
@@ -624,14 +608,16 @@ 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])
 
@@ -657,7 +643,7 @@ function useLoadWorldFiles(worldId) {
           models.push(monaco.editor.createModel(code, 'lean4', uri))
         }
       }
-      return () => { for (let model of models) { model.dispose() } }
+      return () => { for (let model of models) { try {model.dispose()} catch {console.log(`failed to dispose model ${model}`)}} }
     }
   }, [gameInfo.data, worldId])
 }

client/src/connection.ts

@@ -4,7 +4,7 @@
 
 import * as React from 'react';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
-import { LeanClient } from './leanclient';
+import { LeanClient } from 'lean4web/client/src/editor/leanclient';
 
 export class Connection {
   private game: string = undefined // We only keep a connection to a single game at a time

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/index.tsx

@@ -1,45 +1,29 @@
-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()
 
-// // Do not show the landing page in the dev-container context
-// let root_path: RouteObject = (process.env.LEAN4GAME_SINGLE_GAME == "true") ? {
-//   path: "/",
-//   loader: () => redirect("/g/local/game")
-// } : {
-//   path: "/",
-//   element: <LandingPage />,
-// }
-
-
-// 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: "/",
+    element: <LandingPage />,
+  },
+  {
     path: "/game/nng",
     loader: () => redirect("/g/hhu-adam/NNG4")
   },

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/leanclient.ts

@@ -1,612 +0,0 @@
-/* This file is based on `vscode-lean4/src/leanclient.ts` */
-
-import {
-  TextDocument, EventEmitter, Diagnostic,
-  DocumentHighlight, Range, DocumentHighlightKind, workspace,
-  Disposable, Uri, ConfigurationChangeEvent, OutputChannel, DiagnosticCollection,
-  WorkspaceFolder, window
-} from 'vscode'
-import {
-  DidChangeTextDocumentParams,
-  DidCloseTextDocumentParams,
-  DidOpenTextDocumentNotification,
-  DocumentFilter,
-  InitializeResult,
-  MonacoLanguageClient as LanguageClient,
-  LanguageClientOptions,
-  PublishDiagnosticsParams,
-  CloseAction, ErrorAction,
-  RevealOutputChannelOn,
-} from 'monaco-languageclient'
-import { State } from 'vscode-languageclient'
-import * as ls from 'vscode-languageserver-protocol'
-import { toSocket } from 'vscode-ws-jsonrpc'
-
-import {
-  // toolchainPath, lakePath, addServerEnvPaths, serverArgs, serverLoggingEnabled, serverLoggingPath, shouldAutofocusOutput,
-  getElaborationDelay
-  // lakeEnabled
-} from 'lean4web/client/src/editor/config'
-// import { assert } from './utils/assert'
-import { LeanFileProgressParams, LeanFileProgressProcessingInfo } from '@leanprover/infoview-api'
-// import { LocalStorageService } from './utils/localStorage'
-// import { batchExecute } from './utils/batch'
-// import { readLeanVersion } from './utils/projectInfo'
-import * as fs from 'fs'
-import { URL } from 'url'
-import { join } from 'path'
-// import { logger } from './utils/logger'
-import { SemVer } from 'semver'
-// import { fileExists, isFileInFolder } from './utils/fsHelper'
-import { c2pConverter, p2cConverter, patchConverters } from 'lean4web/client/src/editor/utils/converters'
-import { WasmReader, WasmWriter, WebSocketMessageWriter, WebSocketMessageReader } from './wasm'
-
-const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&')
-
-export type ServerProgress = Map<Uri, LeanFileProgressProcessingInfo[]>
-
-export function getFullRange (diag: Diagnostic): Range {
-  return (diag as any)?.fullRange || diag.range
-}
-
-export class LeanClient implements Disposable {
-  running: boolean = false
-  private client: LanguageClient | undefined
-  // private toolchainPath: string
-  // private readonly outputChannel: OutputChannel
-  // private readonly storageManager: LocalStorageService
-  private readonly workspaceFolder: WorkspaceFolder | undefined
-  private readonly folderUri: Uri
-  private readonly subscriptions: Disposable[] = []
-  private noPrompt: boolean = false
-  private showingRestartMessage: boolean = false
-  // private readonly elanDefaultToolchain: string
-
-  private readonly didChangeEmitter = new EventEmitter<DidChangeTextDocumentParams>()
-  didChange = this.didChangeEmitter.event
-
-  private readonly diagnosticsEmitter = new EventEmitter<PublishDiagnosticsParams>()
-  diagnostics = this.diagnosticsEmitter.event
-
-  private readonly didSetLanguageEmitter = new EventEmitter<string>()
-  didSetLanguage = this.didSetLanguageEmitter.event
-
-  private readonly didCloseEmitter = new EventEmitter<DidCloseTextDocumentParams>()
-  didClose = this.didCloseEmitter.event
-
-  private readonly customNotificationEmitter = new EventEmitter<{ method: string, params: any }>()
-  /** Fires whenever a custom notification (i.e. one not defined in LSP) is received. */
-  customNotification = this.customNotificationEmitter.event
-
-  /** saved progress info in case infoview is opened, it needs to get all of it. */
-  progress: ServerProgress = new Map()
-
-  private readonly progressChangedEmitter = new EventEmitter<[string, LeanFileProgressProcessingInfo[]]>()
-  progressChanged = this.progressChangedEmitter.event
-
-  private readonly stoppedEmitter = new EventEmitter()
-  stopped = this.stoppedEmitter.event
-
-  private readonly restartedEmitter = new EventEmitter()
-  restarted = this.restartedEmitter.event
-
-  private readonly restartingEmitter = new EventEmitter()
-  restarting = this.restartingEmitter.event
-
-  private readonly restartedWorkerEmitter = new EventEmitter<string>()
-  restartedWorker = this.restartedWorkerEmitter.event
-
-  private readonly serverFailedEmitter = new EventEmitter<string>()
-  serverFailed = this.serverFailedEmitter.event
-
-  /** Files which are open. */
-  private readonly isOpen: Map<string, TextDocument> = new Map()
-
-  constructor (private readonly socketUrl: string, workspaceFolder: WorkspaceFolder | undefined, folderUri: Uri,
-    public readonly showRestartMessage: () => void) {
-    // this.storageManager = storageManager
-    // this.outputChannel WebSocketMessageWriter= outputChannel
-    this.workspaceFolder = workspaceFolder // can be null when opening adhoc files.
-    this.folderUri = folderUri
-    // this.elanDefaultToolchain = elanDefaultToolchain
-    // this.subscriptions.push(workspace.onDidChangeConfiguration((e) => this.configChanged(e)))
-  }
-
-  dispose (): void {
-    this.subscriptions.forEach((s) => s.dispose())
-    if (this.isStarted()) void this.stop()
-  }
-
-  // async showRestartMessage (restartFile: boolean = false): Promise<void> {
-  //   // if (!this.showingRestartMessage) {
-  //   //   this.showingRestartMessage = true
-  //   //   let restartItem: string
-  //   //   let messageTitle: string
-  //   //   if (!restartFile) {
-  //   //     restartItem = 'Restart Lean Server'
-  //   //     messageTitle = 'Lean Server has stopped unexpectedly.'
-  //   //   } else {
-  //   //     restartItem = 'Restart Lean Server on this file'
-  //   //     messageTitle = 'The Lean Server has stopped processing this file.'
-  //   //   }
-  //   //   const item = await this.showErrorMessage(messageTitle, restartItem)
-  //   //   this.showingRestartMessage = false
-  //   //   if (item === restartItem) {
-  //   //     void this.start()
-  //   //     // if (restartFile && (window.activeTextEditor != null)) {
-  //   //     //   await this.restartFile(window.activeTextEditor.document)
-  //   //     // } else {
-  //   //     //   void this.start()
-  //   //     // }
-  //   //   }
-  //   // }
-  // }
-
-  async restart (): Promise<void> {
-    const startTime = Date.now()
-
-    console.log('[LeanClient] Restarting Lean Server')
-    if (this.isStarted()) {
-      await this.stop()
-    }
-
-    this.restartingEmitter.fire(undefined)
-    // this.toolchainPath = this.storageManager.getLeanPath()
-    // if (!this.toolchainPath) this.toolchainPath = toolchainPath()
-    // let version = this.storageManager.getLeanVersion()
-    // const env = addServerEnvPaths(process.env)
-    // if (serverLoggingEnabled()) {
-    //   env.LEAN_SERVER_LOG_DIR = serverLoggingPath()
-    // }
-
-    // let executable = lakePath() ||
-    //       (this.toolchainPath ? join(this.toolchainPath, 'bin', 'lake') : 'lake')
-
-    // check if the lake process will start (skip it on scheme: 'untitled' files)
-    // let useLake = lakeEnabled() && this.folderUri && this.folderUri.scheme === 'file'
-    // if (useLake) {
-    //   let knownDate = false
-    //   const lakefile = Uri.joinPath(this.folderUri, 'lakefile.lean')
-    //   if (!await fileExists(new URL(lakefile.toString()))) {
-    //     useLake = false
-    //   } else {
-    //     // see if we can avoid the more expensive checkLakeVersion call.
-    //     const date = await this.checkToolchainVersion(this.folderUri)
-    //     if (date != null) {
-    //       // Feb 16 2022 is when the 3.1.0.pre was released.
-    //       useLake = date >= new Date(2022, 1, 16)
-    //       knownDate = true
-    //     }
-    //     if (useLake && !knownDate) {
-    //       useLake = await this.checkLakeVersion(executable, version)
-    //     }
-    //   }
-    // }
-
-    // if (!useLake) {
-    //   executable = (this.toolchainPath) ? join(this.toolchainPath, 'bin', 'lean') : 'lean'
-    // }
-
-    // const cwd = this.folderUri?.fsPath
-    // if (!cwd && !version) {
-    //   // Fixes issue #227, for adhoc files it would pick up the cwd from the open folder
-    //   // which is not what we want.  For adhoc files we want the (default) toolchain instead.
-    //   version = this.elanDefaultToolchain
-    // }
-
-    // let options = version ? ['+' + version] : []
-    // if (useLake) {
-    //   options = options.concat(['serve', '--'])
-    // } else {
-    //   options = options.concat(['--server'])
-    // }
-
-    // Add folder name to command-line so that it shows up in `ps aux`.
-    // if (cwd) {
-    //   options.push('' + cwd)
-    // } else {
-    //   options.push('untitled')
-    // }
-
-    // const serverOptions: ServerOptions = {
-    //   command: executable,
-    //   args: options.concat(serverArgs()),
-    //   options: {
-    //     cwd,
-    //     env
-    //   }
-    // }
-
-    const clientOptions: LanguageClientOptions = {
-      // use a language id as a document selector
-      documentSelector: ['lean4'],
-      initializationOptions: {
-        editDelay: getElaborationDelay(), hasWidgets: true
-      },
-      connectionOptions: {
-        maxRestartCount: 0,
-        cancellationStrategy: undefined as any
-      },
-      // disable the default error handler
-      errorHandler: {
-        error: () => ({ action: ErrorAction.Continue }),
-        closed: () => ({ action: CloseAction.DoNotRestart })
-      },
-      middleware: {
-        handleDiagnostics: (uri, diagnostics, next) => {
-          next(uri, diagnostics)
-          if (this.client == null) return
-          const uri_ = c2pConverter.asUri(uri)
-          const diagnostics_ = []
-          for (const d of diagnostics) {
-            const d_: ls.Diagnostic = {
-              ...c2pConverter.asDiagnostic(d)
-            }
-            diagnostics_.push(d_)
-          }
-          this.diagnosticsEmitter.fire({ uri: uri_, diagnostics: diagnostics_ })
-        },
-
-        // didOpen: async () => {
-        //   // Note: as per the LSP spec: An open notification must not be sent more than once
-        //   // without a corresponding close notification send before. This means open and close
-        //   // notification must be balanced and the max open count for a particular textDocument
-        //   // is one.  So this even does nothing the notification is handled by the
-        //   // openLean4Document method below after the 'lean4' languageId is established and
-        //   // it has weeded out documents opened to invisible editors (like 'git:' schemes and
-        //   // invisible editors created for Ctrl+Hover events.  A side effect of unbalanced
-        //   // open/close notification is leaking 'lean --worker' processes.
-        //   // See https://github.com/microsoft/vscode/issues/78453).
-
-        // },
-
-        didChange: async (data, next) => {
-          await next(data)
-          if (!this.running || (this.client == null)) return // there was a problem starting lean server.
-          const params = c2pConverter.asChangeTextDocumentParams(data)
-          this.didChangeEmitter.fire(params)
-        },
-
-        didClose: async (doc, next) => {
-          if (!this.isOpen.delete(doc.uri.toString())) {
-            return
-          }
-          await next(doc)
-          if (!this.running || (this.client == null)) return // there was a problem starting lean server.
-          const params = c2pConverter.asCloseTextDocumentParams(doc)
-          this.didCloseEmitter.fire(params)
-        },
-
-        provideDocumentHighlights: async (doc, pos, ctok, next) => {
-          const leanHighlights = await next(doc, pos, ctok)
-          if (leanHighlights?.length) return leanHighlights
-
-          // vscode doesn't fall back to textual highlights,
-          // so we need to do that manually
-          await new Promise((res) => setTimeout(res, 250))
-          if (ctok.isCancellationRequested) return
-
-          const wordRange = doc.getWordRangeAtPosition(pos)
-          if (wordRange == null) return
-          const word = doc.getText(wordRange)
-
-          const highlights: DocumentHighlight[] = []
-          const text = doc.getText()
-          const nonWordPattern = '[`~@$%^&*()-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\\\|;:\",./\\s]|^|$'
-          const regexp = new RegExp(`(?<=${nonWordPattern})${escapeRegExp(word)}(?=${nonWordPattern})`, 'g')
-          for (const match of text.matchAll(regexp)) {
-            const start = doc.positionAt(match.index ?? 0)
-            highlights.push({
-              range: new Range(start, start.translate(0, match[0].length)),
-              kind: DocumentHighlightKind.Text
-            })
-          }
-
-          return highlights
-        }
-      }
-    }
-    if (!this.client) {
-      this.client = new LanguageClient({
-        id: 'lean4',
-        name: 'Lean 4',
-        clientOptions,
-        connectionProvider: {
-          get: async () => {
-            return await new Promise((resolve, reject) => {
-              const worker = new Worker("worker.js")
-              const reader = new WasmReader(worker)
-              const writer = new WasmWriter(worker)
-              resolve({
-                reader,
-                writer
-              })
-            })
-          }
-        }
-      })
-    } else {
-      await this.client.start()
-    }
-
-
-    // HACK: Prevent monaco from panicking when the Lean server crashes
-    this.client.handleFailedRequest = (type, token: any, error: any, defaultValue, showNotification?: boolean) => {
-      return defaultValue
-    }
-
-    let insideRestart = true
-    patchConverters(this.client.protocol2CodeConverter, this.client.code2ProtocolConverter)
-    try {
-      this.client.onDidChangeState(async (s) => {
-        // see https://github.com/microsoft/vscode-languageserver-node/issues/825
-        if (s.newState === State.Starting) {
-          console.log('[LeanClient] starting')
-        } else if (s.newState === State.Running) {
-          const end = Date.now()
-          console.log(`[LeanClient] running, started in ${end - startTime} ms`)
-          this.running = true // may have been auto restarted after it failed.
-          if (!insideRestart) {
-            this.restartedEmitter.fire(undefined)
-          }
-        } else if (s.newState === State.Stopped) {
-          this.running = false
-          console.log('[LeanClient] has stopped or it failed to start')
-          if (!this.noPrompt) {
-            // only raise this event and show the message if we are not the ones
-            // who called the stop() method.
-            this.stoppedEmitter.fire({ message: 'Lean server has stopped.', reason: '' })
-            await this.showRestartMessage()
-          }
-        }
-      })
-      await this.client.start()
-      // tell the new client about the documents that are already open!
-      // for (const key of this.isOpen.keys()) {
-      //   const doc = this.isOpen.get(key)
-      //   if (doc != null) this.notifyDidOpen(doc)
-      // }
-      // if we got this far then the client is happy so we are running!
-      this.running = true
-    } catch (error) {
-      console.log(error)
-      this.serverFailedEmitter.fire('' + error)
-      insideRestart = false
-      return
-    }
-
-    // HACK(WN): Register a default notification handler to fire on custom notifications.
-    // A mechanism to do this is provided in vscode-jsonrpc. One can register a `StarNotificationHandler`
-    // here: https://github.com/microsoft/vscode-languageserver-node/blob/b2fc85d28a1a44c22896559ee5f4d3ba37a02ef5/jsonrpc/src/common/connection.ts#L497
-    // which fires on any LSP notifications not in the standard, for example the `$/lean/..` ones.
-    // However this mechanism is not exposed in vscode-languageclient, so we hack around its implementation.
-    const starHandler = (method: string, params_: any) => {
-      if (method === '$/lean/fileProgress' && (this.client != null)) {
-        const params = params_ as LeanFileProgressParams
-        const uri = p2cConverter.asUri(params.textDocument.uri)
-        this.progressChangedEmitter.fire([uri.toString(), params.processing])
-        // save the latest progress on this Uri in case infoview needs it later.
-        this.progress.set(uri, params.processing)
-      }
-
-      this.customNotificationEmitter.fire({ method, params: params_ })
-    }
-    // eslint-disable-next-line @typescript-eslint/no-unsafe-argument
-    this.client.onNotification(starHandler as any, () => {})
-
-    // Reveal the standard error output channel when the server prints something to stderr.
-    // The vscode-languageclient library already takes care of writing it to the output channel.
-    // let stderrMsgBoxVisible = false;
-    // (this.client)._serverProcess.stderr.on('data', async (chunk: Buffer) => {
-    //   if (shouldAutofocusOutput()) {
-    //     this.client?.outputChannel.show(true)
-    //   } else if (!stderrMsgBoxVisible) {
-    //     stderrMsgBoxVisible = true
-    //     const outputItem = 'Show stderr output'
-    //     const outPrompt = `Lean server printed an error:\n${chunk.toString()}`
-    //     if (await window.showErrorMessage(outPrompt, outputItem) === outputItem) {
-    //       this.outputChannel.show(false)
-    //     }
-    //     stderrMsgBoxVisible = false
-    //   }
-    // })
-
-    this.restartedEmitter.fire(undefined)
-    insideRestart = false
-  }
-
-  async openLean4Document (doc: TextDocument) {
-    if (this.isOpen.has(doc.uri.toString())) return
-    if (!await this.isSameWorkspace(doc.uri)) {
-      // skip it, this file belongs to a different workspace...
-      return
-    }
-
-    this.isOpen.set(doc.uri.toString(), doc)
-
-    if (!this.running) return // there was a problem starting lean server.
-
-    // didOpenEditor may have also changed the language, so we fire the
-    // event here because the InfoView should be wired up to receive it now.
-    this.didSetLanguageEmitter.fire(doc.languageId)
-
-    this.notifyDidOpen(doc)
-  }
-
-  notifyDidOpen (doc: TextDocument) {
-    // BUG: was `DidOpenTextDocumentNotification.type` instead of the string, but that failed
-    void this.client?.sendNotification('textDocument/didOpen', {
-      textDocument: {
-        uri: doc.uri.toString(),
-        languageId: doc.languageId,
-        version: 1,
-        text: doc.getText()
-      }
-    })
-  }
-
-  async isSameWorkspace (uri: Uri): Promise<boolean> {
-    // if (this.folderUri) {
-    //   if (this.folderUri.scheme !== uri.scheme) return false
-    //   if (this.folderUri.scheme === 'file') {
-    //     const realPath1 = await fs.promises.realpath(this.folderUri.fsPath)
-    //     const realPath2 = await fs.promises.realpath(uri.fsPath)
-    //     return isFileInFolder(realPath2, realPath1)
-    //   } else {
-    //     return uri.toString().startsWith(this.folderUri.toString())
-    //   }
-    // } else {
-    //   return uri.scheme === 'untitled'
-    // }
-    return false
-  }
-
-  getWorkspaceFolder (): string {
-    return this.folderUri?.toString()
-  }
-
-  async start (): Promise<void> {
-    return await this.restart()
-  }
-
-  isStarted (): boolean {
-    return this.client !== undefined
-  }
-
-  isRunning (): boolean {
-    if (this.client != null) {
-      return this.running
-    }
-    return false
-  }
-
-  async stop (): Promise<void> {
-    // assert(() => this.isStarted())
-    if ((this.client != null) && this.running) {
-      this.noPrompt = true
-      try {
-        // some timing conditions can happen while running unit tests that cause
-        // this to throw an exception which then causes those tests to fail.
-        await this.client.stop()
-      } catch (e) {
-        console.log(`[LeanClient] Error stopping language client: ${e}`)
-      }
-    }
-
-    this.noPrompt = false
-    this.progress = new Map()
-    this.client = undefined
-    this.running = false
-  }
-
-  configChanged (e: ConfigurationChangeEvent): void {
-    // let newToolchainPath = this.storageManager.getLeanPath()
-    // if (!newToolchainPath) newToolchainPath = toolchainPath()
-    // if (this.toolchainPath !== newToolchainPath) {
-    //  void this.restart()
-    // }
-  }
-
-  async restartFile (doc: TextDocument): Promise<void> {
-    if (!this.running) return // there was a problem starting lean server.
-
-    // assert(() => this.isStarted())
-
-    if (!await this.isSameWorkspace(doc.uri)) {
-      // skip it, this file belongs to a different workspace...
-      return
-    }
-    const uri = doc.uri.toString()
-    console.log(`[LeanClient] Restarting File: ${uri}`)
-    // This causes a text document version number discontinuity. In
-    // (didChange (oldVersion) => restartFile => didChange (newVersion))
-    // the client emits newVersion = oldVersion + 1, despite the fact that the
-    // didOpen packet emitted below initializes the version number to be 1.
-    // This is not a problem though, since both client and server are fine
-    // as long as the version numbers are monotonous.
-    void this.client?.sendNotification('textDocument/didClose', {
-      textDocument: {
-        uri
-      }
-    })
-    void this.client?.sendNotification('textDocument/didOpen', {
-      textDocument: {
-        uri,
-        languageId: 'lean4',
-        version: 1,
-        text: doc.getText()
-      }
-    })
-    this.restartedWorkerEmitter.fire(uri)
-  }
-
-  // eslint-disable-next-line @typescript-eslint/explicit-module-boundary-types
-  async sendRequest (method: string, params: any): Promise<any> {
-    return this.running && (this.client != null)
-      ? await this.client.sendRequest(method, params)
-      : await new Promise<any>((_, reject) => { reject('Client is not running') })
-  }
-
-  // eslint-disable-next-line @typescript-eslint/explicit-module-boundary-types
-  sendNotification (method: string, params: any): Promise<void> | undefined {
-    return this.running && (this.client != null) ? this.client.sendNotification(method, params) : undefined
-  }
-
-  async getDiagnosticParams (uri: Uri, diagnostics: readonly Diagnostic[]): Promise<PublishDiagnosticsParams> {
-    const params: PublishDiagnosticsParams = {
-      uri: c2pConverter.asUri(uri),
-      diagnostics: await c2pConverter.asDiagnostics(diagnostics as Diagnostic[])
-    }
-    return params
-  }
-
-  getDiagnostics (): DiagnosticCollection | undefined {
-    return this.running ? this.client?.diagnostics : undefined
-  }
-
-  get initializeResult (): InitializeResult | undefined {
-    return this.running ? this.client?.initializeResult : undefined
-  }
-
-  private async checkToolchainVersion (folderUri: Uri): Promise<Date | undefined> {
-    // see if we have a well known toolchain label that corresponds
-    // to a known date like 'leanprover/lean4:nightly-2022-02-01'
-    // const toolchainVersion = await readLeanVersion(folderUri)
-    // if (toolchainVersion) {
-    //   const match = /^leanprover\/lean4:nightly-(\d+)-(\d+)-(\d+)$/.exec(toolchainVersion)
-    //   if (match != null) {
-    //     return new Date(parseInt(match[1]), parseInt(match[2]) - 1, parseInt(match[3]))
-    //   }
-    //   if (toolchainVersion === 'leanprover/lean4:stable') {
-    //     return new Date(2022, 2, 1)
-    //   }
-    // }
-    return undefined
-  }
-
-  // async checkLakeVersion (executable: string, version: string): Promise<boolean> {
-  //   // Check that the Lake version is high enough to support "lake serve" option.
-  //   const versionOptions = version ? ['+' + version, '--version'] : ['--version']
-  //   const start = Date.now()
-  //   const lakeVersion = await batchExecute(executable, versionOptions, this.folderUri?.fsPath, undefined)
-  //   logger.log(`[LeanClient] Ran '${executable} ${versionOptions.join(' ')}' in ${Date.now() - start} ms`)
-  //   const actual = this.extractVersion(lakeVersion)
-  //   if (actual.compare('3.0.0') > 0) {
-  //     return true
-  //   }
-  //   return false
-  // }
-
-  // private extractVersion (v: string | undefined): SemVer {
-  //   if (!v) return new SemVer('0.0.0')
-  //   const prefix = 'Lake version'
-  //   if (v.startsWith(prefix)) v = v.slice(prefix.length).trim()
-  //   const pos = v.indexOf('(')
-  //   if (pos > 0) v = v.slice(0, pos).trim()
-  //   try {
-  //     return new SemVer(v)
-  //   } catch {
-  //     return new SemVer('0.0.0')
-  //   }
-  // }
-}

client/src/wasm.ts

@@ -1,341 +0,0 @@
-
-
-import { DataCallback, AbstractMessageReader, MessageReader } from 'vscode-jsonrpc/lib/common/messageReader.js';
-
-import { Message } from 'vscode-jsonrpc/lib/common/messages.js';
-import { AbstractMessageWriter, MessageWriter } from 'vscode-jsonrpc/lib/common/messageWriter.js';
-import { Emitter } from 'vscode-jsonrpc/lib/common/events.js';
-import { Disposable, IWebSocket } from 'vscode-ws-jsonrpc/.';
-
-declare var IO: any;
-
-export class WasmWriter implements MessageWriter {
-  protected errorCount = 0;
-  errorEmitter
-  closeEmitter
-  constructor(private worker: Worker) {
-    this.errorEmitter = new Emitter()
-    this.closeEmitter = new Emitter()
-}
-dispose() {
-    this.errorEmitter.dispose();
-    this.closeEmitter.dispose();
-}
-get onError() {
-    return this.errorEmitter.event;
-}
-fireError(error, message, count) {
-    this.errorEmitter.fire([this.asError(error), message, count]);
-}
-get onClose() {
-    return this.closeEmitter.event;
-}
-fireClose() {
-    this.closeEmitter.fire(undefined);
-}
-asError(error) {
-    if (error instanceof Error) {
-        return error;
-    }
-    else {
-        return new Error(`Writer received error. Reason: ${error.message}`);
-    }
-}
-
-  end(): void {
-  }
-
-  async write(msg: Message): Promise<void> {
-      try {
-          const content = JSON.stringify(msg);
-          this.worker.postMessage(content)
-      } catch (e) {
-          this.errorCount++;
-          this.fireError(e, msg, this.errorCount);
-      }
-  }
-}
-
-
-export class WasmReader implements MessageReader {
-  protected state: 'initial' | 'listening' | 'closed' = 'initial';
-  protected callback: DataCallback | undefined;
-  protected readonly events: { message?: any, error?: any }[] = [];
-
-  constructor(private worker: Worker) {
-    this.worker.onmessage = (ev) => {
-      this.readMessage(ev.data)
-    }
-      // this.socket.onMessage(message =>
-      //     this.readMessage(message)
-      // );
-      // this.socket.onError(error =>
-      //     this.fireError(error)
-      // );
-      // this.socket.onClose((code, reason) => {
-      //     if (code !== 1000) {
-      //         const error: Error = {
-      //             name: '' + code,
-      //             message: `Error during socket reconnect: code = ${code}, reason = ${reason}`
-      //         };
-      //         this.fireError(error);
-      //     }
-      //     this.fireClose();
-      // });
-    this.errorEmitter = new Emitter()
-    this.closeEmitter = new Emitter()
-    this.partialMessageEmitter = new Emitter()
-  }
-
-  protected errorCount = 0;
-  errorEmitter
-  closeEmitter
-  partialMessageEmitter
-
-dispose() {
-    this.errorEmitter.dispose();
-    this.closeEmitter.dispose();
-}
-get onError() {
-    return this.errorEmitter.event;
-}
-get onClose() {
-    return this.closeEmitter.event;
-}
-get onPartialMessage() {
-    return this.partialMessageEmitter.event;
-}
-firePartialMessage(info) {
-    this.partialMessageEmitter.fire(info);
-}
-asError(error) {
-    if (error instanceof Error) {
-        return error;
-    }
-    else {
-        return new Error(`Reader received error. Reason: ${error.message ? error.message : 'unknown'}`);
-    }
-}
-
-  listen(callback: DataCallback): Disposable {
-      if (this.state === 'initial') {
-          this.state = 'listening';
-          this.callback = callback;
-          while (this.events.length !== 0) {
-              const event = this.events.pop()!;
-              if (event.message) {
-                  this.readMessage(event.message);
-              } else if (event.error) {
-                  this.fireError(event.error);
-              } else {
-                  this.fireClose();
-              }
-          }
-      }
-      return {
-          dispose: () => {
-              if (this.callback === callback) {
-                  this.callback = undefined;
-              }
-          }
-      };
-  }
-
-  protected readMessage(message: any): void {
-      if (this.state === 'initial') {
-          this.events.splice(0, 0, { message });
-      } else if (this.state === 'listening') {
-          try {
-              const data = JSON.parse(message);
-              this.callback!(data);
-          } catch (err) {
-              const error: Error = {
-                  name: '' + 400,
-                  message: `Error during message parsing, reason = ${typeof err === 'object' ? (err as any).message : 'unknown'}`
-              };
-              this.fireError(error);
-          }
-      }
-  }
-
-  protected fireError(error: any): void {
-      if (this.state === 'initial') {
-          this.events.splice(0, 0, { error });
-      } else if (this.state === 'listening') {
-
-    this.errorEmitter.fire(this.asError(error));
-      }
-  }
-
-  protected fireClose(): void {
-      if (this.state === 'initial') {
-          this.events.splice(0, 0, {});
-      } else if (this.state === 'listening') {
-        this.closeEmitter.fire(undefined);
-      }
-      this.state = 'closed';
-  }
-}
-export class WebSocketMessageWriter implements MessageWriter {
-    protected errorCount = 0;
-    errorEmitter
-    closeEmitter
-
-    constructor(protected readonly socket: IWebSocket) {
-        this.errorEmitter = new Emitter();
-        this.closeEmitter = new Emitter();
-    }
-    dispose() {
-        this.errorEmitter.dispose();
-        this.closeEmitter.dispose();
-    }
-    get onError() {
-        return this.errorEmitter.event;
-    }
-    fireError(error, message, count) {
-        this.errorEmitter.fire([this.asError(error), message, count]);
-    }
-    get onClose() {
-        return this.closeEmitter.event;
-    }
-    fireClose() {
-        this.closeEmitter.fire(undefined);
-    }
-    asError(error) {
-        if (error instanceof Error) {
-            return error;
-        }
-        else {
-            return new Error(`Writer received error. Reason: ${(error.message) ? error.message : 'unknown'}`);
-        }
-    }
-    end(): void {
-    }
-
-    async write(msg: Message): Promise<void> {
-        console.log("WRITE",msg)
-        try {
-            const content = JSON.stringify(msg);
-            this.socket.send(content);
-        } catch (e) {
-            this.errorCount++;
-            this.fireError(e, msg, this.errorCount);
-        }
-    }
-}
-
-
-
-export class WebSocketMessageReader implements MessageReader {
-    protected state: 'initial' | 'listening' | 'closed' = 'initial';
-    protected callback: DataCallback | undefined;
-    protected readonly events: { message?: any, error?: any }[] = [];
-    errorEmitter
-    closeEmitter
-    partialMessageEmitter
-
-    constructor(protected readonly socket: IWebSocket) {
-        this.errorEmitter = new Emitter();
-        this.closeEmitter = new Emitter();
-        this.partialMessageEmitter = new Emitter();
-        this.socket.onMessage(message =>{
-            console.log("READ", message)
-            this.readMessage(message)
-        });
-        this.socket.onError(error =>
-            this.fireError(error)
-        );
-        this.socket.onClose((code, reason) => {
-            if (code !== 1000) {
-                const error: Error = {
-                    name: '' + code,
-                    message: `Error during socket reconnect: code = ${code}, reason = ${reason}`
-                };
-                this.fireError(error);
-            }
-            this.fireClose();
-        });
-    }
-    dispose() {
-        this.errorEmitter.dispose();
-        this.closeEmitter.dispose();
-    }
-    get onError() {
-        return this.errorEmitter.event;
-    }
-    get onClose() {
-        return this.closeEmitter.event;
-    }
-    get onPartialMessage() {
-        return this.partialMessageEmitter.event;
-    }
-    firePartialMessage(info) {
-        this.partialMessageEmitter.fire(info);
-    }
-    asError(error) {
-        if (error instanceof Error) {
-            return error;
-        }
-        else {
-            return new Error(`Reader received error. Reason: ${(error.message) ? error.message : 'unknown'}`);
-        }
-    }
-
-    listen(callback: DataCallback): Disposable {
-        if (this.state === 'initial') {
-            this.state = 'listening';
-            this.callback = callback;
-            while (this.events.length !== 0) {
-                const event = this.events.pop()!;
-                if (event.message) {
-                    this.readMessage(event.message);
-                } else if (event.error) {
-                    this.fireError(event.error);
-                } else {
-                    this.fireClose();
-                }
-            }
-        }
-        return {
-            dispose: () => {
-                if (this.callback === callback) {
-                    this.callback = undefined;
-                }
-            }
-        };
-    }
-
-    protected readMessage(message: any): void {
-        if (this.state === 'initial') {
-            this.events.splice(0, 0, { message });
-        } else if (this.state === 'listening') {
-            try {
-                const data = JSON.parse(message);
-                this.callback!(data);
-            } catch (err) {
-                const error: Error = {
-                    name: '' + 400,
-                    message: `Error during message parsing, reason = ${typeof err === 'object' ? (err as any).message : 'unknown'}`
-                };
-                this.fireError(error);
-            }
-        }
-    }
-
-    protected fireError(error: any): void {
-        if (this.state === 'initial') {
-            this.events.splice(0, 0, { error });
-        } else if (this.state === 'listening') {
-            this.errorEmitter.fire(this.asError(error));
-        }
-    }
-
-    protected fireClose(): void {
-        if (this.state === 'initial') {
-            this.events.splice(0, 0, {});
-        } else if (this.state === 'listening') {
-            this.closeEmitter.fire(undefined);
-        }
-        this.state = 'closed';
-    }
-}

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,10 +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](https://github.com/leanprover-community/lean4game/blob/main/doc/update_game.md).
-
 ## Further Notes
 
 Here are some random further things you should consider designing a new 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,15 +73,15 @@ 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
 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,15 +106,15 @@ 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 setting `export LEAN4GAME=local` inside your local game before building it:
+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
-export LEAN4GAME=local
+export NODE_ENV=development
 lake update
 lake build
 ```

doc/update_game.md

@@ -1,37 +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` (followed by `lake exe cache get` if you depend on mathlib.)
-* Gitpod/Codespaces: Create a fresh one
-
-This will update `lean4game` and `mathlib` in your project 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're 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:
-
-```
-lakefile.lean
-.devcontainer/**
-.docker/**
-.gitpod
-.vscode/**
-```
-
-simply copy them from the `GameSkeleton` into your game.
-
-(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.)

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

@@ -15,8 +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",
-    "coi-serviceworker": "^0.1.7",
     "cross-env": "^7.0.3",
     "cytoscape": "^3.23.0",
     "cytoscape-elk": "^2.1.0",
@@ -38,18 +36,21 @@
     "remark-gfm": "^3.0.1",
     "remark-math": "^5.1.1",
     "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",
@@ -58,16 +59,21 @@
     "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",
-    "build_server": "cd server && lake build",
+    "production": "cross-env NODE_ENV=production node server/index.mjs",
-    "build_client": "cross-env NODE_ENV=production vite 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",
-    "production": "cross-env NODE_ENV=production node server/index.mjs"
+    "build_nng": "rm -rf ./NNG4 && git clone https://github.com/hhu-adam/NNG4 && docker build ./NNG4 --file ./NNG4/Dockerfile --tag g/hhu-adam/nng4 && rm -rf ./NNG4",
+    "update_lean": "./UPDATE_LEAN.sh"
   },
   "eslintConfig": {
     "extends": [

server/.gitignore

@@ -1,3 +1,3 @@
-.lake
+build
 adam
-lakefile32.olean
+nng

server/GameServer.lean

@@ -1,13 +0,0 @@
-import Lean.Server.Watchdog
-import GameServer.Commands
-import GameServer.Game
-
-Game "TestGame"
-Title "Hello Test"
-
-World "Test"
-Level 1
-
-Statement : 1 = 1 := sorry
-
-MakeGame

server/GameServer/FileWorker.lean

@@ -395,9 +395,26 @@ section Initialization
     fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
     fileMap  := default
 
-  def mkHeaderTask (m : DocumentMeta) (hOut : FS.Stream) (paths : List System.FilePath)
+  def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-      (env : Environment) (opts : Options) (hasWidgets : Bool) :
+      (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) :
       IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
+    -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
+    let out ← IO.Process.output
+      { cwd := levelParams.gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
+    if out.exitCode != 0 then
+      throwServerError s!"Error while running Lake: {out.stderr}"
+
+    -- Make the paths relative to the current directory
+    let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
+    let currentDir ← IO.currentDir
+    let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p
+
+    -- Set the search path
+    Lean.searchPathRef.set paths
+
+    let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
+    -- return (env, paths)
+
     -- use empty header
     let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
       {m.mkInputContext with
@@ -439,32 +456,11 @@ section Initialization
       publishDiagnostics m headerSnap.diagnostics.toArray hOut
       return (headerSnap, srcSearchPath)
 
-  def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-      (levelParams : Game.DidOpenLevelParams) :
-      IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
-    -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
-    let out ← IO.Process.output
-      { cwd := levelParams.gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
-    if out.exitCode != 0 then
-      throwServerError s!"Error while running Lake: {out.stderr}"
-
-    -- Make the paths relative to the current directory
-    let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
-    let currentDir ← IO.currentDir
-    let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p
-
-    -- Set the search path
-    Lean.searchPathRef.set paths
-
-    let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
-    -- return (env, paths)
-    mkHeaderTask m hOut paths env opts hasWidgets
-
   def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
        (levelParams : Game.DidOpenLevelParams) : IO (WorkerContext × WorkerState) := do
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
     let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-      levelParams
+      levelParams initParams
     let cancelTk ← CancelToken.new
     let ctx :=
       { hIn  := i
@@ -500,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
 
@@ -519,8 +515,10 @@ section MessageHandling
 end MessageHandling
 
 section MainLoop
-  partial def mainLoop1 (msg : JsonRpc.Message): GameWorkerM Bool := do
+  partial def mainLoop : GameWorkerM Unit := do
+    let ctx ← read
     let mut st ← StateT.lift get
+    let msg ← ctx.hIn.readLspMessage
     let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
         : IO PendingRequestMap := do
       if (← hasFinished task) then
@@ -543,11 +541,11 @@ section MainLoop
     match msg with
     | Message.request id method (some params) =>
       handleRequest id method (toJson params)
-      return false
+      mainLoop
     | Message.notification "exit" none =>
       let doc := st.doc
       doc.cancelTk.set
-      return true
+      return ()
     | Message.notification "$/game/setInventory" params =>
       let p := (← parseParams Game.SetInventoryParams (toJson params))
       let s ← get
@@ -555,19 +553,11 @@ section MainLoop
       set {s with levelParams := {s.levelParams with
         inventory := p.inventory,
         difficulty := p.difficulty}}
-      return false
+      mainLoop
     | Message.notification method (some params) =>
       handleNotification method (toJson params)
-      return false
+      mainLoop
     | _ => throwServerError "Got invalid JSON-RPC message"
-
-
-partial def mainLoop : GameWorkerM Unit := do
-  let ctx ← read
-  let msg ← ctx.hIn.readLspMessage
-  if not (← mainLoop1 msg) then
-    mainLoop
-
 end MainLoop
 
 def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
@@ -583,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/WasmServer.lean

@@ -1,257 +0,0 @@
-import Lean.Server.Watchdog
-import GameServer.FileWorker
-import GameServer.EnvExtensions
-import GameServer.Game
-
-namespace WasmServer.Watchdog
-open Lean
-open Server
-open Watchdog
-open IO
-open Lsp
-open JsonRpc
-open System.Uri
-
-open MyServer.FileWorker
-
-structure WasmFileState :=
-  fileWorkerState : FileWorker.WorkerState
-  gameWorkerState : GameWorkerState
-  headerTask : Task (Except Error (Snapshots.Snapshot × SearchPath))
-
-structure WasmServerState :=
-  initParams? : Option InitializeParams
-  gameServerState : GameServerState
-  fileState : HashMap String WasmFileState := {}
-
-def wasmSearchPath : SearchPath  := ["/lib", "/gamelib"]
-
-@[export game_make_state]
-unsafe def makeState : IO WasmServerState := do
-  let e ← IO.getStderr
-  try
-    Lean.enableInitializersExecution
-    searchPathRef.set wasmSearchPath
-    let env ← importModules #[
-      { module := `GameServer : Import }
-    ] {} 0
-    let state : GameServerState := {
-      env,
-      game := `TestGame,
-      gameDir := "test",
-      inventory := #[]
-      difficulty := 0
-    }
-    return ⟨none, state, {}⟩
-  catch err =>
-    e.putStrLn s!"Import error: {err}"
-    throw err
-
-def readMessage (s : String) : IO JsonRpc.Message := do
-  let j ← ofExcept (Json.parse s)
-  let m  ← match fromJson? j with
-  | Except.ok (m : JsonRpc.Message) => pure m
-  | Except.error inner => throw $ userError s!"JSON '{j.compress}' did not have the format of a JSON-RPC message.\n{inner}"
-  return m
-
-def readLspRequestAs (s : String) (expectedMethod : String) (α : Type) [FromJson α] : IO (Request α) := do
-  let m ← readMessage s
-  match m with
-  | Message.request id method params? =>
-    if method = expectedMethod then
-      let j := toJson params?
-      match fromJson? j with
-      | Except.ok v => pure $ JsonRpc.Request.mk id expectedMethod (v : α)
-      | Except.error inner => throw $ userError s!"Unexpected param '{j.compress}' for method '{expectedMethod}'\n{inner}"
-    else
-      throw $ userError s!"Expected method '{expectedMethod}', got method '{method}'"
-  | _ => throw $ userError s!"Expected JSON-RPC request, got: '{(toJson m).compress}'"
-
-def initializeServer (id : RequestID) : IO Unit := do
-  let o ← IO.getStdout
-  o.writeLspResponse {
-    id     := id
-    result := {
-      capabilities := mkLeanServerCapabilities
-      serverInfo?  := some {
-        name     := "Lean 4 Game Server"
-        version? := "0.1.1"
-      }
-      : InitializeResult
-    }
-  }
-  return ()
-
-def mkServerContext (state : WasmServerState) : IO ServerContext := do
-  let i ← IO.getStdin
-  let o ← IO.getStdout
-  let e ← IO.getStderr
-  let srcSearchPath ← searchPathRef.get
-  let references ← IO.mkRef (← loadReferences)
-  let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
-  let workerPath := "no-worker-path"
-  let some initParams := state.initParams?
-    | throwServerError "no yet initialized"
-  return {
-    hIn            := i
-    hOut           := o
-    hLog           := e
-    args           := []
-    fileWorkersRef := fileWorkersRef
-    initParams
-    workerPath
-    srcSearchPath
-    references
-  }
-
-def runGameServerM (state : WasmServerState) (x : GameServerM α) : IO (α × WasmServerState) := do
-  let (res, gameServerState) ← ReaderT.run
-      (StateT.run x state.gameServerState)
-      (← mkServerContext state)
-  return (res, {state with gameServerState})
-
-def mkWorkerContext (state : WasmServerState) (headerTask : Task (Except Error (Snapshots.Snapshot × SearchPath))) :
-    IO FileWorker.WorkerContext := do
-  let i ← IO.getStdin
-  let o ← IO.getStdout
-  let e ← IO.getStderr
-  let some initParams := state.initParams?
-    | throwServerError "no yet initialized"
-  let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
-  return {
-    hIn  := i
-    hOut := o
-    hLog := e
-    headerTask := headerTask
-    initParams := initParams
-    clientHasWidgets
-  }
-
-def runGameWorkerM (state : WasmServerState) (fileState : WasmFileState) (x : GameWorkerM α) :
-    IO (α × WasmFileState) := do
-  let s := fileState.fileWorkerState
-  let ctx ← mkWorkerContext state fileState.headerTask
-  let ((res, gameWorkerState), s) ← StateRefT'.run (s := s) <| ReaderT.run (r := ctx) <|
-      StateT.run (s := fileState.gameWorkerState) <| x
-  let fileState := {fileState with gameWorkerState := gameWorkerState, fileWorkerState := s}
-  return (res, fileState)
-
-def parseParams {paramType : Type} [FromJson paramType] (params : Json) : IO paramType :=
-  match fromJson? params with
-  | Except.ok parsed => pure parsed
-  | Except.error inner => throwServerError s!"Got param with wrong structure: {params.compress}\n{inner}"
-
-def requestWorkerUri (method : String) (params : Json) : IO (Option DocumentUri) := do
-  if method == "$/lean/rpc/connect" then
-    let ps : Lsp.RpcConnectParams ← parseParams params
-    pure <| fileSource ps
-  else match (← routeLspRequest method params) with
-    | Except.error e =>
-      throwServerError e.message
-    | Except.ok uri => pure uri
-
-open FileWorker in
-def handleDidOpen (params : DidOpenTextDocumentParams) (state : WasmServerState) : IO WasmServerState := do
-  let some initParams := state.initParams?
-    | throwServerError "no yet initialized"
-  let (_, state) ← runGameServerM state do
-    let some lvl ← GameServer.getLevelByFileName? initParams
-        ((System.Uri.fileUriToPath? params.textDocument.uri).getD params.textDocument.uri |>.toString)
-      | throwServerError s!"Level not found: {params.textDocument.uri} | {initParams.rootUri?}"
-
-    let env ← importModules #[
-      { module := lvl.module : Import }
-    ] {} 0
-
-    (← getStderr).putStr "Import for level completed"
-
-    let doc := params.textDocument
-    let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
-    let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
-
-    let (headerStx, headerTask) ← mkHeaderTask meta (← getStdout) wasmSearchPath env {} clientHasWidgets
-    let cancelTk ← CancelToken.new
-
-    let levelParams := {
-      uri := meta.uri
-      gameDir := state.gameServerState.gameDir
-      levelModule := lvl.module
-      tactics := lvl.tactics.tiles
-      lemmas := lvl.lemmas.tiles
-      definitions := lvl.definitions.tiles
-      inventory := state.gameServerState.inventory
-      difficulty := state.gameServerState.difficulty
-      statementName := lvl.statementName
-      : Game.DidOpenLevelParams
-    }
-
-    let ctx ← mkWorkerContext state headerTask
-    let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk levelParams ctx (startAfterMs := 0)
-      | Except.error e   => throw (e : ElabTaskError))
-    let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
-
-
-    let s : WasmFileState := {
-      fileWorkerState := {
-        doc             := doc
-        initHeaderStx   := headerStx
-        pendingRequests := RBMap.empty
-        rpcSessions     := RBMap.empty
-      }
-      gameWorkerState := { levelParams }
-      headerTask
-    }
-    let fileState := state.fileState.insert params.textDocument.uri s
-    return {state with fileState}
-  return state
-
-@[export game_send_message]
-unsafe def sendMessage (s : String) (state : WasmServerState) : IO WasmServerState := do
-  let e ← IO.getStderr
-  try
-    let m ← readMessage s
-    match m with
-    | Message.request id "initialize" (some params) =>
-      let p : InitializeParams ← parseParams (toJson params)
-      initializeServer id
-      let p := {p with rootUri? := some (toString state.gameServerState.game)}
-      return {state with initParams? := some p}
-    | _ =>
-      let (isGameEv, state) ← runGameServerM state (Game.handleServerEvent (.clientMsg m))
-      if isGameEv then
-        return state
-      else
-        match m with
-        | Message.notification method (some params) =>
-            let handle := (fun α [FromJson α] (handler : α → WasmServerState → IO WasmServerState)
-              => parseParams (toJson params) >>= (handler · state))
-            match method with --TODO
-            | "textDocument/didOpen"            => handle DidOpenTextDocumentParams handleDidOpen
-            -- | "textDocument/didChange"          => handle DidChangeTextDocumentParams handleDidChange
-            -- | "textDocument/didClose"           => handle DidCloseTextDocumentParams handleDidClose
-            -- | "workspace/didChangeWatchedFiles" => handle DidChangeWatchedFilesParams handleDidChangeWatchedFiles
-            -- | "$/cancelRequest"                 => handle CancelParams handleCancelRequest
-            -- | "$/lean/rpc/connect"              => handle RpcConnectParams (forwardNotification method)
-            -- | "$/lean/rpc/release"              => handle RpcReleaseParams (forwardNotification method)
-            -- | "$/lean/rpc/keepAlive"            => handle RpcKeepAliveParams (forwardNotification method)
-            | _ => return state
-        | Message.request id method (some params) =>
-          let some uri ← requestWorkerUri method (toJson params)
-            | throwServerError s!"Could not find Uri for request: {method}"
-          let some fileState := state.fileState.find? uri
-            | throwServerError s!"File not open: {uri}"
-          let (_, fileState) ← runGameWorkerM state fileState do
-            MyServer.FileWorker.mainLoop1 m
-          let fileState := state.fileState.insert uri fileState
-          return {state with fileState}
-        | Message.responseError _ _ e .. =>
-          throwServerError s!"Unhandled response error: {e}"
-        | _ => throwServerError "Got invalid JSON-RPC message"
-        -- match m with
-        -- | _ =>
-        --   e.putStrLn s!"Expected JSON-RPC request, got: '{(toJson m).compress}'"
-        --   return state
-  catch err =>
-    e.putStrLn s!"Server error: {err}"
-    return state

server/Main.lean

@@ -1,10 +1,5 @@
 import GameServer.FileWorker
 import GameServer.Watchdog
-import GameServer.WasmServer
-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/lakefile.lean

@@ -3,7 +3,6 @@ open Lake DSL
 
 package GameServer
 
-@[default_target]
 lean_lib GameServer
 
 @[default_target]

server/lakefile32.lean

@@ -1,15 +0,0 @@
-import Lake
-open Lake DSL
-
-package GameServer {
-  buildDir := ".lake/build32"
-}
-
-@[default_target]
-lean_lib GameServer
-
-@[default_target]
-lean_exe gameserver {
-  root := `Main
-  supportInterpreter := true
-}

server/lean-toolchain

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

server/main.c

@@ -1,58 +0,0 @@
-#include <stdio.h>
-#include <lean/lean.h>
-
-extern lean_object* game_send_message(lean_object*, lean_object*, lean_object*);
-extern lean_object* game_make_state(lean_object*);
-
-// see https://leanprover.github.io/lean4/doc/dev/ffi.html#initialization
-extern void lean_initialize_runtime_module();
-extern void lean_initialize();
-extern void lean_io_mark_end_initialization();
-extern lean_object * initialize_GameServer_WasmServer(uint8_t builtin, lean_object *);
-
-lean_object * state;
-lean_object * io_world;
-
-
-void main() {
-  lean_initialize_runtime_module();
-  lean_initialize();
-  lean_object * res;
-  // use same default as for Lean executables
-  uint8_t builtin = 1;
-  io_world = lean_io_mk_world();
-  res = initialize_GameServer_WasmServer(builtin, io_world);
-  if (lean_io_result_is_ok(res)) {
-      lean_dec(res);
-  } else {
-      lean_io_result_show_error(res);
-      lean_dec(res);
-      return;  // do not access Lean declarations if initialization failed
-  }
-  lean_init_task_manager();
-  lean_io_mark_end_initialization();
-
-  res = game_make_state(io_world);
-  if (lean_io_result_is_ok(res)) {
-    state = lean_io_result_get_value(res);
-    lean_inc(state);
-    lean_dec(res);
-  } else {
-    lean_io_result_show_error(res);
-    lean_dec(res);
-    return;  // do not access Lean declarations if initialization failed
-  }
-}
-
-void send_message(char* msg){
-  lean_object * s = lean_mk_string(msg);
-  lean_object * res = game_send_message(s, state, io_world);
-  if (lean_io_result_is_ok(res)) {
-    state = lean_io_result_get_value(res);
-    lean_inc(state);
-    lean_dec(res);
-  } else {
-    lean_io_result_show_error(res);
-    lean_dec(res);
-  }
-}

vite.config.ts

@@ -1,43 +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({
-  plugins: [
-    react(),
-    svgr({
-      svgrOptions: {
-        // svgr options
-      },
-    }),
-    viteStaticCopy({
-      targets: [
-        {
-          src: 'node_modules/@leanprover/infoview/dist/*.production.min.js',
-          dest: '.'
-        },
-        {
-          src: 'node_modules/coi-serviceworker/coi-serviceworker.js',
-          dest: '.'
-        }
-      ]
-    })
-  ],
-  publicDir: "client/public",
-  server: {
-    port: 3000,
-    proxy: {
-      '/websocket': {
-        target: 'ws://localhost:8080',
-        ws: true
-      },
-    }
-  },
-  resolve: {
-    alias: {
-      path: "path-browserify",
-    },
-  },
-})

wasm.sh

@@ -1,37 +0,0 @@
-#!/bin/bash
-
-cd server
-
-mkdir -p .lake/toolchains
-if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst  ]
-then
-    wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_wasm32.tar.zst
-    tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst -C .lake/toolchains
-fi
-if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst  ]
-then
-    wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_x86.tar.zst
-    tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst -C .lake/toolchains
-fi
-
-# Linking will fail, but that's ok. We only need the c files.
-.lake/toolchains/lean-4.3.0-rc2-linux_x86/bin/lake build -f=lakefile32.lean
-
-
-lake build
-
-
-OUT_DIR=../client/public
-LEAN_SYSROOT=.lake/toolchains/lean-4.3.0-rc2-linux_wasm32
-LEAN_LIBDIR=$LEAN_SYSROOT/lib/lean
-
-emcc -o $OUT_DIR/server.js main.c -I $LEAN_SYSROOT/include -L $LEAN_LIBDIR .lake/build/ir/GameServer/*.c -lInit -lLean -lleancpp -lleanrt \
-  -sFORCE_FILESYSTEM -lnodefs.js -s EXIT_RUNTIME=0 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto \
-  -sPTHREAD_POOL_SIZE_STRICT=2 \
-  --preload-file "${LEAN_SYSROOT}/lib/lean/Init"@/lib/Init \
-  --preload-file "${LEAN_SYSROOT}/lib/lean/Init.olean"@/lib/Init.olean \
-  --preload-file "${LEAN_SYSROOT}/lib/lean/Init.ilean"@/lib/Init.ilean \
-  --preload-file "${LEAN_SYSROOT}/lib/lean/Lean"@/lib/Lean \
-  --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.olean"@/lib/Lean.olean \
-  --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.ilean"@/lib/Lean.ilean \
-  --preload-file "./.lake/build32/lib"@/gamelib