fix redirect from landing page in dev container #145

.gitignore

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

NOTES.md

@@ -15,9 +15,6 @@ 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 "."
 ```
 
 
@@ -146,12 +143,6 @@ Activate config:
 ```
 
 
-## Install `unzip` for Importing Docker Images
-
-```
-sudo apt-get install unzip
-```
-
 ## Install bubblewrap (bwrap)
 ```
 sudo apt-get install bubblewrap

client/src/components/infoview/main.tsx

@@ -1,7 +1,6 @@
 /* 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';
@@ -328,17 +327,6 @@ 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>
@@ -350,51 +338,19 @@ 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 { showHelp, setShowHelp } = React.useContext(DeletedChatContext)
+  const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
   const {mobile} = React.useContext(MobileContext)
   const { proof } = React.useContext(ProofContext)
+  const { setTypewriterInput } = React.useContext(InputModeContext)
   const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
 
   const proofPanelRef = React.useRef<HTMLDivElement>(null)
@@ -402,9 +358,33 @@ export function TypewriterInterface({props}) {
   // const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
   // const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
 
-  // rpc session
+  const rpcSess = useRpcSessionAtPos({uri: uri, line: 0, character: 0})
-  // editor, model or uri might be null if connection is broken
+
-  const rpcSess = useRpcSessionAtPos({uri: editor?.getModel()?.uri?.toString() ?? '', line: 0, character: 0})
+  /** Delete all proof lines starting from a given line.
+  * Note that the first line (i.e. deleting everything) is `1`!
+  */
+  function deleteProof(line: number) {
+    return (ev) => {
+      let deletedChat: Array<GameHint> = []
+      proof.slice(line).map((step, i) => {
+        // Only add these hidden hints to the deletion stack which were visible
+        deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
+      })
+      setDeletedChat(deletedChat)
+
+      editor.executeEdits("typewriter", [{
+        range: monaco.Selection.fromPositions(
+          { lineNumber: line, column: 1 },
+          editor.getModel().getFullModelRange().getEndPosition()
+        ),
+        text: '',
+        forceMoveMarkers: false
+      }])
+      setSelectedStep(undefined)
+      setTypewriterInput(proof[line].command)
+      ev.stopPropagation()
+    }
+  }
 
   function toggleSelectStep(line: number) {
     return (ev) => {
@@ -419,8 +399,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,15 +91,11 @@ 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}))
       )
@@ -162,7 +158,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)
@@ -170,7 +166,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
@@ -189,7 +185,6 @@ 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([])
@@ -200,7 +195,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
       editor.executeEdits("typewriter", [{
         range: monaco.Selection.fromPositions(
           pos,
-          model.getFullModelRange().getEndPosition()
+          editor.getModel().getFullModelRange().getEndPosition()
         ),
         text: typewriterInput.trim() + "\n",
         forceMoveMarkers: false
@@ -209,7 +204,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     }
 
     editor.setPosition(pos)
-  }, [typewriterInput, editor, model])
+  }, [typewriterInput, editor])
 
   useEffect(() => {
     if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) {
@@ -225,14 +220,12 @@ 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(model.getFullModelRange().getEndPosition())
+        editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
       }
     } else {
       // console.debug(`expected uri: ${uri}, got: ${params.uri}`)
@@ -241,7 +234,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, editor, model]);
+  }, [uri]);
 
   useEffect(() => {
     const myEditor = monaco.editor.create(inputRef.current!, {
@@ -311,8 +304,10 @@ 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,7 +6,6 @@ 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';
@@ -115,32 +114,16 @@ 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>
-      <DocContent doc={doc} />
+    <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>
   </div>
 }
 

client/src/components/level.tsx

@@ -237,6 +237,8 @@ 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}))
   }
@@ -252,30 +254,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
@@ -294,31 +296,28 @@ function PlayableLevel({impressum, setImpressum}) {
       setTypewriterMode(false)
 
       if (editor) {
-        let model = editor.getModel()
+        let code = editor.getModel().getLinesContent()
-        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: model.getFullModelRange(),
+            range: editor.getModel().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 {
@@ -336,49 +335,17 @@ function PlayableLevel({impressum, setImpressum}) {
     setShowHelp(new Set(selectHelp(gameId, worldId, levelId)(store.getState())))
   }, [gameId, worldId, levelId])
 
-  // switching editor mode
   useEffect(() => {
-    if (editor) {
+    if (!typewriterMode) {
-      let model = editor.getModel()
+      // Delete last input attempt from command line
-      if (model) {
+      editor.executeEdits("typewriter", [{
-        if (typewriterMode) {
+        range: editor.getSelection(),
-          // typewriter gets enabled
+        text: "",
-          let code = model.getLinesContent().filter(line => line.trim())
+        forceMoveMarkers: false
-          editor.executeEdits("typewriter", [{
+      }]);
-            range: model.getFullModelRange(),
+      editor.focus()
-            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()
-        }
-      }
-
-
     }
-  }, [editor, typewriterMode])
+  }, [typewriterMode])
 
   useEffect(() => {
     // Forget whether hidden hints are displayed for steps that don't exist yet
@@ -396,6 +363,33 @@ 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}}>
@@ -489,9 +483,33 @@ 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)
@@ -586,19 +604,17 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
       if (!model) {
         model = monaco.editor.createModel(initialCode, 'lean4', uri)
       }
-      if (model) { // in case of broken pipe, this remains null
+      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
-        model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
+      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
-        editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
+      editor.setModel(model)
-        editor.setModel(model)
+      if (initialSelections) {
-        if (initialSelections) {
+        console.debug("Initial Selection: ", initialSelections)
-          console.debug("Initial Selection: ", initialSelections)
+        // BUG: Somehow I get an `invalid arguments` bug here
-          // BUG: Somehow I get an `invalid arguments` bug here
+        // editor.setSelections(initialSelections)
-          // 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])
@@ -608,16 +624,14 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
     if (editor && leanClientStarted) {
 
       let model = monaco.editor.getModel(uri)
-      if (model) {
+      infoviewApi.serverRestarted(leanClient.initializeResult)
-        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])
 
@@ -643,7 +657,7 @@ function useLoadWorldFiles(worldId) {
           models.push(monaco.editor.createModel(code, 'lean4', uri))
         }
       }
-      return () => { for (let model of models) { try {model.dispose()} catch {console.log(`failed to dispose model ${model}`)}} }
+      return () => { for (let model of models) { model.dispose() } }
     }
   }, [gameInfo.data, worldId])
 }

client/src/css/app.css

@@ -42,12 +42,6 @@ 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,29 +1,45 @@
-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 {
+import type { RouteObject } from "react-router"
-  createHashRouter,
+import { createHashRouter, RouterProvider, Route, redirect } from "react-router-dom"
-  RouterProvider,
+import ErrorPage from './components/error_page'
-  Route,
+import Welcome from './components/welcome'
-} from "react-router-dom";
+import LandingPage from './components/landing_page'
-import ErrorPage from './components/error_page';
+import Level from './components/level'
-import Welcome from './components/welcome';
+import { monacoSetup } from 'lean4web/client/src/monacoSetup'
-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,
   {
-    path: "/",
+    // For backwards compatibility
-    element: <LandingPage />,
-  },
-  {
     path: "/game/nng",
     loader: () => redirect("/g/hhu-adam/NNG4")
   },

client/src/index_local.tsx

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

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

index.html

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

package.json

@@ -15,6 +15,7 @@
     "@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",
@@ -36,21 +37,18 @@
     "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",
@@ -59,21 +57,16 @@
     "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 webpack-dev-server --hot",
+    "start_client": "cross-env NODE_ENV=development vite --host",
-    "build": "cross-env NODE_ENV=production webpack",
+    "build": "npm run build_server && npm run build_client",
-    "production": "cross-env NODE_ENV=production node server/index.mjs",
+    "build_server": "cd server && lake build",
-    "build_robo": "rm -rf ./Robo && git clone https://github.com/hhu-adam/Robo && docker build ./Robo --file ./Robo/Dockerfile --tag g/hhu-adam/robo && rm -rf ./Robo",
+    "build_client": "cross-env NODE_ENV=production vite build",
-    "build_nng": "rm -rf ./NNG4 && git clone https://github.com/hhu-adam/NNG4 && docker build ./NNG4 --file ./NNG4/Dockerfile --tag g/hhu-adam/nng4 && rm -rf ./NNG4",
+    "production": "cross-env NODE_ENV=production node server/index.mjs"
-    "update_lean": "./UPDATE_LEAN.sh"
   },
   "eslintConfig": {
     "extends": [

server/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⟩
+      updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
 
 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⟩
+  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try

server/Main.lean

@@ -1,5 +1,9 @@
 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.1.0
+leanprover/lean4:v4.2.0

vite.config.ts

@@ -0,0 +1,39 @@
+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",
+    },
+  },
+})