error: Tried to spawn a new thread, but

.env

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

.github/workflows/build.yml

@@ -5,17 +5,7 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-      - name: install elan
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v3
       - uses: actions/setup-node@v3
-      - name: print lean and lake versions
-        run: |
-          lean --version
-          lake --version
       - run: npm install
       - run: npm run build

.gitignore

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

README.md

@@ -8,27 +8,21 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular,
 
 * Step 5: [How to Run Games Locally](doc/running_locally.md)
 * Step 7: [How to Update an existing Game](doc/update_game.md)
-* Step 8: [How to Publishing a Game](doc/publish_game.md)
+
+### Publishing a Game
+
+We encourage anybody to have games hosted on our [Lean Game Server](https://adam.math.hhu.de) for anybody to play. For that you simply need to contact us with the link to your game repo. We are also happy to add work-in-progress games and games in any language.
+
+For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).
 
 ## Documentation
 
-The documentation is very much work in progress but the linked documentation here
-should be up-to-date:
+The documentation for the game engine itself is still missing, but there is [Creating a Game](doc/create_game.md) explaining the API to create a game.
 
-### Game creation API
+Some documentation:
 
-- [Creating a Game](doc/create_game.md): **the main document to consult**.
-- [More about Hints](doc/hints.md): describes the `Hint` and `Branch` tactic.
-
-### Frontend API
-
-* [How to Run Games Locally](doc/running_locally.md): play a game on your computer
-* [How to Update an existing Game](doc/update_game.md): update to a new lean version
-* [How to Publishing a Game](doc/publish_game.md): load your game to adam.math.hhu.de for others to play
-
-### Backend
-
-not written yet
+- [NPM Scripts](doc/npm_scripts.md)
+- [Old documentation](doc/DOCUMENTATION.md)
 
 ## Contributing
 
@@ -42,5 +36,5 @@ Providing the use access to a Lean instance running on the server is a severe se
 
 The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
 (NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
-by Kevin Buzzard and Mohammad Pedramfar.
+of Kevin Buzzard and Mohammad Pedramfar.
 The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).

client/public/worker.js

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

client/src/app.tsx

@@ -10,7 +10,6 @@ import './css/reset.css';
 import './css/app.css';
 import { MobileContext } from './components/infoview/context';
 import { useWindowDimensions } from './window_width';
-import { connection } from './connection';
 
 export const GameIdContext = React.createContext<string>(undefined);
 
