change to vite

.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
-  // editor, model or uri might be null if connection is broken
-  const rpcSess = useRpcSessionAtPos({uri: editor?.getModel()?.uri?.toString() ?? '', line: 0, character: 0})
+  const rpcSess = useRpcSessionAtPos({uri: uri, line: 0, character: 0})
+
+  /** Delete all proof lines starting from a given line.
+  * Note that the first line (i.e. deleting everything) is `1`!
+  */
+  function deleteProof(line: number) {
+    return (ev) => {
+      let deletedChat: Array<GameHint> = []
+      proof.slice(line).map((step, i) => {
+        // Only add these hidden hints to the deletion stack which were visible
+        deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
+      })
+      setDeletedChat(deletedChat)
+
+      editor.executeEdits("typewriter", [{
+        range: monaco.Selection.fromPositions(
+          { lineNumber: line, column: 1 },
+          editor.getModel().getFullModelRange().getEndPosition()
+        ),
+        text: '',
+        forceMoveMarkers: false
+      }])
+      setSelectedStep(undefined)
+      setTypewriterInput(proof[line].command)
+      ev.stopPropagation()
+    }
+  }
 
   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.
-  React.useEffect(() => {
+   // Scroll to the end of the proof if it is updated.
+   React.useEffect(() => {
     if (proof?.length > 1) {
       proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
     } else {

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 uri = model?.uri?.toString()
+  const model = editor.getModel()
+  const uri = model.uri.toString()
 
   const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
   const [processing, setProcessing] = useState(false)
@@ -91,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
-  //  * `TypewriterInterface`.
-  //  */
-  // const handleUndo = () => {
-  //   const endPos = editor.getModel().getFullModelRange().getEndPosition()
-  //   let range
-  //   console.log(endPos.column)
-  //   if (endPos.column === 1) {
-  //     range = monaco.Selection.fromPositions(
-  //       new monaco.Position(endPos.lineNumber - 1, 1),
-  //       endPos
-  //     )
-  //   } else {
-  //     range = monaco.Selection.fromPositions(
-  //       new monaco.Position(endPos.lineNumber, 1),
-  //       endPos
-  //     )
-  //   }
-  //   editor.executeEdits("undo-button", [{
-  //     range,
-  //     text: "",
-  //     forceMoveMarkers: false
-  //   }]);
-  // }
+  /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside
+   * `TypewriterInterface`.
+   */
+  const handleUndo = () => {
+    const endPos = editor.getModel().getFullModelRange().getEndPosition()
+    let range
+    console.log(endPos.column)
+    if (endPos.column === 1) {
+      range = monaco.Selection.fromPositions(
+        new monaco.Position(endPos.lineNumber - 1, 1),
+        endPos
+      )
+    } else {
+      range = monaco.Selection.fromPositions(
+        new monaco.Position(endPos.lineNumber, 1),
+        endPos
+      )
+    }
+    editor.executeEdits("undo-button", [{
+      range,
+      text: "",
+      forceMoveMarkers: false
+    }]);
+  }
 
   // Select and highlight proof steps and corresponding hints
   // TODO: with the new design, there is no difference between the introduction and
@@ -294,31 +296,28 @@ function PlayableLevel({impressum, setImpressum}) {
       setTypewriterMode(false)
 
       if (editor) {
-        let model = editor.getModel()
-        if (model) {
-          let code = model.getLinesContent()
+        let code = editor.getModel().getLinesContent()
 
-          // console.log(`insert. code: ${code}`)
-          // console.log(`insert. join: ${code.join('')}`)
-          // console.log(`insert. trim: ${code.join('').trim()}`)
-          // console.log(`insert. length: ${code.join('').trim().length}`)
-          // console.log(`insert. range: ${editor.getModel().getFullModelRange()}`)
+        // console.log(`insert. code: ${code}`)
+        // console.log(`insert. join: ${code.join('')}`)
+        // console.log(`insert. trim: ${code.join('').trim()}`)
+        // console.log(`insert. length: ${code.join('').trim().length}`)
+        // console.log(`insert. range: ${editor.getModel().getFullModelRange()}`)
 
 
-          // TODO: It does seem that the template is always indented by spaces.
-          // This is a hack, assuming there are exactly two.
-          if (!code.join('').trim().length) {
-            console.debug(`inserting template:\n${level.data.template}`)
-            // TODO: This does not work! HERE
-            // Probably overwritten by a query to the server
-            editor.executeEdits("template-writer", [{
-              range: model.getFullModelRange(),
-              text: level.data.template + `\n`,
-              forceMoveMarkers: true
-            }])
-          } else {
-            console.debug(`not inserting template.`)
-          }
+        // TODO: It does seem that the template is always indented by spaces.
+        // This is a hack, assuming there are exactly two.
+        if (!code.join('').trim().length) {
+          console.debug(`inserting template:\n${level.data.template}`)
+          // TODO: This does not work! HERE
+          // Probably overwritten by a query to the server
+          editor.executeEdits("template-writer", [{
+            range: editor.getModel().getFullModelRange(),
+            text: level.data.template + `\n`,
+            forceMoveMarkers: true
+          }])
+        } else {
+          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) {
-      let model = editor.getModel()
-      if (model) {
-        if (typewriterMode) {
-          // typewriter gets enabled
-          let code = model.getLinesContent().filter(line => line.trim())
-          editor.executeEdits("typewriter", [{
-            range: model.getFullModelRange(),
-            text: code.length ? code.join('\n') + '\n' : '',
-            forceMoveMarkers: true
-          }])
-
-          // let endPos = model.getFullModelRange().getEndPosition()
-          // if (model.getLineContent(endPos.lineNumber).trim() !== "") {
-          //   editor.executeEdits("typewriter", [{
-          //     range: monaco.Selection.fromPositions(endPos, endPos),
-          //     text: "\n",
-          //     forceMoveMarkers: true
-          //   }]);
-          // }
-          // let endPos = model.getFullModelRange().getEndPosition()
-          // let currPos = editor.getPosition()
-          // if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) {
-          //   // This is not a position that would naturally occur from Typewriter, reset:
-          //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
-          // }
-        } else {
-          // typewriter gets disabled
-          // delete last input attempt from command line
-          editor.executeEdits("typewriter", [{
-            range: editor.getSelection(),
-            text: "",
-            forceMoveMarkers: false
-          }]);
-          editor.focus()
-        }
-      }
-
-
+    if (!typewriterMode) {
+      // 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()))
-        editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
-        editor.setModel(model)
-        if (initialSelections) {
-          console.debug("Initial Selection: ", initialSelections)
-          // BUG: Somehow I get an `invalid arguments` bug here
-          // editor.setSelections(initialSelections)
-        }
+      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
+      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
+      editor.setModel(model)
+      if (initialSelections) {
+        console.debug("Initial Selection: ", initialSelections)
+        // BUG: Somehow I get an `invalid arguments` bug here
+        // editor.setSelections(initialSelections)
+      }
 
-        return () => {
-          editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
-          model.dispose(); }
+      return () => {
+        editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
       }
     }
   }, [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 abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+      const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
+      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
 
-        return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
-      }
+      return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
     }
   }, [editor, connection, leanClientStarted])
 
@@ -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%;

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",
-    "webpack": "^5.75.0",
-    "webpack-cli": "^4.10.0",
-    "webpack-dev-server": "^4.11.1",
-    "webpack-shell-plugin-next": "^2.3.1"
+    "url-loader": "^4.1.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",
-    "build": "cross-env NODE_ENV=production webpack",
-    "production": "cross-env NODE_ENV=production node server/index.mjs",
-    "build_robo": "rm -rf ./Robo && git clone https://github.com/hhu-adam/Robo && docker build ./Robo --file ./Robo/Dockerfile --tag g/hhu-adam/robo && rm -rf ./Robo",
-    "build_nng": "rm -rf ./NNG4 && git clone https://github.com/hhu-adam/NNG4 && docker build ./NNG4 --file ./NNG4/Dockerfile --tag g/hhu-adam/nng4 && rm -rf ./NNG4",
-    "update_lean": "./UPDATE_LEAN.sh"
+    "start_client": "cross-env NODE_ENV=development vite --host",
+    "build": "npm run build_server && npm run build_client",
+    "build_server": "cd server && lake build",
+    "build_client": "cross-env NODE_ENV=production vite build",
+    "production": "cross-env NODE_ENV=production node server/index.mjs"
   },
   "eslintConfig": {
     "extends": [

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",
+    },
+  },
+})