work on network interruption errors

.gitignore

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

NOTES.md

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

client/public/index.html

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

client/src/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/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>
+);

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,7 +15,6 @@
     "@reduxjs/toolkit": "^1.9.1",
     "@types/cytoscape": "^3.19.9",
     "@types/react-router-dom": "^5.3.3",
-    "@vitejs/plugin-react-swc": "^3.4.0",
     "cross-env": "^7.0.3",
     "cytoscape": "^3.23.0",
     "cytoscape-elk": "^2.1.0",
@@ -37,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",
@@ -57,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/GameServer/FileWorker.lean

@@ -496,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
 
@@ -573,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/Main.lean

@@ -1,9 +1,5 @@
 import GameServer.FileWorker
 import GameServer.Watchdog
-import GameServer.Commands
-
--- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`
--- should we have a different solution?
 
 unsafe def main : List String → IO UInt32 := fun args => do
   let e ← IO.getStderr

server/lean-toolchain

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

vite.config.ts

@@ -1,39 +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: '.'
-        }
-      ]
-    })
-  ],
-  publicDir: "client/public",
-  server: {
-    port: 3000,
-    proxy: {
-      '/websocket': {
-        target: 'ws://localhost:8080',
-        ws: true
-      },
-    }
-  },
-  resolve: {
-    alias: {
-      path: "path-browserify",
-    },
-  },
-})