@@ -20,10 +19,6 @@ function App() {
   const {width, height} = useWindowDimensions()
   const [mobile, setMobile] = React.useState(width < 800)
 
-  React.useEffect(() => {
-    connection.startLeanClient(gameId);
-  }, [gameId])
-
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>

client/src/components/hints.tsx

@@ -1,7 +1,6 @@
 import { GameHint } from "./infoview/rpc_api";
 import * as React from 'react';
 import Markdown from './markdown';
-import { ProofStep } from "./infoview/context";
 
 export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
   return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
@@ -44,24 +43,3 @@ export function DeletedHints({hints} : {hints: GameHint[]}) {
     {hiddenHints.map((hint, i) => <DeletedHint key={`deleted-hidden-hint-${i}`} hint={hint}/>)}
   </>
 }
-
-/** Filter hints to not show consequtive identical hints twice.
- *
- * This function takes a `ProofStep[]` and extracts the hints in form of an
- * element of type `GameHint[][]` where it removes hints that are identical to hints
- * appearing in the previous step. Hidden hints are not filtered.
- *
- * This effectively means we prevent consequtive identical hints from being shown.
- */
-export function filterHints(proof: ProofStep[]): GameHint[][] {
-  return proof.map((step, i) => {
-    if (i == 0){
-      return step.hints
-    } else {
-      // TODO: Writing all fields explicitely is somewhat fragile to changes, is there a
-      // good way to shallow-compare objects?
-      return step.hints.filter((hint) => hint.hidden ||
-        (proof[i-1].hints.find((x) => (x.text == hint.text && x.hidden == hint.hidden)) === undefined))
-    }
-  })
-}

client/src/components/infoview/main.tsx

@@ -34,7 +34,7 @@ import { Button } from '../button';
 import { CircularProgress } from '@mui/material';
 import { GameHint } from './rpc_api';
 import { store } from '../../state/store';
-import { Hints, filterHints } from '../hints';
+import { Hints } from '../hints';
 
 /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
  * always present, or the monaco editor cannot start.
@@ -156,7 +156,7 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
 
   const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
 
-  console.debug(`template: ${props.data?.template}`)
+  console.debug(`template: ${props.data.template}`)
 
   // React.useEffect (() => {
   //   if (props.data.template) {
@@ -347,7 +347,6 @@ export function TypewriterInterface({props}) {
   const uri = model.uri.toString()
 
   const [disableInput, setDisableInput] = React.useState<boolean>(false)
-  const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
   const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
   const {mobile} = React.useContext(MobileContext)
   const { proof } = React.useContext(ProofContext)
@@ -367,9 +366,9 @@ export function TypewriterInterface({props}) {
   function deleteProof(line: number) {
     return (ev) => {
       let deletedChat: Array<GameHint> = []
-      filterHints(proof).slice(line).map((hintsAtStep, i) => {
+      proof.slice(line).map((step, i) => {
         // Only add these hidden hints to the deletion stack which were visible
-        deletedChat = [...deletedChat, ...hintsAtStep.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
+        deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
       })
       setDeletedChat(deletedChat)
 
@@ -456,17 +455,6 @@ export function TypewriterInterface({props}) {
 
   let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false
 
-
-  useServerNotificationEffect("$/game/loading", (params : any) => {
-    if (params.kind == "loadConstants") {
-      setLoadingProgress(params.counter/100*50)
-    } else if (params.kind == "finalizeExtensions") {
-      setLoadingProgress(50 + params.counter/150*50)
-    } else {
-      console.error(`Unknown loading kind: ${params.kind}`)
-    }
-  })
-
   return <div className="typewriter-interface">
     <RpcContext.Provider value={rpcSess}>
     <div className="content">
@@ -533,7 +521,7 @@ export function TypewriterInterface({props}) {
                 }
               </div>
             }
-          </> : <CircularProgress variant="determinate" value={loadingProgress} />
+          </> : <CircularProgress />
         }
       </div>
     </div>

client/src/components/inventory.tsx

@@ -5,7 +5,7 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faLock, faBan } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from '../app';
 import Markdown from './markdown';
-import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery, WorldOverview } from '../state/api';
+import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
 import { selectDifficulty, selectInventory } from '../state/progress';
 import { store } from '../state/store';
 import { useSelector } from 'react-redux';
@@ -37,79 +37,6 @@ export function Inventory({levelInfo, openDoc, enableAll=false} :
   )
 }
 
-export function OverviewInventory({data, openDoc, enableAll=false, showOverview=true} :
-  {
-    data: WorldOverview[],
-    openDoc: (props: {name: string, type: string}) => void,
-    enableAll?: boolean,
-    showOverview?: boolean
-  }) {
-
-  const gameId = React.useContext(GameIdContext)
-  const difficulty = useSelector(selectDifficulty(gameId))
-  const [tab, setTab] = useState<string>()
-  let inv: string[] = selectInventory(gameId)(store.getState())
-
-  let levelInfo : InventoryOverview = {
-    tactics : data ? data.map(world => (world.tactics.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [],
-    lemmas : data ? data.map(world => (world.lemmas.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [],
-    definitions : data ? data.map(world => (world.definitions.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [],
-    lemmaTab: null,
-  }
-
-  return (
-    <>
-      <Inventory levelInfo={levelInfo} openDoc={openDoc} enableAll={enableAll}/>
-      {showOverview &&
-        <div className="inventory">
-          {data && <>
-            <h2>Overviews</h2>
-            <div className="tab-bar">
-              {data.map(world => {
-                return <div key={`category-${world.world}`} className={`tab ${world.world == tab ? "active": ""}`} onClick={() => { setTab((tab == world.world) ? null : world.world) }}>{world.world}</div>
-              })}
-            </div>
-            <div className="inventory-list">
-              {/* TODO: a bit hacky, do we need to redesign inventory completely and provide it in a better order? */}
-              {data.map(world => {
-                if (world.world == tab) {
-                  return [
-                    ...world.tactics.map(item => {
-                      return <InventoryItem
-                        key={`${world.world}-${item.name}`}
-                        showDoc={() => {openDoc({name: item.name, type: 'Tactic'})}}
-                        name={item.name} displayName={item.displayName}
-                        locked={difficulty > 0 ? !inv.includes(item.name) : false}
-                        disabled={item.disabled} newly={false} enableAll={enableAll} />
-                    }),
-                    ...world.lemmas.map(item => {
-                      return <InventoryItem
-                        key={`${world.world}-${item.name}`}
-                        showDoc={() => {openDoc({name: item.name, type: 'Lemma'})}}
-                        name={item.name} displayName={item.displayName}
-                        locked={difficulty > 0 ? item.locked : false}
-                        disabled={item.disabled} newly={false} enableAll={enableAll} />
-                    }),
-                    ...world.definitions.map(item => {
-                      return <InventoryItem
-                        key={`${world.world}-${item.name}`}
-                        showDoc={() => {openDoc({name: item.name, type: 'Definition'})}}
-                        name={item.name} displayName={item.displayName}
-                        locked={difficulty > 0 ? item.locked : false}
-                        disabled={item.disabled} newly={false} enableAll={enableAll} />
-                    })
-                  ]
-                }
-              })}
-            </div>
-          </>}
-        </div>
-      }
-    </>
-
-  )
-}
-
 function InventoryList({items, docType, openDoc, defaultTab=null, level=undefined, enableAll=false} :
   {
     items: InventoryTile[],
@@ -159,7 +86,7 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
       {[...modifiedItems].sort(
           // For lemas, sort entries `available > disabled > locked`
           // otherwise alphabetically
-          (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
+          (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled)
         ).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => {
             return <InventoryItem key={`${item.category}-${item.name}`}
               showDoc={() => {openDoc({name: item.name, type: docType})}}
@@ -217,21 +144,3 @@ export function InventoryPanel({levelInfo, visible = true}) {
     }
   </div>
 }
-
-/** The panel (on the welcome page) showing the user's inventory with tactics, definitions, and lemmas */
-export function InventoryOverviewPanel({data, visible = true, showOverview=true} : {data : WorldOverview[], visible?: boolean, showOverview?: boolean}) {
-  const gameId = React.useContext(GameIdContext)
-
-  // The inventory is overlayed by the doc entry of a clicked item
-  const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
-  // Set `inventoryDoc` to `null` to close the doc
-  function closeInventoryDoc() {setInventoryDoc(null)}
-
-  return <div className={`column inventory-panel ${visible ? '' : 'hidden'}`}>
-    {inventoryDoc ?
-      <Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
-      :
-      <OverviewInventory data={data} openDoc={setInventoryDoc} enableAll={true} showOverview={showOverview}/>
-    }
-  </div>
-}

client/src/components/landing_page.tsx

@@ -7,12 +7,11 @@ import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 
 import '../css/landing_page.css'
+import coverRobo from '../assets/covers/formaloversum.png'
 import bgImage from '../assets/bg.jpg'
 
 import Markdown from './markdown';
 import {PrivacyPolicyPopup} from './popup/privacy_policy'
-import { GameTile, useGetGameInfoQuery } from '../state/api'
-import path from 'path';
 
 const flag = {
   'Dutch': '🇳🇱',
@@ -20,7 +19,6 @@ const flag = {
   'French': '🇫🇷',
   'German': '🇩🇪',
   'Italian': '🇮🇹',
-  'Spanish': '🇪🇸',
 }
 
 function GithubIcon({url='https://github.com'}) {
@@ -34,42 +32,47 @@ function GithubIcon({url='https://github.com'}) {
     </div>
 }
 
-function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
+function GameTile({
+  title,
+  gameId,
+  intro, // Catchy intro phrase.
+  image=null,
+  worlds='?',
+  levels='?',
+  prereq='&ndash;', // Optional list of games that this game builds on. Use markdown.
+  description, // Longer description. Supports Markdown.
+  language}) {
 
   let navigate = useNavigate();
   const routeChange = () =>{
     navigate(gameId);
   }
 
-  if (typeof data === 'undefined') {
-    return <></>
-  }
-
   return <div className="game" onClick={routeChange}>
     <div className="wrapper">
-      <div className="title">{data.title}</div>
-      <div className="short-description">{data.short}
+      <div className="title">{title}</div>
+      <div className="short-description">{intro}
       </div>
-      { data.image ? <img className="image" src={path.join("data", gameId, data.image)} alt="" /> : <div className="image"/> }
-      <div className="long description"><Markdown>{data.long}</Markdown></div>
+      { image ? <img className="image" src={image} alt="" /> : <div className="image"/> }
+      <div className="long description"><Markdown>{description}</Markdown></div>
     </div>
     <table className="info">
       <tbody>
       <tr>
         <td title="consider playing these games first.">Prerequisites</td>
-        <td><Markdown>{data.prerequisites.join(', ')}</Markdown></td>
+        <td><Markdown>{prereq}</Markdown></td>
       </tr>
       <tr>
         <td>Worlds</td>
-        <td>{data.worlds}</td>
+        <td>{worlds}</td>
       </tr>
       <tr>
         <td>Levels</td>
-        <td>{data.levels}</td>
+        <td>{levels}</td>
       </tr>
       <tr>
         <td>Language</td>
-        <td title={`in ${data.languages.join(', ')}`}>{data.languages.map((lan) => flag[lan]).join(', ')}</td>
+        <td title={`in ${language}`}>{flag[language]}</td>
       </tr>
       </tbody>
     </table>
@@ -85,58 +88,6 @@ function LandingPage() {
   const openImpressum = () => setImpressum(true);
   const closeImpressum = () => setImpressum(false);
 
-  // const [allGames, setAllGames] = React.useState([])
-  // const [allTiles, setAllTiles] = React.useState([])
-
-  // const getTiles=()=>{
-  //   fetch('featured_games.json', {
-  //     headers : {
-  //       'Content-Type': 'application/json',
-  //       'Accept': 'application/json'
-  //     }
-  //   }
-  //   ).then(function(response){
-  //     return response.json()
-  //   }).then(function(data) {
-  //     setAllGames(data.featured_games)
-
-  //   })
-  // }
-
-  // React.useEffect(()=>{
-  //   getTiles()
-  // },[])
-
-  // React.useEffect(()=>{
-
-  //   Promise.allSettled(
-  //     allGames.map((gameId) => (
-  //       fetch(`data/g/${gameId}/game.json`).catch(err => {return undefined})))
-  //   ).then(responses =>
-  //     responses.forEach((result) => console.log(result)))
-  //   //   Promise.all(responses.map(res => {
-  //   //     if (res.status == "fulfilled") {
-  //   //       console.log(res.value.json())
-  //   //       return res.value.json()
-  //   //     } else {
-  //   //       return undefined
-  //   //     }
-  //   //   }))
-  //   // ).then(allData => {
-  //   //   setAllTiles(allData.map(data => data?.tile))
-  //   // })
-  // },[allGames])
-
-  // TODO: I would like to read the supported games list form a JSON,
-  // Then load all these games in
-  //
-  let allGames = [
-    "leanprover-community/nng4",
-    "hhu-adam/robo",
-    "djvelleman/stg4",
-    "miguelmarco/STG4",
-  ]
-  let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
 
   return <div className="landing-page">
     <header style={{backgroundImage: `url(${bgImage})`}}>
@@ -153,26 +104,49 @@ function LandingPage() {
       </div>
     </header>
     <div className="game-list">
-      {allTiles.length == 0 ?
-        <p>No Games loaded. Use <a>http://localhost:3000/#/g/local/FOLDER</a> to open a
-          game directly from a local folder.
-        </p>
-        : allGames.map((id, i) => (
-          <Tile
-            key={id}
-            gameId={`g/${id}`}
-            data={allTiles[i]}
-          />
-        ))
-      }
+
+      <GameTile
+        title="Natural Number Game"
+        gameId="g/hhu-adam/NNG4"
+        intro="The classical introduction game for Lean."
+        description="In this game you recreate the natural numbers $\mathbb{N}$ from the Peano axioms,
+learning the basics about theorem proving in Lean.
+
+This is a good first introduction to Lean!"
+        worlds="4"
+        levels="30"
+        language="English"
+        />
+
+      <GameTile
+        title="Formaloversum"
+        gameId="g/hhu-adam/Robo"
+        intro="Erkunde das Leansche Universum mit deinem Robo, welcher dir bei der Verständigung mit den Formalosophen zur Seite steht."
+        description="
+Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet danach verschiedene Bereiche des Bachelorstudiums an.
+
+(Das Spiel befindet sich noch in der Entstehungsphase.)"
+        image={coverRobo}
+        language="German"
+        />
+
+      <GameTile
+        title="NNG (OLD)"
+        gameId="g/hhu-adam/nng4-old"
+        intro="The old version of the NNG copied from lean3."
+        description="This version is not maintained and might break at any point. You should play the new version instead"
+        worlds="9"
+        levels="72"
+        language="English"
+        />
     </div>
     <section>
       <div className="wrapper">
         <h2>Development notes</h2>
         <p>
           As this server runs lean on our university machines, it has a limited capacity.
-          Our current estimate is about 70 simultaneous games.
-          We hope to address and test this limitation better in the future.
+          Our current estimate is about 55 copies of the NNG or 25 copies of games importing
+          mathlib. We hope to address this limitation in the future.
         </p>
         <p>
           Most aspects of the games and the infrastructure are still in development. Feel free to
@@ -186,19 +160,18 @@ function LandingPage() {
         <h2>Adding new games</h2>
         <p>
           If you are considering writing your own game, you should use
-          the <a target="_blank" href="https://github.com/hhu-adam/GameSkeleton">GameSkeleton Github Repo</a> as
-          a template and read <a target="_blank" href="https://github.com/leanprover-community/lean4game/">How to Create a Game</a>.
+          the <a target="_blank" href="https://github.com/hhu-adam/NNG4">NNG Github Repo</a> as
+          a template.
         </p>
         <p>
-          You can directly load your games into the server and play it using
-          the correct URL. The <a target="_blank" href="https://github.com/leanprover-community/lean4game/">instructions above</a> also
-          explain the details for how to load your game to the server.
-
-          We'd like to encourage you to contact us if you have any questions.
+          There is an option to load and run your own games directly on the server,
+          instructions are in the NNG repo. Since this is still in development we'd like to
+          encourage you to contact us for support creating your own game. The documentation is
+          not polished yet.
         </p>
         <p>
-          Featured games on this page are added manually.
-          Please get in contact and we-ll happily add yours.
+          To add games to this main page, you should get in contact as
+          games will need to be added manually.
         </p>
       </div>
     </section>
@@ -216,6 +189,9 @@ function LandingPage() {
       <a className="link" onClick={openImpressum}>Impressum</a>
       {impressum? <PrivacyPolicyPopup handleClose={closeImpressum} />: null}
     </footer>
+
+    {/* <PrivacyPolicy/> */}
+
   </div>
 
 }

client/src/components/level.tsx

@@ -22,19 +22,18 @@ import { ConnectionContext, connection, useLeanClient } from '../connection'
 import { useAppDispatch, useAppSelector } from '../hooks'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'
 import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited,
-  selectHelp, selectDifficulty, selectInventory, selectTypewriterMode, changeTypewriterMode } from '../state/progress'
+  selectHelp, selectDifficulty, selectInventory } from '../state/progress'
 import { store } from '../state/store'
 import { Button } from './button'
 import Markdown from './markdown'
-import {InventoryOverviewPanel, InventoryPanel} from './inventory'
+import {InventoryPanel} from './inventory'
 import { hasInteractiveErrors } from './infoview/typewriter'
 import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext,
   ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
 import { GameHint } from './infoview/rpc_api'
-import { DeletedHints, Hint, Hints, filterHints } from './hints'
+import { DeletedHints, Hint, Hints } from './hints'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
-import path from 'path';
 
 import '@fontsource/roboto/300.css'
 import '@fontsource/roboto/400.css'
@@ -49,6 +48,7 @@ function Level() {
   const params = useParams()
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
+  // useLoadWorldFiles(worldId)
 
   const [impressum, setImpressum] = React.useState(false)
 
@@ -138,24 +138,19 @@ function ChatPanel({lastLevel}) {
 
   let introText: Array<string> = level?.data?.introduction.split(/\n(\s*\n)+/)
 
-  // experimental: Remove all hints that appeared identically in the previous step
-  // This effectively prevent consequtive hints being shown.
-  let modifiedHints : GameHint[][] = filterHints(proof)
-
   return <div className="chat-panel">
     <div ref={chatRef} className="chat">
       {introText?.filter(t => t.trim()).map(((t, i) =>
-        // Show the level's intro text as hints, too
         <Hint key={`intro-p-${i}`}
           hint={{text: t, hidden: false}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
       ))}
-      {modifiedHints.map((step, i) => {
+      {proof.map((step, i) => {
         // It the last step has errors, it will have the same hints
         // as the second-to-last step. Therefore we should not display them.
         if (!(i == proof.length - 1 && withErr)) {
           // TODO: Should not use index as key.
           return <Hints key={`hints-${i}`}
-            hints={step} showHidden={showHelp.has(i)} step={i}
+            hints={step.hints} showHidden={showHelp.has(i)} step={i}
             selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.length - 1}/>
         }
       })}
@@ -209,16 +204,11 @@ function PlayableLevel({impressum, setImpressum}) {
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const {mobile} = React.useContext(MobileContext)
 
-  const dispatch = useAppDispatch()
-
   const difficulty = useSelector(selectDifficulty(gameId))
   const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
   const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
   const inventory: Array<String> = useSelector(selectInventory(gameId))
 
-  const typewriterMode = useSelector(selectTypewriterMode(gameId))
-  const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
-
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
 
@@ -231,11 +221,12 @@ function PlayableLevel({impressum, setImpressum}) {
   const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
   // Only for mobile layout
   const [pageNumber, setPageNumber] = useState(0)
-
+  const [typewriterMode, setTypewriterMode] = useState(true)
   // set to true to prevent switching between typewriter and editor
   const [lockInputMode, setLockInputMode] = useState(false)
   const [typewriterInput, setTypewriterInput] = useState("")
   const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
+  const dispatch = useAppDispatch()
 
   // impressum pop-up
   function toggleImpressum() {setImpressum(!impressum)}
@@ -329,6 +320,8 @@ function PlayableLevel({impressum, setImpressum}) {
           console.debug(`not inserting template.`)
         }
       }
+    } else {
+      setTypewriterMode(true)
     }
   }, [level, levelId, worldId, gameId, editor])
 
@@ -343,7 +336,7 @@ function PlayableLevel({impressum, setImpressum}) {
   }, [gameId, worldId, levelId])
 
   useEffect(() => {
-    if (!typewriterMode && editor) {
+    if (!typewriterMode) {
       // Delete last input attempt from command line
       editor.executeEdits("typewriter", [{
         range: editor.getSelection(),
@@ -473,11 +466,6 @@ function Introduction({impressum, setImpressum}) {
 
   const gameInfo = useGetGameInfoQuery({game: gameId})
 
-  const {worldId} = useContext(WorldLevelIdContext)
-
-  let image: string = gameInfo.data?.worlds.nodes[worldId].image
-
-
   const toggleImpressum = () => {
     setImpressum(!impressum)
   }
@@ -491,14 +479,8 @@ function Introduction({impressum, setImpressum}) {
       :
         <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
           <IntroductionPanel gameInfo={gameInfo} />
-          <div className="world-image-container empty">
-            {image &&
-              // TODO: Temporary for testing
-              <img className={worldId=="Proposition" ? "cover" : "contain"} src={path.join("data", gameId, image)} alt="" />
-            }
-
-          </div>
-          <InventoryOverviewPanel data={inventory?.data} />
+          <div className="world-image-container empty"></div>
+          <InventoryPanel levelInfo={inventory?.data} />
         </Split>
       }
 
@@ -633,7 +615,6 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
 
       return () => {
         editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
-        model.dispose();
       }
     }
   }, [editor, levelId, connection, leanClientStarted])
@@ -656,3 +637,27 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
 
   return {editor, infoProvider, editorConnection}
 }
+
+/** Open all files in this world on the server so that they will load faster when accessed */
+function useLoadWorldFiles(worldId) {
+  const gameId = React.useContext(GameIdContext)
+  const gameInfo = useGetGameInfoQuery({game: gameId})
+  const store = useStore()
+
+  useEffect(() => {
+    if (gameInfo.data) {
+      const models = []
+      for (let levelId = 1; levelId <= gameInfo.data.worldSize[worldId]; levelId++) {
+        const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`)
+        let model = monaco.editor.getModel(uri)
+        if (model) {
+          models.push(model)
+        } else {
+          const code = selectCode(gameId, worldId, levelId)(store.getState())
+          models.push(monaco.editor.createModel(code, 'lean4', uri))
+        }
+      }
+      return () => { for (let model of models) { model.dispose() } }
+    }
+  }, [gameInfo.data, worldId])
+}

client/src/components/welcome.tsx

@@ -11,7 +11,7 @@ import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
 import { Button } from './button'
 import { MobileContext } from './infoview/context'
-import { InventoryOverviewPanel, InventoryPanel } from './inventory'
+import { InventoryPanel } from './inventory'
 import { ErasePopup } from './popup/erase'
 import { InfoPopup } from './popup/game_info'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
@@ -111,7 +111,7 @@ function Welcome() {
               <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
                 rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
             :
-              <InventoryOverviewPanel data={inventory?.data} />
+              <InventoryPanel levelInfo={inventory?.data} />
             )}
           </div>
         :
@@ -119,7 +119,7 @@ function Welcome() {
             <IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
             <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
               rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
-            <InventoryOverviewPanel data={inventory?.data} />
+            <InventoryPanel levelInfo={inventory?.data} />
           </Split>
       }
     </div>

client/src/connection.ts

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

client/src/css/landing_page.css

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

client/src/css/level.css

@@ -336,21 +336,6 @@ td code  {
   background-color: #eee;
 }
 
-.world-image-container {
-  display: flex;
-  flex-direction: column;
-  justify-content: center;
-}
-
-.world-image-container img.contain {
-  object-fit: contain;
-}
-
-.world-image-container img.cover {
-  height: 100%;
-  object-fit: cover;
-}
-
 .typewriter-interface .proof {
   background-color: #fff;
 }

client/src/index.tsx

@@ -15,6 +15,15 @@ import { monacoSetup } from 'lean4web/client/src/monacoSetup'
 
 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
@@ -34,11 +43,6 @@ const router = createHashRouter([
     path: "/game/nng",
     loader: () => redirect("/g/hhu-adam/NNG4")
   },
-  {
-    // For backwards compatibility
-    path: "/g/hhu-adam/NNG4",
-    loader: () => redirect("/g/leanprover-community/NNG4")
-  },
   {
     path: "/g/:owner/:repo",
     element: <App />,

client/src/leanclient.ts

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

client/src/state/api.ts

@@ -2,29 +2,16 @@
  * @fileOverview Define API of the server-client communication
 */
 import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react'
-
-
-export interface GameTile {
-  title: string
-  short: string
-  long: string
-  languages: Array<string>
-  prerequisites: Array<string>
-  worlds: number
-  levels: number
-  image: string
-}
+import { Connection } from '../connection'
 
 export interface GameInfo {
   title: null|string,
   introduction: null|string,
   info: null|string,
-  worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string, image: string}}, edges: string[][]},
+  worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string}}, edges: string[][]},
   worldSize: null|{[key: string]: number},
   authors: null|string[],
   conclusion: null|string,
-  tile: null|GameTile,
-  image: null|string
 }
 
 export interface InventoryTile {
@@ -50,8 +37,7 @@ export interface LevelInfo {
   lemmaTab: null|string,
   statementName: null|string,
   displayName: null|string,
-  template: null|string,
-  image: null|string
+  template: null|string
 }
 
 /** Used to display the inventory on the welcome page */
@@ -71,29 +57,40 @@ interface Doc {
   category: string,
 }
 
-export interface WorldOverview {
-  world: string
-  tactics: InventoryTile[]
-  lemmas: InventoryTile[]
-  definitions: InventoryTile[]
+
+const customBaseQuery = async (
+  args : {game: string, method: string, params?: any},
+  { signal, dispatch, getState, extra },
+  extraOptions
+) => {
+  try {
+    const connection : Connection = extra.connection
+    let leanClient = await connection.startLeanClient(args.game)
+    console.log(`Sending request ${args.method}`)
+    let res = await leanClient.sendRequest(args.method, args.params)
+    console.log('Received response') //, res)
+    return {'data': res}
+   } catch (e) {
+    return {'error': e}
+   }
 }
 
 // Define a service using a base URL and expected endpoints
 export const apiSlice = createApi({
   reducerPath: 'gameApi',
-  baseQuery: fetchBaseQuery({ baseUrl: window.location.origin + "/data" }),
+  baseQuery: customBaseQuery,
   endpoints: (builder) => ({
     getGameInfo: builder.query<GameInfo, {game: string}>({
-      query: ({game}) => `${game}/game.json`,
+      query: ({game}) => {return {game, method: 'info', params: {}}},
     }),
     loadLevel: builder.query<LevelInfo, {game: string, world: string, level: number}>({
-      query: ({game, world, level}) => `${game}/level__${world}__${level}.json`,
+      query: ({game, world, level}) => {return {game, method: "loadLevel", params: {world, level}}},
     }),
-    loadInventoryOverview: builder.query<WorldOverview[], {game: string}>({
-      query: ({game}) => `${game}/inventory.json`,
+    loadInventoryOverview: builder.query<InventoryOverview, {game: string}>({
+      query: ({game}) => {return {game, method: "loadInventoryOverview", params: {}}},
     }),
     loadDoc: builder.query<Doc, {game: string, name: string, type: "lemma"|"tactic"}>({
-      query: ({game, type, name}) => `${game}/doc__${type}__${name}.json`,
+      query: ({game, name, type}) => {return {game, method: "loadDoc", params: {name, type}}},
     }),
   }),
 })

client/src/state/progress.ts

@@ -26,8 +26,7 @@ export interface GameProgressState {
   inventory: string[],
   difficulty: number,
   openedIntro: boolean,
-  data: WorldProgressState,
-  typewriterMode?: boolean
+  data: WorldProgressState
 }
 
 /**
@@ -127,11 +126,6 @@ export const progressSlice = createSlice({
       addGameProgress(state, action)
       state.games[action.payload.game].openedIntro = action.payload.openedIntro
     },
-    /** set the typewriter mode */
-    changeTypewriterMode(state: ProgressState, action: PayloadAction<{game: string, typewriterMode: boolean}>) {
-      addGameProgress(state, action)
-      state.games[action.payload.game].typewriterMode = action.payload.typewriterMode
-    }
   }
 })
 
@@ -202,14 +196,7 @@ export function selectOpenedIntro(game: string) {
   }
 }
 
-/** return typewriter mode for the current game if it exists */
-export function selectTypewriterMode(game: string) {
-  return (state) => {
-    return state.progress.games[game]?.typewriterMode ?? true
-  }
-}
-
 /** Export actions to modify the progress */
 export const { changedSelection, codeEdited, levelCompleted, deleteProgress,
   deleteLevelProgress, loadProgress, helpEdited, changedInventory, changedOpenedIntro,
-  changedDifficulty, changeTypewriterMode} = progressSlice.actions
+  changedDifficulty } = progressSlice.actions

client/src/wasm.ts

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

doc/DOCUMENTATION.md

@@ -1,8 +1,6 @@
-**NOTE! This document is deprecated! The current documentation is [How To Create A Game](create_game.md)**
-
 # Creating a game.
 
-Ideally one takes the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new game.
+Ideally one takes the [NNG template](https://github.com/hhu-adam/NNG4) to create a new game.
 
 ## Game Structure
 
@@ -297,9 +295,8 @@ cd lean4game
 npm install
 ```
 
-TODO: This is outdated!
 If you are developing a game other than `Robo` or `NNG4`, adapt the
-code at the beginning of `lean4game/relay/index.mjs`:
+code at the beginning of `lean4game/server/index.mjs`:
 ```typescript
 const games = {
     "g/hhu-adam/robo": {

doc/create_game.md

@@ -223,40 +223,29 @@ One thing to keep in mind is that the game will look at the main proof to figure
 Most important for game development are probably the `Hints`.
 
 The hints will be displayed whenever the player's current goal matches the goal the hint is
-placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands.
+placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands. If you specify
 
-Read [More about Hints](doc/hints.md) for how they work and what the options are.
+```
+Hint (strict := true) "some hidden hint"
+```
 
-### 6. e) Extra: Images
-You can add images on any layer of the game (i.e. game/world/level). These will be displayed in your game.
+a hint only matches iff the assumptions match exactly one-to-one. (Otherwise, it does not care if there are additional assumptions in context)
 
-The images need to be placed in `images/` and you need to add a command like `Image "images/path/to/myWorldImage.png"` 
-in one of the files you created in 2), 3), or 4) (i.e. game/world/level).
+Further, you can choose to hide hints and only have them displayed when the player presses "More Help":
+```
+Hint (hidden := true) "some hidden hint"
+```
 
-NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world.
+Lastly, you should put variable names in hints inside brackets:
+
+```
+Hint "now use `rw [{h}]` to use your assumption {h}."
+```
+That way, the game will replace it with the actual name the assumption has in the player's proof state.
 
 ## 7. Update your game
 
-In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](doc/update_game.md).
-
-## 8. Publish your game
-
-To publish your game on the official server, see [Publishing a game](doc/publish_game.md)
-
-There are a few more options you can add in `Game.lean` before the `MakeGame` command, which describe the tile that is visible on the server's landing page:
-
-```lean
-Languages "English"
-CaptionShort "Game Template"
-CaptionLong "You should use this game as a template for your own game and add your own levels."
-Prerequisites "NNG"
-CoverImage "images/cover.png"
-```
-* `Languages`: Currently only a single language (capital English name). The tile will show a corresponding flag.
-* `CaptionShort`: One catch phrase. Appears above the image.
-* `CaptionLong`: 2-4 sentences to describe the game.
-* `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text.
-* `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens.
+In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](https://github.com/leanprover-community/lean4game/blob/main/doc/update_game.md).
 
 ## Further Notes
 

doc/hints.md

@@ -1,87 +0,0 @@
-# Hints
-
-Most important for game development are probably the "Hints". You can add Hints at any place in your proof using the `Hint` tactic
-
-```
-Statement .... := by
-  Hint "Hint to show at the start"
-  rw [h]
-  Hint "some tip after using rw"
-  ...
-```
-
-## 1. When do hints show?
-
-A hint will be displayed if the player's goal matches the one where the hint was placed in the
-sample solutions and the entire context from the sample solutions is present in the
-player's context. The player's context may contain additional items.
-
-This means if you have multiple identical
-subgoals, you should only place a single hint in one of them and it will be displayed in
-all of them.
-
-However, identical (non-hidden) hints which where already present in the step
-before are omitted. This is to allow a player to add new assumptions to context, for example
-with `have`, without seeing the same hint over and over again.
-Hidden hints are not filtered.
-
-## 2. Alternative Proofs / `Branch`
-
-You can use `Branch` to place hints
-in dead ends or alternative proof strands.
-
-A proof inside a `Branch`-block is normally evaluated by lean but it's discarded at the end
-so that no progress has been made on proofing the goal.
-
-```
-Statement .... := by
-  Hint "Huse `rw` or `rewrite`."
-  Branch
-    rewrite [h]
-    Hint "now you still need `rfl`"
-  rw [h]
-```
-
-## 3. Variables names
-
-Put variables in the hint text inside brackets like this: `{h}`! This way the server can replace
-the variable's name with the one the user actually used.
-
-For example, if the sample proof contains
-
-```
-have h : True := trivial
-Hint "Now use `rw [{h}]` to use your assumption `{h}`."
-```
-
-but the player writes `have g : True := trivial`, they will see a hint saying
-"Now use `rw [g]` to use your assumption `g`."
-
-## 4. Hidden hints
-
-Some hints can be hidden, and only show after the user clicks on a button to get additional
-help. You mark a hint as hidden with `(hidden := true)`:
-
-```
-Hint (hidden := true) "some hidden hint"
-```
-
-## 5. Strict context matching
-
-If you use the attribute `(strict := true)` a hint is only shown if the entire context
-matches exactly the one where the hint is placed. With `(hint := false)`, which is the default,
-it does not matter if additional assumptions are present in the player's context.
-
-```
-Hint (strict := true) "now use `have` to create a new assumption."
-```
-
-You should probably use `(strict := true)` if you want to give fine-grained details about
-tactics like `have` which do not modify the goal or any existing assumptions, but only
-create new assumptions.
-
-## 6. Formatting
-
-You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$`
-
-TODO: Write a doc about latex/markdown options available.

doc/publish_game.md

@@ -1,32 +0,0 @@
-# Publishing games
-
-You can publish your game on the official (Lean Game Server)[https://adam.math.hhu.de] in a few simple
-steps.
-
-## 1. Upload Game to github
-
-First, you need your game in a public Github repository and make sure the github action has run.
-You can check this by spotting the green checkmark on the start page, or by looking at the "Actions"
-tab.
-
-## 2. Import the game
-
-You call the URL that's listed under "What's Next?" in the latest action run. Explicitely you call
-the URL of the form
-
-> adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY}
-
-where `{USER}` and `{REPOSITORY}` are replaced with the github user and repository name.
-
-You should see a white screen which shows import updates and eventually reports "Done."
-
-## 3. Play the game
-
-Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITORY}`!
-
-## 4. Main page
-
-Adding games to the main page happens manually by the server maintainers. Tell us if you want us
-to add a tile for your game!
-
-For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).

doc/running_locally.md

@@ -85,11 +85,12 @@ git clone https://github.com/hhu-adam/GameSkeleton.git
 Download dependencies and build the game:
 ```bash
 cd GameSkeleton
-lake update -R
+lake update
+lake exe cache get   # if your game depends on mathlib
 lake build
 ```
 
-Clone the server repository into a directory next to the game:
+Clone the game repository into a directory next to the game:
 ```bash
 cd ..
 git clone https://github.com/leanprover-community/lean4game.git
@@ -112,12 +113,12 @@ This takes a little time. Eventually, the game is available on http://localhost:
 
 ## Modifying the GameServer
 
-When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by using `lake update -R -Klean4game.local`:
+When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by setting `export LEAN4GAME=local` inside your local game before building it:
 
 ```bash
 cd NNG4
-lake update -R -Klean4game.local
+export LEAN4GAME=local
+lake update
 lake build
 ```
-This causes lake to search locally for the `GameServer` lake package instead of using the version from github. Therefore, you can the local copy of the edit `GameServer` in `../lean4game` and
-`lake build` will then directly use this modified copy to build your game.
+This causes lake to search locally for the `GameServer` lake package instead of using the version from github. Therefore, when you `lake build` your game, it will rebuild with the modified `GameServer`.

doc/server.md

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

doc/update_game.md

@@ -10,43 +10,28 @@ Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https:
 Then, depending on the setup you use, do one of the following:
 
 * Dev Container: Rebuild the VSCode Devcontainer.
-* Local Setup: in your game's folder run the following:
-  ```
-  lake update -R
-  lake build
-  ```
-
-  * Additionally, if you have a local copy of the server `lean4game`,
-    you should update this one to the matching version. Run the following in the folder `lean4game/`:
-    ```
-    git fetch
-    git checkout {VERSION_TAG}
-    npm install
-    ```
-    where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
+* Local Setup: run `lake update` (followed by `lake exe cache get` if you depend on mathlib.)
 * Gitpod/Codespaces: Create a fresh one
 
-This will update your game (and the mathlib version you might be using) to the new lean version.
+This will update `lean4game` and `mathlib` in your project to the new lean version.
 
 ## Newest developing setup
 
 There are a few files in your game repository which are used for the developing setup
-(dev container/codespaces/gitpod). If you need to update your developing setup, for example because it doesn't work
+(dev container/codespaces/gitpod). If you need to update your're developing setup, for example because it doesn't work
 anymore, you will need to copy the relevant files from the [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) template into your game repo.
 
 The relevant files are:
 
 ```
-.devcontainer/
-.docker/
-.github/
-.gitpod/
-.vscode/
 lakefile.lean
+.devcontainer/**
+.docker/**
+.gitpod
+.vscode/**
 ```
 
-simply copy them from the `GameSkeleton` into your game and proceed as above,
-i.e. `lake update -R && lake build`.
+simply copy them from the `GameSkeleton` into your game.
 
 (Note: You should not need to modify any of these files, with the exception of the `lakefile.lean`,
-where you need to add any dependencies of your game, or remove mathlib if you don't need it.)
+where you need to add any dependencies of your game.)

ecosystem.config.js

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

index.html

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

package-lock.json

@@ -20,6 +20,7 @@
         "@types/cytoscape": "^3.19.9",
         "@types/react-router-dom": "^5.3.3",
         "@vitejs/plugin-react-swc": "^3.4.0",
+        "coi-serviceworker": "^0.1.7",
         "cross-env": "^7.0.3",
         "cytoscape": "^3.23.0",
         "cytoscape-elk": "^2.1.0",
@@ -40,7 +41,6 @@
         "rehype-katex": "^6.0.2",
         "remark-gfm": "^3.0.1",
         "remark-math": "^5.1.1",
-        "request": "^2.88.2",
         "request-progress": "^3.0.0",
         "vite": "^4.5.0",
         "vite-plugin-static-copy": "^0.17.0",
@@ -57,7 +57,7 @@
         "concurrently": "^7.6.0",
         "css-loader": "^6.7.3",
         "file-loader": "^6.2.0",
-        "nodemon": "^3.0.1",
+        "nodemon": "^2.0.20",
         "react-refresh": "^0.14.0",
         "style-loader": "^3.3.1",
         "ts-loader": "^9.4.2",
@@ -6015,6 +6015,7 @@
       "version": "6.12.6",
       "resolved": "https://registry.npmjs.org/ajv/-/ajv-6.12.6.tgz",
       "integrity": "sha512-j3fVLgvTo527anyYyJOGTYJbG+vnnQYvE0m5mmkc1TK+nxAppkCLMIL0aZ4dblVCNoGShhm+kzE4ZUykBoMg4g==",
+      "dev": true,
       "dependencies": {
         "fast-deep-equal": "^3.1.1",
         "fast-json-stable-stringify": "^2.0.0",
@@ -6183,22 +6184,6 @@
       "resolved": "https://registry.npmjs.org/asap/-/asap-2.0.6.tgz",
       "integrity": "sha512-BSHWgDSAiKs50o2Re8ppvp3seVHXSRM44cdSsT9FfNEUUZLOGWVCsiWaRPWM1Znn+mqZ1OfVZ3z3DWEzSp7hRA=="
     },
-    "node_modules/asn1": {
-      "version": "0.2.6",
-      "resolved": "https://registry.npmjs.org/asn1/-/asn1-0.2.6.tgz",
-      "integrity": "sha512-ix/FxPn0MDjeyJ7i/yoHGFt/EX6LyNbxSEhPPXODPL+KB0VPk86UYfL0lMdy+KCnv+fmvIzySwaK5COwqVbWTQ==",
-      "dependencies": {
-        "safer-buffer": "~2.1.0"
-      }
-    },
-    "node_modules/assert-plus": {
-      "version": "1.0.0",
-      "resolved": "https://registry.npmjs.org/assert-plus/-/assert-plus-1.0.0.tgz",
-      "integrity": "sha512-NfJ4UzBCcQGLDlQq7nHxH+tv3kyZ0hHQqF5BO6J7tNJeP5do1llPr8dZ8zHonfhAu0PHAdMkSo+8o0wxg9lZWw==",
-      "engines": {
-        "node": ">=0.8"
-      }
-    },
     "node_modules/ast-types": {
       "version": "0.15.2",
       "resolved": "https://registry.npmjs.org/ast-types/-/ast-types-0.15.2.tgz",
@@ -6228,11 +6213,6 @@
       "resolved": "https://registry.npmjs.org/async-limiter/-/async-limiter-1.0.1.tgz",
       "integrity": "sha512-csOlWGAcRFJaI6m+F2WKdnMKr4HhdhFVBk0H/QbJFMCr+uO2kwohwXQPxw/9OCxp05r5ghVBFSyioixx3gfkNQ=="
     },
-    "node_modules/asynckit": {
-      "version": "0.4.0",
-      "resolved": "https://registry.npmjs.org/asynckit/-/asynckit-0.4.0.tgz",
-      "integrity": "sha512-Oei9OH4tRh0YqU3GxhX79dM/mwVgvbZJaSNaRk+bshkj0S5cfHcgYakreBjrHwatXKbz+IoIdYLxrKim2MjW0Q=="
-    },
     "node_modules/available-typed-arrays": {
       "version": "1.0.5",
       "resolved": "https://registry.npmjs.org/available-typed-arrays/-/available-typed-arrays-1.0.5.tgz",
@@ -6245,40 +6225,12 @@
         "url": "https://github.com/sponsors/ljharb"
       }
     },
-    "node_modules/aws-sign2": {
-      "version": "0.7.0",
-      "resolved": "https://registry.npmjs.org/aws-sign2/-/aws-sign2-0.7.0.tgz",
-      "integrity": "sha512-08kcGqnYf/YmjoRhfxyu+CLxBjUtHLXLXX/vUfx9l2LYzG3c1m61nrpyFUZI6zeS+Li/wWMMidD9KgrqtGq3mA==",
-      "engines": {
-        "node": "*"
-      }
-    },
-    "node_modules/aws4": {
-      "version": "1.12.0",
-      "resolved": "https://registry.npmjs.org/aws4/-/aws4-1.12.0.tgz",
-      "integrity": "sha512-NmWvPnx0F1SfrQbYwOi7OeaNGokp9XhzNioJ/CSBs8Qa4vxug81mhJEAVZwxXuBmYB5KDRfMq/F3RR0BIU7sWg=="
-    },
     "node_modules/axios": {
-      "version": "1.6.2",
-      "resolved": "https://registry.npmjs.org/axios/-/axios-1.6.2.tgz",
-      "integrity": "sha512-7i24Ri4pmDRfJTR7LDBhsOTtcm+9kjX5WiY1X3wIisx6G9So3pfMkEiU7emUBe46oceVImccTEM3k6C5dbVW8A==",
+      "version": "0.24.0",
+      "resolved": "https://registry.npmjs.org/axios/-/axios-0.24.0.tgz",
+      "integrity": "sha512-Q6cWsys88HoPgAaFAVUb0WpPk0O8iTeisR9IMqy9G8AbO4NlpVknrnQS03zzF9PGAWgO3cgletO3VjV/P7VztA==",
       "dependencies": {
-        "follow-redirects": "^1.15.0",
-        "form-data": "^4.0.0",
-        "proxy-from-env": "^1.1.0"
-      }
-    },
-    "node_modules/axios/node_modules/form-data": {
-      "version": "4.0.0",
-      "resolved": "https://registry.npmjs.org/form-data/-/form-data-4.0.0.tgz",
-      "integrity": "sha512-ETEklSGi5t0QMZuiXoA/Q6vcnxcLQP5vdugSpuAyi6SVGi2clPPp+xgEhuMaHC+zGgn31Kd235W35f7Hykkaww==",
-      "dependencies": {
-        "asynckit": "^0.4.0",
-        "combined-stream": "^1.0.8",
-        "mime-types": "^2.1.12"
-      },
-      "engines": {
-        "node": ">= 6"
+        "follow-redirects": "^1.14.4"
       }
     },
     "node_modules/babel-core": {
@@ -6430,14 +6382,6 @@
       "optional": true,
       "peer": true
     },
-    "node_modules/bcrypt-pbkdf": {
-      "version": "1.0.2",
-      "resolved": "https://registry.npmjs.org/bcrypt-pbkdf/-/bcrypt-pbkdf-1.0.2.tgz",
-      "integrity": "sha512-qeFIXtP4MSoi6NLqO12WfqARWWuCKi2Rn/9hJLEmtB5yTNr9DqFWkJRCf2qShWzPeAMRnOgCrq0sg/KLv5ES9w==",
-      "dependencies": {
-        "tweetnacl": "^0.14.3"
-      }
-    },
     "node_modules/before-after-hook": {
       "version": "2.2.3",
       "resolved": "https://registry.npmjs.org/before-after-hook/-/before-after-hook-2.2.3.tgz",
@@ -6728,11 +6672,6 @@
         }
       ]
     },
-    "node_modules/caseless": {
-      "version": "0.12.0",
-      "resolved": "https://registry.npmjs.org/caseless/-/caseless-0.12.0.tgz",
-      "integrity": "sha512-4tYFyifaFfGacoiObjJegolkwSU4xQNGbVgUiNYVUxbQ2x2lUsFvY4hVgVzGiIe6WLOPqycWXA40l+PWsxthUw=="
-    },
     "node_modules/ccount": {
       "version": "2.0.1",
       "resolved": "https://registry.npmjs.org/ccount/-/ccount-2.0.1.tgz",
@@ -6952,6 +6891,11 @@
         "node": ">=6"
       }
     },
+    "node_modules/coi-serviceworker": {
+      "version": "0.1.7",
+      "resolved": "https://registry.npmjs.org/coi-serviceworker/-/coi-serviceworker-0.1.7.tgz",
+      "integrity": "sha512-bjSUqEngCPOkErY2vbyWsaIGCNRODYzlNycaREVw5s12/C8SM+RnRUUeX6pZbTtov6C52ZLY/+tvHK+BDxuUuA=="
+    },
     "node_modules/color-convert": {
       "version": "1.9.3",
       "resolved": "https://registry.npmjs.org/color-convert/-/color-convert-1.9.3.tgz",
@@ -6970,17 +6914,6 @@
       "resolved": "https://registry.npmjs.org/colorette/-/colorette-1.4.0.tgz",
       "integrity": "sha512-Y2oEozpomLn7Q3HFP7dpww7AtMJplbM9lGZP6RDfHqmbeRjiwRg4n6VM6j4KLmRke85uWEI7JqF17f3pqdRA0g=="
     },
-    "node_modules/combined-stream": {
-      "version": "1.0.8",
-      "resolved": "https://registry.npmjs.org/combined-stream/-/combined-stream-1.0.8.tgz",
-      "integrity": "sha512-FQN4MRfuJeHf7cBbBMJFXhKSDq+2kAArBlmRBvcvFE5BB1HZKXtSFASDhdlz9zOYwxh8lDdnvmMOe/+5cdoEdg==",
-      "dependencies": {
-        "delayed-stream": "~1.0.0"
-      },
-      "engines": {
-        "node": ">= 0.8"
-      }
-    },
     "node_modules/comma-separated-tokens": {
       "version": "2.0.3",
       "resolved": "https://registry.npmjs.org/comma-separated-tokens/-/comma-separated-tokens-2.0.3.tgz",
@@ -7497,17 +7430,6 @@
         "cytoscape": "^3.2.0"
       }
     },
-    "node_modules/dashdash": {
-      "version": "1.14.1",
-      "resolved": "https://registry.npmjs.org/dashdash/-/dashdash-1.14.1.tgz",
-      "integrity": "sha512-jRFi8UDGo6j+odZiEpjazZaWqEal3w/basFjQHQEwVtZJGDpxbH1MeYluwCS8Xq5wmLJooDlMgvVarmWfGM44g==",
-      "dependencies": {
-        "assert-plus": "^1.0.0"
-      },
-      "engines": {
-        "node": ">=0.10"
-      }
-    },
     "node_modules/date-fns": {
       "version": "2.30.0",
       "resolved": "https://registry.npmjs.org/date-fns/-/date-fns-2.30.0.tgz",
@@ -7674,14 +7596,6 @@
         "url": "https://github.com/sponsors/ljharb"
       }
     },
-    "node_modules/delayed-stream": {
-      "version": "1.0.0",
-      "resolved": "https://registry.npmjs.org/delayed-stream/-/delayed-stream-1.0.0.tgz",
-      "integrity": "sha512-ZySD7Nf91aLB0RxL4KGrKHBXl7Eds1DAmEdcoVawXnLD7SDhpNgtuII2aAkg7a7QS41jxPSZ17p4VdGnMHk3MQ==",
-      "engines": {
-        "node": ">=0.4.0"
-      }
-    },
     "node_modules/denodeify": {
       "version": "1.2.1",
       "resolved": "https://registry.npmjs.org/denodeify/-/denodeify-1.2.1.tgz",
@@ -7840,15 +7754,6 @@
         "tslib": "^2.0.3"
       }
     },
-    "node_modules/ecc-jsbn": {
-      "version": "0.1.2",
-      "resolved": "https://registry.npmjs.org/ecc-jsbn/-/ecc-jsbn-0.1.2.tgz",
-      "integrity": "sha512-eh9O+hwRHNbG4BLTjEl3nw044CkGm5X6LoaCf7LPp7UU8Qrt47JYNi6nPX8xjW97TKGKm1ouctg0QSpZe9qrnw==",
-      "dependencies": {
-        "jsbn": "~0.1.0",
-        "safer-buffer": "^2.1.0"
-      }
-    },
     "node_modules/ecdsa-sig-formatter": {
       "version": "1.0.11",
       "resolved": "https://registry.npmjs.org/ecdsa-sig-formatter/-/ecdsa-sig-formatter-1.0.11.tgz",
@@ -8237,18 +8142,11 @@
       "resolved": "https://registry.npmjs.org/extend/-/extend-3.0.2.tgz",
       "integrity": "sha512-fjquC59cD7CyW6urNXK0FBufkZcoiGG80wTuPujX590cB5Ttln20E2UB4S/WARVqhXffZl2LNgS+gQdPIIim/g=="
     },
-    "node_modules/extsprintf": {
-      "version": "1.3.0",
-      "resolved": "https://registry.npmjs.org/extsprintf/-/extsprintf-1.3.0.tgz",
-      "integrity": "sha512-11Ndz7Nv+mvAC1j0ktTa7fAb0vLyGGX+rMHNBYQviQDGU0Hw7lhctJANqbPhu9nV9/izT/IntTgZ7Im/9LJs9g==",
-      "engines": [
-        "node >=0.6.0"
-      ]
-    },
     "node_modules/fast-deep-equal": {
       "version": "3.1.3",
       "resolved": "https://registry.npmjs.org/fast-deep-equal/-/fast-deep-equal-3.1.3.tgz",
-      "integrity": "sha512-f3qQ9oQy9j2AhBe/H9VC91wLmKBCCU/gDOnKNAYG5hswO7BLKj09Hc5HYNz9cGI++xlpDCIgDaitVs03ATR84Q=="
+      "integrity": "sha512-f3qQ9oQy9j2AhBe/H9VC91wLmKBCCU/gDOnKNAYG5hswO7BLKj09Hc5HYNz9cGI++xlpDCIgDaitVs03ATR84Q==",
+      "dev": true
     },
     "node_modules/fast-glob": {
       "version": "3.3.1",
@@ -8268,7 +8166,8 @@
     "node_modules/fast-json-stable-stringify": {
       "version": "2.1.0",
       "resolved": "https://registry.npmjs.org/fast-json-stable-stringify/-/fast-json-stable-stringify-2.1.0.tgz",
-      "integrity": "sha512-lhd/wF+Lk98HZoTCtlVraHtfh5XYijIjalXck7saUtuanSDyLMxnHhSXEDJqHxD7msR8D0uCmqlkwjCV8xvwHw=="
+      "integrity": "sha512-lhd/wF+Lk98HZoTCtlVraHtfh5XYijIjalXck7saUtuanSDyLMxnHhSXEDJqHxD7msR8D0uCmqlkwjCV8xvwHw==",
+      "dev": true
     },
     "node_modules/fast-plist": {
       "version": "0.1.3",
@@ -8453,27 +8352,6 @@
         "is-callable": "^1.1.3"
       }
     },
-    "node_modules/forever-agent": {
-      "version": "0.6.1",
-      "resolved": "https://registry.npmjs.org/forever-agent/-/forever-agent-0.6.1.tgz",
-      "integrity": "sha512-j0KLYPhm6zeac4lz3oJ3o65qvgQCcPubiyotZrXqEaG4hNagNYO8qdlUrX5vwqv9ohqeT/Z3j6+yW067yWWdUw==",
-      "engines": {
-        "node": "*"
-      }
-    },
-    "node_modules/form-data": {
-      "version": "2.3.3",
-      "resolved": "https://registry.npmjs.org/form-data/-/form-data-2.3.3.tgz",
-      "integrity": "sha512-1lLKB2Mu3aGP1Q/2eCOx0fNbRMe7XdwktwOruhfqqd0rIJWwN4Dh+E3hrPSlDCXnSR7UtZ1N38rVXm+6+MEhJQ==",
-      "dependencies": {
-        "asynckit": "^0.4.0",
-        "combined-stream": "^1.0.6",
-        "mime-types": "^2.1.12"
-      },
-      "engines": {
-        "node": ">= 0.12"
-      }
-    },
     "node_modules/forwarded": {
       "version": "0.2.0",
       "resolved": "https://registry.npmjs.org/forwarded/-/forwarded-0.2.0.tgz",
@@ -8603,14 +8481,6 @@
         "url": "https://github.com/sponsors/sindresorhus"
       }
     },
-    "node_modules/getpass": {
-      "version": "0.1.7",
-      "resolved": "https://registry.npmjs.org/getpass/-/getpass-0.1.7.tgz",
-      "integrity": "sha512-0fzj9JxOLfJ+XGLhR8ze3unN0KZCgZwiSSDz168VERjK8Wl8kVSdcu2kspd4s4wtAa1y/qrVRiAA0WclVsu0ng==",
-      "dependencies": {
-        "assert-plus": "^1.0.0"
-      }
-    },
     "node_modules/glob": {
       "version": "7.2.3",
       "resolved": "https://registry.npmjs.org/glob/-/glob-7.2.3.tgz",
@@ -8681,27 +8551,6 @@
       "optional": true,
       "peer": true
     },
-    "node_modules/har-schema": {
-      "version": "2.0.0",
-      "resolved": "https://registry.npmjs.org/har-schema/-/har-schema-2.0.0.tgz",
-      "integrity": "sha512-Oqluz6zhGX8cyRaTQlFMPw80bSJVG2x/cFb8ZPhUILGgHka9SsokCCOQgpveePerqidZOrT14ipqfJb7ILcW5Q==",
-      "engines": {
-        "node": ">=4"
-      }
-    },
-    "node_modules/har-validator": {
-      "version": "5.1.5",
-      "resolved": "https://registry.npmjs.org/har-validator/-/har-validator-5.1.5.tgz",
-      "integrity": "sha512-nmT2T0lljbxdQZfspsno9hgrG3Uir6Ks5afism62poxqBM6sDnMEuPmzTq8XN0OEwqKLLdh1jQI3qyE66Nzb3w==",
-      "deprecated": "this library is no longer supported",
-      "dependencies": {
-        "ajv": "^6.12.3",
-        "har-schema": "^2.0.0"
-      },
-      "engines": {
-        "node": ">=6"
-      }
-    },
     "node_modules/has": {
       "version": "1.0.4",
       "resolved": "https://registry.npmjs.org/has/-/has-1.0.4.tgz",
@@ -9132,20 +8981,6 @@
         "url": "https://github.com/sponsors/sindresorhus"
       }
     },
-    "node_modules/http-signature": {
-      "version": "1.2.0",
-      "resolved": "https://registry.npmjs.org/http-signature/-/http-signature-1.2.0.tgz",
-      "integrity": "sha512-CAbnr6Rz4CYQkLYUtSNXxQPUH2gK8f3iWexVlsnMeD+GjlsQ0Xsy1cOX+mN3dtxYomRy21CiOzU8Uhw6OwncEQ==",
-      "dependencies": {
-        "assert-plus": "^1.0.0",
-        "jsprim": "^1.2.2",
-        "sshpk": "^1.7.0"
-      },
-      "engines": {
-        "node": ">=0.8",
-        "npm": ">=1.3.7"
-      }
-    },
     "node_modules/human-signals": {
       "version": "2.1.0",
       "resolved": "https://registry.npmjs.org/human-signals/-/human-signals-2.1.0.tgz",
@@ -9653,11 +9488,6 @@
         "url": "https://github.com/sponsors/ljharb"
       }
     },
-    "node_modules/is-typedarray": {
-      "version": "1.0.0",
-      "resolved": "https://registry.npmjs.org/is-typedarray/-/is-typedarray-1.0.0.tgz",
-      "integrity": "sha512-cyA56iCMHAh5CdzjJIa4aohJyeO1YbwLi3Jc35MmRU6poroFjIGZzUzupGiRPOjgHg9TLu43xbpwXk523fMxKA=="
-    },
     "node_modules/is-unicode-supported": {
       "version": "0.1.0",
       "resolved": "https://registry.npmjs.org/is-unicode-supported/-/is-unicode-supported-0.1.0.tgz",
@@ -9718,11 +9548,6 @@
         "node": ">=0.10.0"
       }
     },
-    "node_modules/isstream": {
-      "version": "0.1.2",
-      "resolved": "https://registry.npmjs.org/isstream/-/isstream-0.1.2.tgz",
-      "integrity": "sha512-Yljz7ffyPbrLpLngrMtZ7NduUgVvi6wG9RJ9IUcyCd59YQ911PBJphODUcbOVbqYfxe1wuYf/LJ8PauMRwsM/g=="
-    },
     "node_modules/jest-environment-node": {
       "version": "29.7.0",
       "resolved": "https://registry.npmjs.org/jest-environment-node/-/jest-environment-node-29.7.0.tgz",
@@ -10131,11 +9956,6 @@
         "js-yaml": "bin/js-yaml.js"
       }
     },
-    "node_modules/jsbn": {
-      "version": "0.1.1",
-      "resolved": "https://registry.npmjs.org/jsbn/-/jsbn-0.1.1.tgz",
-      "integrity": "sha512-UVU9dibq2JcFWxQPA6KCqj5O42VOmAY3zQUfEKxU0KpTGXwNoCjkX1e13eHNvw/xPynt6pU0rZ1htjWTNTSXsg=="
-    },
     "node_modules/jsc-android": {
       "version": "250231.0.0",
       "resolved": "https://registry.npmjs.org/jsc-android/-/jsc-android-250231.0.0.tgz",
@@ -10263,20 +10083,11 @@
       "resolved": "https://registry.npmjs.org/json-parse-even-better-errors/-/json-parse-even-better-errors-2.3.1.tgz",
       "integrity": "sha512-xyFwyhro/JEof6Ghe2iz2NcXoj2sloNsWr/XsERDK/oiPCfaNhl5ONfp+jQdAZRQQ0IJWNzH9zIZF7li91kh2w=="
     },
-    "node_modules/json-schema": {
-      "version": "0.4.0",
-      "resolved": "https://registry.npmjs.org/json-schema/-/json-schema-0.4.0.tgz",
-      "integrity": "sha512-es94M3nTIfsEPisRafak+HDLfHXnKBhV3vU5eqPcS3flIWqcxJWgXHXiey3YrpaNsanY5ei1VoYEbOzijuq9BA=="
-    },
     "node_modules/json-schema-traverse": {
       "version": "0.4.1",
       "resolved": "https://registry.npmjs.org/json-schema-traverse/-/json-schema-traverse-0.4.1.tgz",
-      "integrity": "sha512-xbbCH5dCYU5T8LcEhhuh7HJ88HXuW3qsI3Y0zOZFKfZEHcpWiHU/Jxzk629Brsab/mMiHQti9wMP+845RPe3Vg=="
-    },
-    "node_modules/json-stringify-safe": {
-      "version": "5.0.1",
-      "resolved": "https://registry.npmjs.org/json-stringify-safe/-/json-stringify-safe-5.0.1.tgz",
-      "integrity": "sha512-ZClg6AaYvamvYEE82d3Iyd3vSSIjQ+odgjaTzRuO3s7toCdFKczob2i0zCh7JE8kWn17yvAWhUVxvqGwUalsRA=="
+      "integrity": "sha512-xbbCH5dCYU5T8LcEhhuh7HJ88HXuW3qsI3Y0zOZFKfZEHcpWiHU/Jxzk629Brsab/mMiHQti9wMP+845RPe3Vg==",
+      "dev": true
     },
     "node_modules/json5": {
       "version": "2.2.3",
@@ -10348,20 +10159,6 @@
       "resolved": "https://registry.npmjs.org/yallist/-/yallist-4.0.0.tgz",
       "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A=="
     },
-    "node_modules/jsprim": {
-      "version": "1.4.2",
-      "resolved": "https://registry.npmjs.org/jsprim/-/jsprim-1.4.2.tgz",
-      "integrity": "sha512-P2bSOMAc/ciLz6DzgjVlGJP9+BrJWu5UDGK70C2iweC5QBIeFf0ZXRvGjEj2uYgrY2MkAAhsSWHDWlFtEroZWw==",
-      "dependencies": {
-        "assert-plus": "1.0.0",
-        "extsprintf": "1.3.0",
-        "json-schema": "0.4.0",
-        "verror": "1.10.0"
-      },
-      "engines": {
-        "node": ">=0.6.0"
-      }
-    },
     "node_modules/jwa": {
       "version": "1.4.1",
       "resolved": "https://registry.npmjs.org/jwa/-/jwa-1.4.1.tgz",
@@ -10438,22 +10235,22 @@
       }
     },
     "node_modules/lean4": {
-      "version": "0.0.119",
-      "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985",
-      "integrity": "sha512-hA7bb0EFlNwtk7+/7gO5OZS7HtrhmoRacE/b2etFBYG4FbkZd/NKTcs5PHGcKsYXeVghkOOZjw0uhNWaeW3gvw==",
+      "version": "0.0.99",
+      "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?79d345c739bf707024eef5057ccef81b404a2ddf",
+      "integrity": "sha512-jgl4gGQXvP+RhdAr9r0+K6I5SpPkad++zAql9BawHI7OE7vMwK+7GbYXoa5aAP8T1BSIZQ+y3w0cl8FCk5C++A==",
       "license": "Apache-2.0",
       "dependencies": {
-        "@leanprover/infoview": "~0.4.3",
-        "@leanprover/infoview-api": "~0.2.1",
-        "axios": "^1.6.2",
+        "@leanprover/infoview": "~0.3.0",
+        "@leanprover/infoview-api": "~0.2.0",
+        "axios": "~0.24.0",
         "cheerio": "^1.0.0-rc.10",
+        "es-module-shims": "^1.6.2",
         "mobx": "5.15.7",
-        "semver": "^7.5.4",
-        "vscode-languageclient": "=8.0.2",
-        "zod": "^3.22.4"
+        "semver": "=7.3.5",
+        "vscode-languageclient": "=8.0.2"
       },
       "engines": {
-        "vscode": "^1.75.0"
+        "vscode": "^1.70.0"
       }
     },
     "node_modules/lean4-infoview": {
@@ -10472,6 +10269,19 @@
         "vscode-languageserver-protocol": "^3.17.2"
       }
     },
+    "node_modules/lean4/node_modules/@leanprover/infoview": {
+      "version": "0.3.0",
+      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.3.0.tgz",
+      "integrity": "sha512-wVMd9Qc6AC8Ub4cfkENcyCqs342lqwS+4C1SpX+3z0RETxL+TxTFPdM8bYoLgtAg/eApdHhV1TDLSrBNkTWi5g==",
+      "dependencies": {
+        "@leanprover/infoview-api": "~0.2.0",
+        "@vscode/codicons": "^0.0.32",
+        "marked": "^4.2.2",
+        "react-fast-compare": "^3.2.0",
+        "tachyons": "^4.12.0",
+        "vscode-languageserver-protocol": "^3.17.2"
+      }
+    },
     "node_modules/lean4/node_modules/lru-cache": {
       "version": "6.0.0",
       "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-6.0.0.tgz",
@@ -10493,9 +10303,9 @@
       }
     },
     "node_modules/lean4/node_modules/semver": {
-      "version": "7.5.4",
-      "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.4.tgz",
-      "integrity": "sha512-1bCSESV6Pv+i21Hvpxp3Dx+pSD8lIPt8uVjRrxAUt/nbswYc+tK6Y2btiULjd4+fnq15PX+nqQDC7Oft7WkwcA==",
+      "version": "7.3.5",
+      "resolved": "https://registry.npmjs.org/semver/-/semver-7.3.5.tgz",
+      "integrity": "sha512-PoeGJYh8HK4BTO/a9Tf6ZG3veo/A7ZVsYrSA6J8ny9nb3B1VrpkuN+z9OE5wfE5p6H4LchYZsegiQgbJD94ZFQ==",
       "dependencies": {
         "lru-cache": "^6.0.0"
       },
@@ -10513,7 +10323,7 @@
     },
     "node_modules/lean4web": {
       "version": "0.1.0",
-      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#6fc9c11179934cce7ca1f78140c57b6931186b42",
+      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#b02044f3a3b9130b663c3619ce56c603fa3a4cf4",
       "dependencies": {
         "@emotion/react": "^11.11.1",
         "@emotion/styled": "^11.11.0",
@@ -10522,13 +10332,12 @@
         "@fortawesome/fontawesome-svg-core": "^6.2.0",
         "@fortawesome/free-solid-svg-icons": "^6.2.0",
         "@fortawesome/react-fontawesome": "^0.2.0",
-        "@leanprover/infoview": "^0.4.3",
+        "@leanprover/infoview": "^0.4.1",
         "@mui/material": "^5.13.7",
-        "@vitejs/plugin-react-swc": "^3.4.0",
         "express": "^4.18.2",
         "file-saver": "^2.0.5",
         "ip-anonymize": "^0.1.0",
-        "lean4": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985",
+        "lean4": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?79d345c739bf707024eef5057ccef81b404a2ddf",
         "mobx": "^6.6.2",
         "moment-timezone": "^0.5.39",
         "monaco-editor": "^0.34.1",
@@ -10543,7 +10352,6 @@
         "react-popper": "^2.3.0",
         "react-split": "^2.0.14",
         "stream-http": "^3.2.0",
-        "vite": "^4.5.0",
         "vscode-ws-jsonrpc": "^2.0.0",
         "ws": "^8.9.0"
       }
@@ -12809,9 +12617,9 @@
       }
     },
     "node_modules/nodemon": {
-      "version": "3.0.1",
-      "resolved": "https://registry.npmjs.org/nodemon/-/nodemon-3.0.1.tgz",
-      "integrity": "sha512-g9AZ7HmkhQkqXkRc20w+ZfQ73cHLbE8hnPbtaFbFtCumZsjyMhKk9LajQ07U5Ux28lvFjZ5X7HvWR1xzU8jHVw==",
+      "version": "2.0.22",
+      "resolved": "https://registry.npmjs.org/nodemon/-/nodemon-2.0.22.tgz",
+      "integrity": "sha512-B8YqaKMmyuCO7BowF1Z1/mkPqLk6cs/l63Ojtd6otKjMx47Dq1utxfRxcavH1I7VSaL8n5BUaoutadnsX3AAVQ==",
       "dev": true,
       "dependencies": {
         "chokidar": "^3.5.2",
@@ -12819,8 +12627,8 @@
         "ignore-by-default": "^1.0.1",
         "minimatch": "^3.1.2",
         "pstree.remy": "^1.1.8",
-        "semver": "^7.5.3",
-        "simple-update-notifier": "^2.0.0",
+        "semver": "^5.7.1",
+        "simple-update-notifier": "^1.0.7",
         "supports-color": "^5.5.0",
         "touch": "^3.1.0",
         "undefsafe": "^2.0.5"
@@ -12829,7 +12637,7 @@
         "nodemon": "bin/nodemon.js"
       },
       "engines": {
-        "node": ">=10"
+        "node": ">=8.10.0"
       },
       "funding": {
         "type": "opencollective",
@@ -12845,39 +12653,15 @@
         "ms": "^2.1.1"
       }
     },
-    "node_modules/nodemon/node_modules/lru-cache": {
-      "version": "6.0.0",
-      "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-6.0.0.tgz",
-      "integrity": "sha512-Jo6dJ04CmSjuznwJSS3pUeWmd/H0ffTlkXXgwZi+eq1UCmqQwCh+eLsYOYCwY991i2Fah4h1BEMCx4qThGbsiA==",
-      "dev": true,
-      "dependencies": {
-        "yallist": "^4.0.0"
-      },
-      "engines": {
-        "node": ">=10"
-      }
-    },
     "node_modules/nodemon/node_modules/semver": {
-      "version": "7.5.4",
-      "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.4.tgz",
-      "integrity": "sha512-1bCSESV6Pv+i21Hvpxp3Dx+pSD8lIPt8uVjRrxAUt/nbswYc+tK6Y2btiULjd4+fnq15PX+nqQDC7Oft7WkwcA==",
+      "version": "5.7.2",
+      "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.2.tgz",
+      "integrity": "sha512-cBznnQ9KjJqU67B52RMC65CMarK2600WFnbkcaiwWq3xy/5haFJlshgnpjovMVJ+Hff49d8GEn0b87C5pDQ10g==",
       "dev": true,
-      "dependencies": {
-        "lru-cache": "^6.0.0"
-      },
       "bin": {
-        "semver": "bin/semver.js"
-      },
-      "engines": {
-        "node": ">=10"
+        "semver": "bin/semver"
       }
     },
-    "node_modules/nodemon/node_modules/yallist": {
-      "version": "4.0.0",
-      "resolved": "https://registry.npmjs.org/yallist/-/yallist-4.0.0.tgz",
-      "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A==",
-      "dev": true
-    },
     "node_modules/nopt": {
       "version": "1.0.10",
       "resolved": "https://registry.npmjs.org/nopt/-/nopt-1.0.10.tgz",
@@ -12928,14 +12712,6 @@
       "resolved": "https://registry.npmjs.org/nullthrows/-/nullthrows-1.1.1.tgz",
       "integrity": "sha512-2vPPEi+Z7WqML2jZYddDIfy5Dqb0r2fze2zTxNNknZaFpVHU3mFB3R+DWeJWGVx0ecvttSGlJTI+WG+8Z4cDWw=="
     },
-    "node_modules/oauth-sign": {
-      "version": "0.9.0",
-      "resolved": "https://registry.npmjs.org/oauth-sign/-/oauth-sign-0.9.0.tgz",
-      "integrity": "sha512-fexhUFFPTGV8ybAtSIGbV6gOkSv8UtRbDBnAyLQw4QPKkgNlsH2ByPGtMUqdWkos6YCRmAqViwgZrJc/mRDzZQ==",
-      "engines": {
-        "node": "*"
-      }
-    },
     "node_modules/ob1": {
       "version": "0.76.8",
       "resolved": "https://registry.npmjs.org/ob1/-/ob1-0.76.8.tgz",
@@ -13344,11 +13120,6 @@
         "node": ">=8"
       }
     },
-    "node_modules/performance-now": {
-      "version": "2.1.0",
-      "resolved": "https://registry.npmjs.org/performance-now/-/performance-now-2.1.0.tgz",
-      "integrity": "sha512-7EAHlyLHI56VEIdK57uwHdHKIaAGbnXPiw0yWbarQZOKaKpvUIgW0jWRVLiatnM+XXlSwsanIBH/hzGMJulMow=="
-    },
     "node_modules/picocolors": {
       "version": "1.0.0",
       "resolved": "https://registry.npmjs.org/picocolors/-/picocolors-1.0.0.tgz",
@@ -13579,16 +13350,6 @@
         "node": ">= 0.10"
       }
     },
-    "node_modules/proxy-from-env": {
-      "version": "1.1.0",
-      "resolved": "https://registry.npmjs.org/proxy-from-env/-/proxy-from-env-1.1.0.tgz",
-      "integrity": "sha512-D+zkORCbA9f1tdWRK0RaCR3GPv50cMxcrz4X8k5LTSUD1Dkw47mKJEZQNunItRTkWwgtaUSo1RVFRIG9ZXiFYg=="
-    },
-    "node_modules/psl": {
-      "version": "1.9.0",
-      "resolved": "https://registry.npmjs.org/psl/-/psl-1.9.0.tgz",
-      "integrity": "sha512-E/ZsdU4HLs/68gYzgGTkMicWTLPdAftJLfJFlLUAAKZGkStNU72sZjT66SnMDVOfOWY/YAoiD7Jxa9iHvngcag=="
-    },
     "node_modules/pstree.remy": {
       "version": "1.1.8",
       "resolved": "https://registry.npmjs.org/pstree.remy/-/pstree.remy-1.1.8.tgz",
@@ -13599,6 +13360,7 @@
       "version": "2.3.0",
       "resolved": "https://registry.npmjs.org/punycode/-/punycode-2.3.0.tgz",
       "integrity": "sha512-rRV+zQD8tVFys26lAGR9WUuS4iUAngJScM+ZRSKtvl5tKeZ2t5bvdNFdNHBW9FWR4guGHlgmsZ1G7BSm2wTbuA==",
+      "dev": true,
       "engines": {
         "node": ">=6"
       }
@@ -14310,37 +14072,6 @@
         "url": "https://opencollective.com/unified"
       }
     },
-    "node_modules/request": {
-      "version": "2.88.2",
-      "resolved": "https://registry.npmjs.org/request/-/request-2.88.2.tgz",
-      "integrity": "sha512-MsvtOrfG9ZcrOwAW+Qi+F6HbD0CWXEh9ou77uOb7FM2WPhwT7smM833PzanhJLsgXjN89Ir6V2PczXNnMpwKhw==",
-      "deprecated": "request has been deprecated, see https://github.com/request/request/issues/3142",
-      "dependencies": {
-        "aws-sign2": "~0.7.0",
-        "aws4": "^1.8.0",
-        "caseless": "~0.12.0",
-        "combined-stream": "~1.0.6",
-        "extend": "~3.0.2",
-        "forever-agent": "~0.6.1",
-        "form-data": "~2.3.2",
-        "har-validator": "~5.1.3",
-        "http-signature": "~1.2.0",
-        "is-typedarray": "~1.0.0",
-        "isstream": "~0.1.2",
-        "json-stringify-safe": "~5.0.1",
-        "mime-types": "~2.1.19",
-        "oauth-sign": "~0.9.0",
-        "performance-now": "^2.1.0",
-        "qs": "~6.5.2",
-        "safe-buffer": "^5.1.2",
-        "tough-cookie": "~2.5.0",
-        "tunnel-agent": "^0.6.0",
-        "uuid": "^3.3.2"
-      },
-      "engines": {
-        "node": ">= 6"
-      }
-    },
     "node_modules/request-progress": {
       "version": "3.0.0",
       "resolved": "https://registry.npmjs.org/request-progress/-/request-progress-3.0.0.tgz",
@@ -14349,23 +14080,6 @@
         "throttleit": "^1.0.0"
       }
     },
-    "node_modules/request/node_modules/qs": {
-      "version": "6.5.3",
-      "resolved": "https://registry.npmjs.org/qs/-/qs-6.5.3.tgz",
-      "integrity": "sha512-qxXIEh4pCGfHICj1mAJQ2/2XVZkjCDTcEgfoSQxc/fYivUZxTkk7L3bDBJSoNrEzXI17oUO5Dp07ktqE5KzczA==",
-      "engines": {
-        "node": ">=0.6"
-      }
-    },
-    "node_modules/request/node_modules/uuid": {
-      "version": "3.4.0",
-      "resolved": "https://registry.npmjs.org/uuid/-/uuid-3.4.0.tgz",
-      "integrity": "sha512-HjSDRw6gZE5JMggctHBcjVak08+KEVhSIiDzFnT9S9aegmp85S/bReBVTb4QTFaRNptJ9kuYaNhnbNEOkbKb/A==",
-      "deprecated": "Please upgrade  to version 7 or higher.  Older versions may use Math.random() in certain circumstances, which is known to be problematic.  See https://v8.dev/blog/math-random for details.",
-      "bin": {
-        "uuid": "bin/uuid"
-      }
-    },
     "node_modules/require-directory": {
       "version": "2.1.1",
       "resolved": "https://registry.npmjs.org/require-directory/-/require-directory-2.1.1.tgz",
@@ -14869,50 +14583,26 @@
       "integrity": "sha512-wnD2ZE+l+SPC/uoS0vXeE9L1+0wuaMqKlfz9AMUo38JsyLSBWSFcHR1Rri62LZc12vLr1gb3jl7iwQhgwpAbGQ=="
     },
     "node_modules/simple-update-notifier": {
-      "version": "2.0.0",
-      "resolved": "https://registry.npmjs.org/simple-update-notifier/-/simple-update-notifier-2.0.0.tgz",
-      "integrity": "sha512-a2B9Y0KlNXl9u/vsW6sTIu9vGEpfKu2wRV6l1H3XEas/0gUIzGzBoP/IouTcUQbm9JWZLH3COxyn03TYlFax6w==",
+      "version": "1.1.0",
+      "resolved": "https://registry.npmjs.org/simple-update-notifier/-/simple-update-notifier-1.1.0.tgz",
+      "integrity": "sha512-VpsrsJSUcJEseSbMHkrsrAVSdvVS5I96Qo1QAQ4FxQ9wXFcB+pjj7FB7/us9+GcgfW4ziHtYMc1J0PLczb55mg==",
       "dev": true,
       "dependencies": {
-        "semver": "^7.5.3"
+        "semver": "~7.0.0"
       },
       "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/simple-update-notifier/node_modules/lru-cache": {
-      "version": "6.0.0",
-      "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-6.0.0.tgz",
-      "integrity": "sha512-Jo6dJ04CmSjuznwJSS3pUeWmd/H0ffTlkXXgwZi+eq1UCmqQwCh+eLsYOYCwY991i2Fah4h1BEMCx4qThGbsiA==",
-      "dev": true,
-      "dependencies": {
-        "yallist": "^4.0.0"
-      },
-      "engines": {
-        "node": ">=10"
+        "node": ">=8.10.0"
       }
     },
     "node_modules/simple-update-notifier/node_modules/semver": {
-      "version": "7.5.4",
-      "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.4.tgz",
-      "integrity": "sha512-1bCSESV6Pv+i21Hvpxp3Dx+pSD8lIPt8uVjRrxAUt/nbswYc+tK6Y2btiULjd4+fnq15PX+nqQDC7Oft7WkwcA==",
+      "version": "7.0.0",
+      "resolved": "https://registry.npmjs.org/semver/-/semver-7.0.0.tgz",
+      "integrity": "sha512-+GB6zVA9LWh6zovYQLALHwv5rb2PHGlJi3lfiqIHxR0uuwCgefcOJc59v9fv1w8GbStwxuuqqAjI9NMAOOgq1A==",
       "dev": true,
-      "dependencies": {
-        "lru-cache": "^6.0.0"
-      },
       "bin": {
         "semver": "bin/semver.js"
-      },
-      "engines": {
-        "node": ">=10"
       }
     },
-    "node_modules/simple-update-notifier/node_modules/yallist": {
-      "version": "4.0.0",
-      "resolved": "https://registry.npmjs.org/yallist/-/yallist-4.0.0.tgz",
-      "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A==",
-      "dev": true
-    },
     "node_modules/sisteransi": {
       "version": "1.0.5",
       "resolved": "https://registry.npmjs.org/sisteransi/-/sisteransi-1.0.5.tgz",
@@ -15045,30 +14735,6 @@
       "resolved": "https://registry.npmjs.org/sprintf-js/-/sprintf-js-1.0.3.tgz",
       "integrity": "sha512-D9cPgkvLlV3t3IzL0D0YLvGA9Ahk4PcvVwUbN0dSGr1aP0Nrt4AEnTUbuGvquEC0mA64Gqt1fzirlRs5ibXx8g=="
     },
-    "node_modules/sshpk": {
-      "version": "1.18.0",
-      "resolved": "https://registry.npmjs.org/sshpk/-/sshpk-1.18.0.tgz",
-      "integrity": "sha512-2p2KJZTSqQ/I3+HX42EpYOa2l3f8Erv8MWKsy2I9uf4wA7yFIkXRffYdsx86y6z4vHtV8u7g+pPlr8/4ouAxsQ==",
-      "dependencies": {
-        "asn1": "~0.2.3",
-        "assert-plus": "^1.0.0",
-        "bcrypt-pbkdf": "^1.0.0",
-        "dashdash": "^1.12.0",
-        "ecc-jsbn": "~0.1.1",
-        "getpass": "^0.1.1",
-        "jsbn": "~0.1.0",
-        "safer-buffer": "^2.0.2",
-        "tweetnacl": "~0.14.0"
-      },
-      "bin": {
-        "sshpk-conv": "bin/sshpk-conv",
-        "sshpk-sign": "bin/sshpk-sign",
-        "sshpk-verify": "bin/sshpk-verify"
-      },
-      "engines": {
-        "node": ">=0.10.0"
-      }
-    },
     "node_modules/stack-utils": {
       "version": "2.0.6",
       "resolved": "https://registry.npmjs.org/stack-utils/-/stack-utils-2.0.6.tgz",
@@ -15472,18 +15138,6 @@
         "nodetouch": "bin/nodetouch.js"
       }
     },
-    "node_modules/tough-cookie": {
-      "version": "2.5.0",
-      "resolved": "https://registry.npmjs.org/tough-cookie/-/tough-cookie-2.5.0.tgz",
-      "integrity": "sha512-nlLsUzgm1kfLXSXfRZMc1KLAugd4hqJHDTvc2hDIwS3mZAfMEuMbc03SujMF+GEcpaX/qboeycw6iO8JwVv2+g==",
-      "dependencies": {
-        "psl": "^1.1.28",
-        "punycode": "^2.1.1"
-      },
-      "engines": {
-        "node": ">=0.8"
-      }
-    },
     "node_modules/tr46": {
       "version": "0.0.3",
       "resolved": "https://registry.npmjs.org/tr46/-/tr46-0.0.3.tgz",
@@ -15653,22 +15307,6 @@
       "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.6.2.tgz",
       "integrity": "sha512-AEYxH93jGFPn/a2iVAwW87VuUIkR1FVUKB77NwMF7nBTDkDrrT/Hpt/IrCJ0QXhW27jTBDcf5ZY7w6RiqTMw2Q=="
     },
-    "node_modules/tunnel-agent": {
-      "version": "0.6.0",
-      "resolved": "https://registry.npmjs.org/tunnel-agent/-/tunnel-agent-0.6.0.tgz",
-      "integrity": "sha512-McnNiV1l8RYeY8tBgEpuodCC1mLUdbSN+CYBL7kJsJNInOP8UjDDEwdk6Mw60vdLLrr5NHKZhMAOSrR2NZuQ+w==",
-      "dependencies": {
-        "safe-buffer": "^5.0.1"
-      },
-      "engines": {
-        "node": "*"
-      }
-    },
-    "node_modules/tweetnacl": {
-      "version": "0.14.5",
-      "resolved": "https://registry.npmjs.org/tweetnacl/-/tweetnacl-0.14.5.tgz",
-      "integrity": "sha512-KXXFFdAbFXY4geFIwoyNK+f5Z1b7swfXABfL7HXCmoIWMKU3dmS26672A4EeQtDzLKy7SXmfBu51JolvEKwtGA=="
-    },
     "node_modules/type-detect": {
       "version": "4.0.8",
       "resolved": "https://registry.npmjs.org/type-detect/-/type-detect-4.0.8.tgz",
@@ -15966,6 +15604,7 @@
       "version": "4.4.1",
       "resolved": "https://registry.npmjs.org/uri-js/-/uri-js-4.4.1.tgz",
       "integrity": "sha512-7rKUyy33Q1yc98pQ1DAmLtwX109F7TIfWlW1Ydo8Wl1ii1SeHieeh0HHfPeL2fMXK6z0s8ecKs9frCuLJvndBg==",
+      "dev": true,
       "dependencies": {
         "punycode": "^2.1.0"
       }
@@ -16062,24 +15701,6 @@
         "node": ">= 0.8"
       }
     },
-    "node_modules/verror": {
-      "version": "1.10.0",
-      "resolved": "https://registry.npmjs.org/verror/-/verror-1.10.0.tgz",
-      "integrity": "sha512-ZZKSmDAEFOijERBLkmYfJ+vmk3w+7hOLYDNkRCuRuMJGEmqYNCNLyBBFwWKVMhfwaEF3WOd0Zlw86U/WC/+nYw==",
-      "engines": [
-        "node >=0.6.0"
-      ],
-      "dependencies": {
-        "assert-plus": "^1.0.0",
-        "core-util-is": "1.0.2",
-        "extsprintf": "^1.2.0"
-      }
-    },
-    "node_modules/verror/node_modules/core-util-is": {
-      "version": "1.0.2",
-      "resolved": "https://registry.npmjs.org/core-util-is/-/core-util-is-1.0.2.tgz",
-      "integrity": "sha512-3lqz5YjWTYnW6dlDa5TLaTCcShfar1e40rmcJVwCBJC6mWlFuj0eCHIElmG1g5kyuJ/GD+8Wn4FFCcz4gJPfaQ=="
-    },
     "node_modules/vfile": {
       "version": "5.3.7",
       "resolved": "https://registry.npmjs.org/vfile/-/vfile-5.3.7.tgz",
@@ -16122,9 +15743,9 @@
       }
     },
     "node_modules/vite": {
-      "version": "4.5.1",
-      "resolved": "https://registry.npmjs.org/vite/-/vite-4.5.1.tgz",
-      "integrity": "sha512-AXXFaAJ8yebyqzoNB9fu2pHoo/nWX+xZlaRwoeYUxEqBO+Zj4msE5G+BhGBll9lYEKv9Hfks52PAF2X7qDYXQA==",
+      "version": "4.5.0",
+      "resolved": "https://registry.npmjs.org/vite/-/vite-4.5.0.tgz",
+      "integrity": "sha512-ulr8rNLA6rkyFAlVWw2q5YJ91v098AFQ2R0PRFwPzREXOUJQPtFUG0t+/ZikhaOCDqFoDhN6/v8Sq0o4araFAw==",
       "dependencies": {
         "esbuild": "^0.18.10",
         "postcss": "^8.4.27",
@@ -17025,14 +16646,6 @@
         "url": "https://github.com/sponsors/sindresorhus"
       }
     },
-    "node_modules/zod": {
-      "version": "3.22.4",
-      "resolved": "https://registry.npmjs.org/zod/-/zod-3.22.4.tgz",
-      "integrity": "sha512-iC+8Io04lddc+mVqQ9AZ7OQ2MrUKGN+oIQyq1vemgt46jwCwLfhq7/pwnBnNXXXZb8VTVLKwp9EDkx+ryxIWmg==",
-      "funding": {
-        "url": "https://github.com/sponsors/colinhacks"
-      }
-    },
     "node_modules/zwitch": {
       "version": "2.0.4",
       "resolved": "https://registry.npmjs.org/zwitch/-/zwitch-2.0.4.tgz",

package.json

@@ -1,7 +1,6 @@
 {
   "name": "lean4-game",
   "version": "0.1.0",
-  "type": "module",
   "private": true,
   "homepage": ".",
   "dependencies": {
@@ -17,6 +16,7 @@
     "@types/cytoscape": "^3.19.9",
     "@types/react-router-dom": "^5.3.3",
     "@vitejs/plugin-react-swc": "^3.4.0",
+    "coi-serviceworker": "^0.1.7",
     "cross-env": "^7.0.3",
     "cytoscape": "^3.23.0",
     "cytoscape-elk": "^2.1.0",
@@ -37,7 +37,6 @@
     "rehype-katex": "^6.0.2",
     "remark-gfm": "^3.0.1",
     "remark-math": "^5.1.1",
-    "request": "^2.88.2",
     "request-progress": "^3.0.0",
     "vite": "^4.5.0",
     "vite-plugin-static-copy": "^0.17.0",
@@ -54,7 +53,7 @@
     "concurrently": "^7.6.0",
     "css-loader": "^6.7.3",
     "file-loader": "^6.2.0",
-    "nodemon": "^3.0.1",
+    "nodemon": "^2.0.20",
     "react-refresh": "^0.14.0",
     "style-loader": "^3.3.1",
     "ts-loader": "^9.4.2",
@@ -63,13 +62,12 @@
   },
   "scripts": {
     "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
-    "start_server": "(cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\")",
+    "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",
     "build": "npm run build_server && npm run build_client",
-    "preview": "vite preview",
     "build_server": "cd server && lake build",
     "build_client": "cross-env NODE_ENV=production vite build",
-    "production": "cross-env NODE_ENV=production node relay/index.mjs"
+    "production": "cross-env NODE_ENV=production node server/index.mjs"
   },
   "eslintConfig": {
     "extends": [

relay/unpack.sh

@@ -1,30 +0,0 @@
-#/bin/bash
-
-ARTIFACT_ID=$1
-OWNER=$2
-REPO=$3
-
-# mkdir -p games
-cd games
-
-# mkdir -p tmp
-mkdir -p ${OWNER}
-
-echo "Unpacking ZIP."
-unzip -o tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip -d tmp/${OWNER}_${REPO}_${ARTIFACT_ID}
-echo "Unpacking game."
-
-# exit the npm project to avoid reloading. TODO: Where should we actually save these?
-
-
-
-echo "Delete old version of the game"
-rm -rf ${OWNER}/${REPO}
-mkdir -p ${OWNER}/${REPO}
-
-for f in tmp/${OWNER}_${REPO}_${ARTIFACT_ID}/* #Should only be one file
-do
-  echo "Unpacking $f"
-  #tar -xvzf $f -C games/${OWNER}/${REPO}
-  unzip -q -o $f -d ${OWNER}/${REPO}
-done

server/.gitignore

@@ -0,0 +1,3 @@
+.lake
+adam
+lakefile32.olean

server/GameServer.lean

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

server/GameServer/Commands.lean

@@ -46,9 +46,7 @@ elab "Title" t:str : command => do
   match ← getCurLayer with
   | .Level => modifyCurLevel fun level => pure {level with title := t.getString}
   | .World => modifyCurWorld  fun world => pure {world with title := t.getString}
-  | .Game => modifyCurGame  fun game => pure {game with
-      title := t.getString
-      tile := {game.tile with title := t.getString}}
+  | .Game => modifyCurGame  fun game => pure {game with title := t.getString}
 
 /-- Define the introduction of the current game/world/level. -/
 elab "Introduction" t:str : command => do
@@ -60,32 +58,10 @@ elab "Introduction" t:str : command => do
 /-- Define the info of the current game. Used for e.g. credits -/
 elab "Info" t:str : command => do
   match ← getCurLayer with
-  | .Level =>
-    logError "Can't use `Info` in a level!"
-    pure ()
-  | .World =>
-    logError "Can't use `Info` in a world"
-    pure ()
+  | .Level => pure ()
+  | .World => pure ()
   | .Game => modifyCurGame  fun game => pure {game with info := t.getString}
 
-/-- Provide the location of the image for the current game/world/level.
-Paths are relative to the lean project's root. -/
-elab "Image" t:str : command => do
-  let file := t.getString
-  if not <| ← System.FilePath.pathExists file then
-    logWarningAt t s!"Make sure the cover image '{file}' exists."
-  if not <| file.startsWith "images/" then
-    logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."
-
-  match ← getCurLayer with
-  | .Level =>
-    logWarning "Level-images not implemented yet" -- TODO
-    modifyCurLevel fun level => pure {level with image := file}
-  | .World =>
-    modifyCurWorld  fun world => pure {world with image := file}
-  | .Game =>
-    logWarning "Main image of the game not implemented yet" -- TODO
-    modifyCurGame  fun game => pure {game with image := file}
 
 /-- Define the conclusion of the current game or current level if some
 building a level. -/
@@ -95,38 +71,6 @@ elab "Conclusion" t:str : command => do
   | .World => modifyCurWorld  fun world => pure {world with conclusion := t.getString}
   | .Game => modifyCurGame  fun game => pure {game with conclusion := t.getString}
 
-/-- A list of games that should be played before this one. Example `Prerequisites "NNG" "STG"`. -/
-elab "Prerequisites" t:str* : command => do
-  modifyCurGame fun game => pure {game with
-    tile := {game.tile with prerequisites := t.map (·.getString) |>.toList}}
-
-/-- Short caption for the game (1 sentence) -/
-elab "CaptionShort" t:str : command => do
-  modifyCurGame fun game => pure {game with
-    tile := {game.tile with short := t.getString}}
-
-/-- More detailed description what the game is about (2-4 sentences). -/
-elab "CaptionLong" t:str : command => do
-  modifyCurGame fun game => pure {game with
-    tile := {game.tile with long := t.getString}}
-
-/-- A list of Languages the game is translated to. For example `Languages "German" "English"`.
-NOTE: For the time being, only a single language is supported.
- -/
-elab "Languages" t:str* : command => do
-  modifyCurGame fun game => pure {game with
-    tile := {game.tile with languages := t.map (·.getString) |>.toList}}
-
-/-- The Image of the game (optional). TODO: Not impementeds -/
-elab "CoverImage" t:str : command => do
-  let file := t.getString
-  if not <| ← System.FilePath.pathExists file then
-    logWarningAt t s!"Make sure the cover image '{file}' exists."
-  if not <| file.startsWith "images/" then
-    logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."
-
-  modifyCurGame fun game => pure {game with
-    tile := {game.tile with image := file}}
 
 /-! # Inventory
 
@@ -682,27 +626,6 @@ elab "Template" tacs:tacticSeq : tactic => do
   modifyLevel (←getCurLevelId) fun level => do
     return {level with template := s!"{template}"}
 
-
-
-open IO.FS System FilePath in
-/-- Copies the folder `images/` to `.lake/gamedata/images/` -/
-def copyImages : IO Unit := do
-  let target : FilePath := ".lake" / "gamedata"
-  if ← FilePath.pathExists "images" then
-    for file in ← walkDir "images" do
-      let outFile := target.join file
-      -- create the directories
-      if ← file.isDir then
-        createDirAll outFile
-      else
-        if let some parent := outFile.parent then
-          createDirAll parent
-        -- copy file
-        let content ← readBinFile file
-        writeBinFile outFile content
-
-
-
 -- TODO: Notes for testing if a declaration has the simp attribute
 
 -- -- Test: From zulip
@@ -721,47 +644,6 @@ def copyImages : IO Unit := do
 
 /-! # Make Game -/
 
-#eval IO.FS.createDirAll ".lake/gamedata/"
-
--- TODO: register all of this as ToJson instance?
-def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do
-  let game ← getCurGame
-  let env ← getEnv
-  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
-
-  if ← path.isDir then
-    IO.FS.removeDirAll path
-  IO.FS.createDirAll path
-
-  -- copy the images folder
-  copyImages
-
-  for (worldId, world) in game.worlds.nodes.toArray do
-    for (levelId, level) in world.levels.toArray do
-      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
-
-  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
-
-  for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
-    for name in allItemsByType.findD inventoryType {} do
-      let some item ← getInventoryItem? name inventoryType
-        | throwError "Expected item to exist: {name}"
-      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
-
-  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
-    (allItemsByType.findD type {}).toArray.mapM (fun name => do
-      let some item ← getInventoryItem? name type
-        | throwError "Expected item to exist: {name}"
-      return item.toTile)
-  let inventory : InventoryOverview := {
-    lemmas := ← getTiles .Lemma
-    tactics := ← getTiles .Tactic
-    definitions := ← getTiles .Definition
-    lemmaTab := none
-  }
-  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))
-
-
 def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
 | .Tactic => level.tactics
 | .Definition => level.definitions
@@ -928,12 +810,8 @@ elab "MakeGame" : command => do
   -- Items that should not be displayed in inventory
   let mut hiddenItems : HashSet Name := {}
 
-  let allWorlds := game.worlds.nodes.toArray
-  let nrWorlds := allWorlds.size
-  let mut nrLevels := 0
-
   -- Calculate which "items" are used/new in which world
-  for (worldId, world) in allWorlds do
+  for (worldId, world) in game.worlds.nodes.toArray do
     let mut usedItems : HashSet Name := {}
     let mut newItems : HashSet Name := {}
     for inventoryType in #[.Tactic, .Definition, .Lemma] do
@@ -972,12 +850,9 @@ elab "MakeGame" : command => do
     -- logInfo m!"{worldId} uses: {usedItems.toList}"
     -- logInfo m!"{worldId} introduces: {newItems.toList}"
 
-    -- Moreover, count the number of levels in the game
-    nrLevels := nrLevels + world.levels.toArray.size
-
   /- for each "item" this is a HashSet of `worldId`s that introduce this item -/
   let mut worldsWithNewItem : HashMap Name (HashSet Name) := {}
-  for (worldId, _world) in allWorlds do
+  for (worldId, _world) in game.worlds.nodes.toArray do
     for newItem in newItemsInWorld.findD worldId {} do
       worldsWithNewItem := worldsWithNewItem.insert newItem $
         (worldsWithNewItem.findD newItem {}).insert worldId
@@ -989,7 +864,7 @@ elab "MakeGame" : command => do
   let mut dependencyReasons : HashMap (Name × Name) (HashSet Name) := {}
 
   -- Calculate world dependency graph `game.worlds`
-  for (dependentWorldId, _dependentWorld) in allWorlds do
+  for (dependentWorldId, _dependentWorld) in game.worlds.nodes.toArray do
     let mut dependsOnWorlds : HashSet Name := {}
     -- Adding manual dependencies that were specified via the `Dependency` command.
     for (sourceId, targetId) in game.worlds.edges do
@@ -1040,25 +915,14 @@ elab "MakeGame" : command => do
         logError m!"{w1} depends on {w2} because of {items.toList}."
   else
     worldDependsOnWorlds ← removeTransitive worldDependsOnWorlds
-
-    -- need to delete all existing edges as they are already present in `worldDependsOnWorlds`.
-    modifyCurGame fun game =>
-      pure {game with worlds := {game.worlds with edges := Array.empty}}
-
     for (dependentWorldId, worldIds) in worldDependsOnWorlds.toArray do
       modifyCurGame fun game =>
         pure {game with worlds := {game.worlds with
           edges := game.worlds.edges.append (worldIds.toArray.map fun wid => (wid, dependentWorldId))}}
 
-  -- Add the number of levels and worlds to the tile for the landing page
-  modifyCurGame fun game => pure {game with tile := {game.tile with
-    levels := nrLevels
-    worlds := nrWorlds }}
-
   -- Apparently we need to reload `game` to get the changes to `game.worlds` we just made
   let game ← getCurGame
 
-  let mut allItemsByType : HashMap InventoryType (HashSet Name) := {}
   -- Compute which inventory items are available in which level:
   for inventoryType in #[.Tactic, .Definition, .Lemma] do
 
@@ -1188,9 +1052,6 @@ elab "MakeGame" : command => do
 
         modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
           return level.setComputedInventory inventoryType itemsArray
-    allItemsByType := allItemsByType.insert inventoryType allItems
-
-  saveGameData allItemsByType
 
 /-! # Debugging tools -/
 

server/GameServer/EnvExtensions.lean

@@ -108,12 +108,6 @@ structure InventoryTile where
   hidden := false
 deriving ToJson, FromJson, Repr, Inhabited
 
-def InventoryItem.toTile (item : InventoryItem) : InventoryTile := {
-      name := item.name,
-      displayName := item.displayName
-      category := item.category
-}
-
 /-- The extension that stores the doc templates. Note that you can only add, but never modify
 entries! -/
 initialize inventoryTemplateExt :
@@ -141,12 +135,7 @@ def getInventoryItem? [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
     m (Option InventoryItem) := do
   return (inventoryExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
 
-structure InventoryOverview where
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  lemmaTab : Option String
-deriving ToJson, FromJson
+
 
 /-! ## Environment extensions for game specification -/
 
@@ -265,68 +254,8 @@ structure GameLevel where
   lemmas: InventoryInfo := default
   /-- A proof template that is printed in an empty editor. -/
   template: Option String := none
-  /-- The image for this level. -/
-  image : String := default
-deriving Inhabited, Repr
+  deriving Inhabited, Repr
 
-structure WorldOverview where
-  world: Name
-  tactics: Array InventoryTile := default
-  definitions: Array InventoryTile := default
-  lemmas: Array InventoryTile := default
-  deriving FromJson, ToJson, Inhabited, Repr
-
-/-- Json-encodable version of `GameLevel`
-Fields:
-- description: Lemma in mathematical language.
-- descriptionGoal: Lemma printed as Lean-Code.
--/
-structure LevelInfo where
-  index : Nat
-  title : String
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  introduction : String
-  conclusion : String
-  descrText : Option String := none
-  descrFormat : String := ""
-  lemmaTab : Option String
-  displayName : Option String
-  statementName : Option String
-  template : Option String
-  image: Option String
-deriving ToJson, FromJson
-
-def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
-  { index := lvl.index,
-    title := lvl.title,
-    tactics := lvl.tactics.tiles,
-    lemmas := lvl.lemmas.tiles,
-    definitions := lvl.definitions.tiles,
-    descrText := lvl.descrText,
-    descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
-    introduction := lvl.introduction
-    conclusion := lvl.conclusion
-    lemmaTab := match lvl.lemmaTab with
-    | some tab => tab
-    | none =>
-      -- Try to set the lemma tab to the category of the first added lemma
-      match lvl.lemmas.tiles.find? (·.new) with
-      | some tile => tile.category
-      | none => none
-    statementName := lvl.statementName.toString
-    displayName := match lvl.statementName with
-      | .anonymous => none
-      | name => match (inventoryExt.getState env).find?
-          (fun x => x.name == name && x.type == .Lemma) with
-        | some n => n.displayName
-        | none => name.toString
-        -- Note: we could call `.find!` because we check in `Statement` that the
-        -- lemma doc must exist.
-    template := lvl.template
-    image := lvl.image
-  }
 
 /-! ## World -/
 
@@ -342,46 +271,17 @@ structure World where
   conclusion : String := default
   /-- The levels of the world. -/
   levels: HashMap Nat GameLevel := default
-  /-- The introduction image of the world. -/
-  image: String := default
 deriving Inhabited
 
 instance : ToJson World := ⟨
   fun world => Json.mkObj [
     ("name", toJson world.name),
     ("title", world.title),
-    ("introduction", world.introduction),
-    ("image", world.image)]
+    ("introduction", world.introduction)]
 ⟩
 
 /-! ## Game -/
 
-/-- A tile as they are displayed on the servers landing page. -/
-structure GameTile where
-  /-- The title of the game -/
-  title: String
-  /-- One catch phrase about the game -/
-  short: String := default
-  /-- One paragraph description what the game is about -/
-  long: String := default
-  /-- List of languages the game supports
-
-  TODO: What's the expectected format
-  TODO: Must be a list with a single language currently
-   -/
-  languages: List String := default
-  /-- A list of games which this one builds upon -/
-  prerequisites: List String := default
-  /-- Number of worlds in the game -/
-  worlds: Nat := default
-  /-- Number of levels in the game -/
-  levels: Nat := default
-  /-- A cover image of the game
-
-  TODO: What's the format? -/
-  image: String := default
-deriving Inhabited, ToJson
-
 structure Game where
   /-- Internal name of the game. -/
   name : Name
@@ -396,19 +296,8 @@ structure Game where
   /-- TODO: currently unused. -/
   authors : List String := default
   worlds : Graph Name World := default
-  /-- The tile displayed on the server's landing page. -/
-  tile : GameTile := default
-  /-- The path to the background image of the world. -/
-  image : String := default
 deriving Inhabited, ToJson
 
-def getGameJson (game : «Game») : Json := Id.run do
-  let gameJson : Json := toJson game
-  -- Add world sizes to Json object
-  let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
-  let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
-  return gameJson
-
 /-! ## Game environment extension -/
 
 def HashMap.merge [BEq α] [Hashable α] (old : HashMap α β) (new : HashMap α β) (merge : β → β → β) :

server/GameServer/FileWorker.lean

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

server/GameServer/Game.lean

@@ -25,6 +25,53 @@ open Lsp
 open JsonRpc
 open IO
 
+def getGame (game : Name): GameServerM Json := do
+  let some game ← getGame? game
+    | throwServerError "Game not found"
+  let gameJson : Json := toJson game
+  -- Add world sizes to Json object
+  let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
+  let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
+  return gameJson
+
+/--
+Fields:
+- description: Lemma in mathematical language.
+- descriptionGoal: Lemma printed as Lean-Code.
+-/
+structure LevelInfo where
+  index : Nat
+  title : String
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
+  introduction : String
+  conclusion : String
+  descrText : Option String := none
+  descrFormat : String := ""
+  lemmaTab : Option String
+  displayName : Option String
+  statementName : Option String
+  template : Option String
+deriving ToJson, FromJson
+
+structure InventoryOverview where
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
+  lemmaTab : Option String
+deriving ToJson, FromJson
+
+structure LoadLevelParams where
+  world : Name
+  level : Nat
+  deriving ToJson, FromJson
+
+-- structure LoadTemplateParams where
+--   world : Name
+--   level : Nat
+--   deriving ToJson, FromJson
+
 structure DidOpenLevelParams where
   uri : String
   gameDir : String
@@ -44,6 +91,11 @@ structure DidOpenLevelParams where
   statementName : Name
   deriving ToJson, FromJson
 
+structure LoadDocParams where
+  name : Name
+  type : InventoryType
+deriving ToJson, FromJson
+
 structure SetInventoryParams where
   inventory : Array String
   difficulty : Nat
@@ -79,10 +131,86 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
     }
   }
 
+
 partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
   match ev with
   | ServerEvent.clientMsg msg =>
     match msg with
+    | Message.request id "info" _ =>
+      let s ← get
+      let c ← read
+      c.hOut.writeLspResponse ⟨id, (← getGame s.game)⟩
+      return true
+    | Message.request id "loadLevel" params =>
+      let p ← parseParams LoadLevelParams (toJson params)
+      let s ← get
+      let c ← read
+      let some lvl ← getLevel? {game := s.game, world := p.world, level := p.level}
+        | do
+          c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩
+          return true
+
+      let env ← getEnv
+
+      let levelInfo : LevelInfo :=
+          { index := lvl.index,
+            title := lvl.title,
+            tactics := lvl.tactics.tiles,
+            lemmas := lvl.lemmas.tiles,
+            definitions := lvl.definitions.tiles,
+            descrText := lvl.descrText,
+            descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
+            introduction := lvl.introduction
+            conclusion := lvl.conclusion
+            lemmaTab := match lvl.lemmaTab with
+            | some tab => tab
+            | none =>
+              -- Try to set the lemma tab to the category of the first added lemma
+              match lvl.lemmas.tiles.find? (·.new) with
+              | some tile => tile.category
+              | none => none
+            statementName := lvl.statementName.toString
+            displayName := match lvl.statementName with
+              | .anonymous => none
+              | name => match (inventoryExt.getState env).find?
+                  (fun x => x.name == name && x.type == .Lemma) with
+                | some n => n.displayName
+                | none => name.toString
+                -- Note: we could call `.find!` because we check in `Statement` that the
+                -- lemma doc must exist.
+            template := lvl.template
+            }
+      c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩
+      return true
+    -- | Message.request id "loadTemplate" params =>
+    --   let p ← parseParams LoadTemplateParams (toJson params)
+    --   let s ← get
+    --   let c ← read
+
+    --   let some game ← getGame? s.game
+    --     | throwServerError "Game not found"
+    --   let some world := game.worlds.nodes.find? p.world
+    --     | throwServerError "World not found"
+
+    --   let mut templates : Array <| Option String := #[]
+    --   for (_, level) in world.levels.toArray do
+    --     templates := templates.push level.template
+    --   c.hOut.writeLspResponse ⟨id, ToJson.toJson templates⟩
+    --   return true
+    | Message.request id "loadDoc" params =>
+      let p ← parseParams LoadDocParams (toJson params)
+      let c ← read
+      let some doc ← getInventoryItem? p.name p.type
+        | do
+            c.hOut.writeLspResponseError ⟨id, .invalidParams,
+              s!"Documentation not found: {p.name}", none⟩
+            return true
+      -- TODO: not necessary at all?
+      -- Here we only need to convert the fields that were not `String` in the `InventoryDocEntry`
+      -- let doc : InventoryItem := { doc with
+      --   name := doc.name.toString }
+      c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩
+      return true
     | Message.notification "$/game/setInventory" params =>
       let p := (← parseParams SetInventoryParams (toJson params))
       let s ← get
@@ -97,50 +225,26 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       let s ← get
       let some game ← getGame? s.game
         | return false
-
-      let mut overview : Array WorldOverview := #[]
-      for ⟨worldId, world⟩ in game.worlds.nodes.toList do
-        let mut tactics : Array InventoryTile := #[]
-        let mut theorems : Array InventoryTile := #[]
-        let mut definitions : Array InventoryTile := #[]
-        for ⟨_levelId, lvl⟩ in world.levels.toList do
-          tactics := tactics ++ lvl.tactics.tiles.filterMap (fun tile => match tile.new with
-            | true => some {tile with new := false, locked := true, disabled := false}
-            | false => none)
-          theorems := theorems ++ lvl.lemmas.tiles.filterMap (fun tile => match tile.new with
-            | true => some {tile with new := false, locked := true, disabled := false}
-            | false => none)
-          definitions := definitions ++ lvl.definitions.tiles.filterMap (fun tile => match tile.new with
-            | true => some {tile with new := false, locked := true, disabled := false}
-            | false => none)
-        overview := overview.push {
-          world := worldId,
-          tactics := tactics,
-          lemmas := theorems,
-          definitions := definitions }
-      let c ← read
-      c.hOut.writeLspResponse ⟨id, ToJson.toJson overview⟩
-      return true
-      -- -- All Levels have the same tiles, so we just load them from level 1 of an arbitrary world
-      -- -- and reset `new`, `disabled` and `unlocked`.
-      -- -- Note: as we allow worlds without any levels (for developing), we might need
-      -- -- to try until we find the first world with levels.
-      -- for ⟨worldId, _⟩ in game.worlds.nodes.toList do
-      --   let some lvl ← getLevel? {game := s.game, world := worldId, level := 1}
-      --     | do continue
-      --   let inventory : InventoryOverview := {
-      --     tactics := lvl.tactics.tiles.map
-      --       ({ · with locked := true, disabled := false, new := false }),
-      --     lemmas := lvl.lemmas.tiles.map
-      --       ({ · with locked := true, disabled := false, new := false }),
-      --     definitions := lvl.definitions.tiles.map
-      --       ({ · with locked := true, disabled := false, new := false }),
-      --     lemmaTab := none
-      --   }
-      --   let c ← read
-      --   c.hOut.writeLspResponse ⟨id, ToJson.toJson inventory⟩
-      --   return true
-      -- return false
+      -- All Levels have the same tiles, so we just load them from level 1 of an arbitrary world
+      -- and reset `new`, `disabled` and `unlocked`.
+      -- Note: as we allow worlds without any levels (for developing), we might need
+      -- to try until we find the first world with levels.
+      for ⟨worldId, _⟩ in game.worlds.nodes.toList do
+        let some lvl ← getLevel? {game := s.game, world := worldId, level := 1}
+          | do continue
+        let inventory : InventoryOverview := {
+          tactics := lvl.tactics.tiles.map
+            ({ · with locked := true, disabled := false, new := false }),
+          lemmas := lvl.lemmas.tiles.map
+            ({ · with locked := true, disabled := false, new := false }),
+          definitions := lvl.definitions.tiles.map
+            ({ · with locked := true, disabled := false, new := false }),
+          lemmaTab := none
+        }
+        let c ← read
+        c.hOut.writeLspResponse ⟨id, ToJson.toJson inventory⟩
+        return true
+      return false
     | _ => return false
   | _ => return false
 

server/GameServer/ImportModules.lean

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

server/GameServer/RpcHandlers.lean

@@ -78,7 +78,7 @@ partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) :
   | _, _ => none
 
 /-- Check if each fvar in `patterns` has a matching fvar in `fvars` -/
-def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM (Option FVarBijection) := do
+def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM Bool := do
   -- We iterate through the array backwards hoping that this will find us faster results
   -- TODO: implement backtracking
   let mut bij := initBij
@@ -97,11 +97,11 @@ def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (in
         -- usedFvars := usedFvars.set! (fvars.size - j - 1) true
         bij := bij'.insert pattern.fvarId! fvar.fvarId!
         break
-    if ! bij.forward.contains pattern.fvarId! then return none
+    if ! bij.forward.contains pattern.fvarId! then return false
 
-  if !strict || fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
-  then return some bij
-  else return none
+  if strict then
+    return fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
+  return true
 
 unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
   evalExpr (Array Expr → MessageData)
@@ -122,11 +122,10 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams :
         if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
         then
           let lctx := (← goal.getDecl).lctx
-          if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
+          if ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
           then
-            let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
-            let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
-            let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := lctx, opts := {}}
+            let text := (← evalHintMessage hint.text) hintFVars
+            let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
             let text ← (MessageData.withContext ctx text).toString
             return some { text := text, hidden := hint.hidden }
           else return none

server/GameServer/WasmServer.lean

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

server/Main.lean

@@ -1,5 +1,6 @@
 import GameServer.FileWorker
 import GameServer.Watchdog
+import GameServer.WasmServer
 import GameServer.Commands
 
 -- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`

server/bubblewrap.sh

@@ -2,15 +2,11 @@
 
 ELAN_HOME=$(lake env printenv ELAN_HOME)
 
-# $1 : the game directory
-# $2 : the lean4game folder
-# $3 : the gameserver executable
-
 (exec bwrap\
-  --bind $2 /lean4game \
-  --bind $1 /game \
-  --bind $ELAN_HOME /elan \
-  --bind /usr /usr \
+  --ro-bind ../../lean4game /lean4game \
+  --ro-bind ../../$1 /game \
+  --ro-bind $ELAN_HOME /elan \
+  --ro-bind /usr /usr \
   --dev /dev \
   --proc /proc \
   --symlink usr/lib /lib\
@@ -26,6 +22,6 @@ ELAN_HOME=$(lake env printenv ELAN_HOME)
   --unshare-uts  \
   --unshare-cgroup \
   --die-with-parent \
-  --chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \
+  --chdir "/lean4game/server/build/bin/" \
   ./gameserver --server /game
 )

server/import.mjs

@@ -11,7 +11,6 @@ const __filename = fileURLToPath(import.meta.url);
 const __dirname = path.dirname(__filename);
 
 const TOKEN = process.env.LEAN4GAME_GITHUB_TOKEN
-const USERNAME = process.env.LEAN4GAME_GITHUB_USER
 const octokit = new Octokit({
   auth: TOKEN
 })
@@ -42,10 +41,9 @@ async function download(id, url, dest) {
     requestProgress(request({
       url,
       headers: {
-        'accept': 'application/vnd.github+json',
-        'User-Agent': USERNAME,
+        'User-Agent': 'abentkamp',
         'X-GitHub-Api-Version': '2022-11-28',
-        'Authorization': 'Bearer ' + TOKEN
+        'Authorization': 'Bearer '+TOKEN
       }
     }))
     .on('progress', function (state) {
@@ -78,44 +76,35 @@ async function doImport (owner, repo, id) {
       .reduce((acc, cur) => acc.created_at < cur.created_at ? cur : acc)
     artifactId = artifact.id
     const url = artifact.archive_download_url
-    // Make sure the download folder exists
-    if (!fs.existsSync(path.join(__dirname, "..", "games"))){
-      fs.mkdirSync(path.join(__dirname, "..", "games"));
-    }
-    if (!fs.existsSync(path.join(__dirname, "..", "games", "tmp"))){
-      fs.mkdirSync(path.join(__dirname, "..", "games", "tmp"));
+    if (!fs.existsSync("tmp")){
+      fs.mkdirSync("tmp");
     }
     progress[id].output += `Download from ${url}\n`
-    await download(id, url, path.join(__dirname, "..", "games", "tmp", `${owner.toLowerCase()}_${repo.toLowerCase()}_${artifactId}.zip`))
+    await download(id, url, `tmp/artifact_${artifactId}.zip`)
     progress[id].output += `Download finished.\n`
-
-    await runProcess(id, "/bin/bash", [path.join(__dirname, "unpack.sh"), artifactId, owner.toLowerCase(), repo.toLowerCase()], path.join(__dirname, ".."))
-
-
-    // let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
-    // manifest = JSON.parse(manifest);
-    // if (manifest.length !== 1) {
-    //   throw `Unexpected manifest: ${JSON.stringify(manifest)}`
-    // }
-    // manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`]
-    // fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest));
-    // await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`)
-    // // await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`])
-
+    await runProcess(id, "/bin/bash", [`${__dirname}/unpack.sh`, artifactId],".")
+    let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
+    manifest = JSON.parse(manifest);
+    if (manifest.length !== 1) {
+      throw `Unexpected manifest: ${JSON.stringify(manifest)}`
+    }
+    manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`]
+    fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest));
+    await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`)
+    await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`])
     progress[id].done = true
-    progress[id].output += `Done!\n`
-    progress[id].output += `Play the game at: {your website}/#/g/${owner}/${repo}\n`
+    progress[id].output += `Done.\n`
   } catch (e) {
     progress[id].output += `Error: ${e.toString()}\n${e.stack}`
   } finally {
-    // clean-up temp. files
     if (artifactId) {
-      fs.rmSync(path.join(__dirname, "..", "games", "tmp", `${owner}_${repo}_${artifactId}.zip`), {force: true, recursive: false});
-      fs.rmSync(path.join(__dirname, "..", "games", "tmp", `${owner}_${repo}_${artifactId}`), {force: true, recursive: true});
+      fs.rmSync(`tmp/artifact_${artifactId}.zip`, {force: true, recursive: true});
+      fs.rmSync(`tmp/artifact_${artifactId}`, {force: true, recursive: true});
+      fs.rmSync(`tmp/artifact_${artifactId}_inner`, {force: true, recursive: true});
+      fs.rmSync(`tmp/archive_${artifactId}.tar`, {force: true, recursive: true});
     }
     progress[id].done = true
   }
-  await new Promise(resolve => setTimeout(resolve, 10000))
 }
 
 export const importTrigger = (req, res) => {

server/index.mjs

@@ -6,20 +6,25 @@ import * as url from 'url';
 import * as rpc from 'vscode-ws-jsonrpc';
 import * as jsonrpcserver from 'vscode-ws-jsonrpc/server';
 import os from 'os';
-import fs from 'fs';
 import anonymize from 'ip-anonymize';
-import { importTrigger, importStatus } from './import.mjs'
+// import { importTrigger, importStatus } from './import.mjs'
 // import fs from 'fs'
 
 /**
- * Add a game here if the server should keep a queue of pre-loaded games ready at all times.
- *
- * IMPORTANT! Tags here need to be lower case!
 */
-const queueLength = {
-  "g/hhu-adam/robo": 2,
-  "g/hhu-adam/nng4": 5,
-  "g/djvelleman/stg4": 2,
+const games = {
+    "g/hhu-adam/robo": {
+        dir: "Robo",
+        queueLength: 5
+    },
+    "g/hhu-adam/nng4": {
+        dir: "NNG4",
+        queueLength: 5
+    },
+    "g/hhu-adam/nng4-old": {
+        dir: "NNG4-OLD",
+        queueLength: 0
+    }
 }
 
 const __filename = url.fileURLToPath(import.meta.url);
@@ -31,18 +36,11 @@ const PORT = process.env.PORT || 8080;
 
 var router = express.Router();
 
-router.get('/import/status/:owner/:repo', importStatus)
-router.get('/import/trigger/:owner/:repo', importTrigger)
+// router.get('/import/status/:owner/:repo', importStatus)
+// router.get('/import/trigger/:owner/:repo', importTrigger)
 
 const server = app
-  .use(express.static(path.join(__dirname, '..', 'client', 'dist'))) // TODO: add a dist folder from inside the game
-  .use('/data/g/:owner/:repo/*', (req, res, next) => {
-    const owner = req.params.owner;
-    const repo = req.params.repo
-    const filename = req.params[0];
-    req.url = filename;
-    express.static(path.join(getGameDir(owner,repo),".lake","gamedata"))(req, res, next);
-  })
+  .use(express.static(path.join(__dirname, '../client/dist/')))
   .use('/', router)
   .listen(PORT, () => console.log(`Listening on ${PORT}`));
 
@@ -56,61 +54,41 @@ const isDevelopment = environment === 'development'
 /** We keep queues of started Lean Server processes to be ready when a user arrives */
 const queue = {}
 
-function getTag(owner, repo) {
+function tag(owner, repo) {
   return `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
 }
 
-function getGameDir(owner, repo) {
-  owner = owner.toLowerCase()
+function startServerProcess(owner, repo) {
+  let game_dir = (owner == 'local') ?
+    repo : games[tag(owner, repo)]?.dir
+
   if (owner == 'local') {
     if(!isDevelopment) {
       console.error(`No local games in production mode.`)
-      return ""
-    }
-  } else {
-    if(!fs.existsSync(path.join(__dirname, '..', 'games'))) {
-      console.error(`Did not find the following folder: ${path.join(__dirname, '..', 'games')}`)
-      console.error('Did you already import any games?')
-      return ""
+      return
     }
+    // TODO: This test does not work
+    // if (!fs.existsSync(path.join("../", game_dir))) {
+    //   console.error(`Game folder does not exists: ${game_dir}`)
+    //   return
+    // }
   }
 
-  let game_dir = (owner == 'local') ?
-    path.join(__dirname, '..', '..', repo) : // note: here we need `repo` to be case sensitive
-    path.join(__dirname, '..', 'games', `${owner}`, `${repo.toLowerCase()}`)
-
-  if(!fs.existsSync(game_dir)) {
-    console.error(`Game '${game_dir}' does not exist!`)
-    return ""
+  if (!game_dir) {
+    console.error(`Unknown game: ${tag(owner, repo)}`)
+    return
   }
 
-  return game_dir;
-}
-
-function startServerProcess(owner, repo) {
-
-  let game_dir = getGameDir(owner, repo)
-  if (!game_dir) return;
-
   let serverProcess
   if (isDevelopment) {
-    let args = ["--server", game_dir]
-    let binDir = path.join(game_dir, ".lake", "packages", "GameServer", "server", ".lake", "build", "bin")
-    // Note: `cwd` is important to be the `bin` directory as `Watchdog` calls `./gameserver` again
-    if (fs.existsSync(binDir)) {
-      // Try to use the game's own copy of `gameserver`.
-      serverProcess = cp.spawn("./gameserver", args, { cwd: binDir })
-    } else {
-      // If the game is built with `-Klean4game.local` there is no copy in the lake packages.
-      serverProcess = cp.spawn("./gameserver", args,
-        { cwd: path.join(__dirname, "..", "server", ".lake", "build", "bin") })
-    }
+    let args = ["--server", path.join("../../../../", game_dir)]
+    serverProcess = cp.spawn("./gameserver", args,
+        { cwd: path.join(__dirname, "./build/bin/") })
   } else {
     serverProcess =  cp.spawn("./bubblewrap.sh",
-      [ game_dir, path.join(__dirname, '..')],
+      [game_dir],
       { cwd: __dirname })
   }
-
   serverProcess.on('error', error =>
     console.error(`Launching Lean Server failed: ${error}`)
   )
@@ -123,21 +101,15 @@ function startServerProcess(owner, repo) {
 }
 
 /** start Lean Server processes to refill the queue */
-function fillQueue(tag) {
-  while (queue[tag].length < queueLength[tag]) {
-    let serverProcess
-    serverProcess = startServerProcess(tag)
-    if (serverProcess == null) {
-      console.error('serverProcess was undefined/null')
-      return
+function fillQueue(owner, repo) {
+    while (queue[tag(owner, repo)].length < games[tag(owner, repo)].queueLength) {
+      const serverProcess = startServerProcess(tag(owner, repo))
+      queue[tag(owner, repo)].push(serverProcess)
     }
-    queue[tag].push(serverProcess)
-  }
 }
 
-// // TODO: We disabled queue for now
 // if (!isDevelopment) { // Don't use queue in development
-//   for (let tag in queueLength) {
+//   for (let tag in games) {
 //     queue[tag] = []
 //     fillQueue(tag)
 //   }
@@ -150,21 +122,19 @@ wss.addListener("connection", function(ws, req) {
     if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; }
     const owner = reRes[1]
     const repo = reRes[2]
+    // const tag = `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
 
-    const tag = getTag(owner, repo)
+    // // TODO
+    // if (isDevelopment && process.env.DEV_CONTAINER) {
+    //     tag = `g/local/game`
+    // }
 
-    let ps
-    if (!queue[tag] || queue[tag].length == 0) {
-      ps = startServerProcess(owner, repo)
+    let ps;
+    if (!queue[tag(owner, repo)] || queue[tag(owner, repo)].length == 0) {
+        ps = startServerProcess(owner, repo)
     } else {
-        console.info('Got process from the queue')
-        ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately
-        fillQueue(tag)
-    }
-
-    if (ps == null) {
-      console.error('server process is undefined/null')
-      return
+        ps = queue[tag(owner, repo)].shift() // Pick the first Lean process; it's likely to be ready immediately
+        fillQueue(owner, repo)
     }
 
     socketCounter += 1;
@@ -177,14 +147,14 @@ wss.addListener("connection", function(ws, req) {
         onClose: (cb) => { ws.on("close", cb) },
         send: (data, cb) => { ws.send(data,cb) }
     }
-    const reader = new rpc.WebSocketMessageReader(socket)
-    const writer = new rpc.WebSocketMessageWriter(socket)
+    const reader = new rpc.WebSocketMessageReader(socket);
+    const writer = new rpc.WebSocketMessageWriter(socket);
     const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
-    const serverConnection = jsonrpcserver.createProcessStreamConnection(ps)
+    const serverConnection = jsonrpcserver.createProcessStreamConnection(ps);
     socketConnection.forward(serverConnection, message => {
         if (isDevelopment) {console.log(`CLIENT: ${JSON.stringify(message)}`)}
         return message;
-    })
+    });
     serverConnection.forward(socketConnection, message => {
       if (isDevelopment) {console.log(`SERVER: ${JSON.stringify(message)}`)}
         return message;
@@ -195,9 +165,9 @@ wss.addListener("connection", function(ws, req) {
 
     ws.on('close', () => {
       console.log(`[${new Date()}] Socket closed - ${ip}`)
-      socketCounter -= 1
+      socketCounter -= 1;
     })
 
-    socketConnection.onClose(() => serverConnection.dispose())
-    serverConnection.onClose(() => socketConnection.dispose())
+    socketConnection.onClose(() => serverConnection.dispose());
+    serverConnection.onClose(() => socketConnection.dispose());
 })

server/lake-manifest.json

@@ -1,14 +1,4 @@
-{"version": 7,
- "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/leanprover/std4.git",
-   "type": "git",
-   "subDir": null,
-   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
-   "name": "std",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
- "name": "GameServer",
- "lakeDir": ".lake"}
+{"version": 6,
+ "packagesDir": "lake-packages",
+ "packages": [],
+ "name": "GameServer"}

server/lakefile.lean

@@ -3,11 +3,7 @@ open Lake DSL
 
 package GameServer
 
--- Using this assumes that each dependency has a tag of the form `v4.X.0`.
-def leanVersion : String := s!"v{Lean.versionString}"
-
-require std from git "https://github.com/leanprover/std4.git" @ leanVersion
-
+@[default_target]
 lean_lib GameServer
 
 @[default_target]
@@ -15,13 +11,3 @@ lean_exe gameserver {
   root := `Main
   supportInterpreter := true
 }
-
-/--
-When a package depending on GameServer updates its dependencies,
-build the `gameserver` executable.
--/
-post_update pkg do
-  let rootPkg ← getRootPackage
-  if rootPkg.name = pkg.name then
-    return -- do not run in GameServer itself
-  discard <| runBuild gameserver.build >>= (·.await)

server/lakefile32.lean

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

server/lean-toolchain

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

server/main.c

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

server/unpack.sh

@@ -0,0 +1,13 @@
+#/bin/bash
+
+ARTIFACT_ID=$1
+
+echo "Unpacking ZIP."
+unzip -o tmp/artifact_${ARTIFACT_ID}.zip -d tmp/artifact_${ARTIFACT_ID}
+echo "Unpacking TAR."
+for f in tmp/artifact_${ARTIFACT_ID}/* #Should only be one file
+do
+  echo "Unpacking $f"
+  mkdir tmp/artifact_${ARTIFACT_ID}_inner
+  tar -xvf $f -C tmp/artifact_${ARTIFACT_ID}_inner
+done

tsconfig.json

@@ -12,5 +12,5 @@
     "experimentalDecorators": true,
     "allowSyntheticDefaultImports": true,
   },
-  "exclude": ["server", "relay"]
+  "exclude": ["server"]
 }

vite.config.ts

@@ -5,12 +5,6 @@ import svgr from "vite-plugin-svgr"
 
 // https://vitejs.dev/config/
 export default defineConfig({
-  //root: 'client/src',
-  build: {
-    // Relative to the root
-    // Note: This has to match the path in `relay/index.mjs`
-    outDir: 'client/dist',
-  },
   plugins: [
     react(),
     svgr({
@@ -23,14 +17,15 @@ export default defineConfig({
         {
           src: 'node_modules/@leanprover/infoview/dist/*.production.min.js',
           dest: '.'
+        },
+        {
+          src: 'node_modules/coi-serviceworker/coi-serviceworker.js',
+          dest: '.'
         }
       ]
     })
   ],
   publicDir: "client/public",
-  optimizeDeps: {
-    exclude: ['games']
-  },
   server: {
     port: 3000,
     proxy: {
@@ -38,12 +33,6 @@ export default defineConfig({
         target: 'ws://localhost:8080',
         ws: true
       },
-      '/import': {
-        target: 'http://localhost:8080',
-      },
-      '/data': {
-        target: 'http://localhost:8080',
-      },
     }
   },
   resolve: {

wasm.sh

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

webpack.config.js

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