Update update_game.md

Merge branch 'dev'
update doc, including #148
2023-11-30 19:32:38 +01:00 · 2023-11-30 19:29:18 +01:00 · 2023-11-30 19:26:42 +01:00 · 2023-11-30 17:39:29 +01:00 · 2023-11-30 12:16:06 +01:00 · 2023-11-30 11:18:56 +01:00
36 changed files with 1037 additions and 506 deletions
@@ -1 +0,0 @@
-LEAN4GAME_SINGLE_GAME=false
@@ -5,7 +5,17 @@ jobs:
  build:
    runs-on: ubuntu-latest
    steps:
-      - uses: actions/checkout@v3
+      - 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/setup-node@v3
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
      - run: npm install
      - run: npm run build
@@ -1,6 +1,6 @@
 node_modules
+games/
 client/dist
-server/build
-server/lakefile.olean
-**/lake-packages/
+games/
+server/.lake
 **/.DS_Store
@@ -8,6 +8,7 @@ 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

@@ -10,6 +10,7 @@ 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);

@@ -19,6 +20,10 @@ 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}>
@@ -347,6 +347,7 @@ 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)
@@ -455,6 +456,17 @@ 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">
@@ -521,7 +533,7 @@ export function TypewriterInterface({props}) {
                }
              </div>
            }
-          </> : <CircularProgress />
+          </> : <CircularProgress variant="determinate" value={loadingProgress} />
        }
      </div>
    </div>
@@ -8,6 +8,7 @@ import '@fontsource/roboto/700.css';

 import '../css/landing_page.css'
 import coverRobo from '../assets/covers/formaloversum.png'
+import coverNNG from '../assets/covers/nng.png'
 import bgImage from '../assets/bg.jpg'

 import Markdown from './markdown';
@@ -113,7 +114,18 @@ function LandingPage() {
 learning the basics about theorem proving in Lean.

 This is a good first introduction to Lean!"
-        worlds="4"
+        worlds="8"
+        levels="67"
+        image={coverNNG}
+        language="English"
+        />
+
+      <GameTile
+        title="Set Theory Game"
+        gameId="g/djvelleman/STG4"
+        intro="A game about set theory"
+        description=""
+        worlds="5"
        levels="30"
        language="English"
        />
@@ -48,7 +48,6 @@ function Level() {
  const params = useParams()
  const levelId = parseInt(params.levelId)
  const worldId = params.worldId
-  // useLoadWorldFiles(worldId)

  const [impressum, setImpressum] = React.useState(false)

@@ -615,6 +614,7 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange

      return () => {
        editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
+        model.dispose();
      }
    }
  }, [editor, levelId, connection, leanClientStarted])
@@ -637,27 +637,3 @@ 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])
-}
@@ -48,6 +48,7 @@ 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;
@@ -15,15 +15,6 @@ 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
@@ -43,6 +34,11 @@ 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 />,
@@ -2,7 +2,6 @@
 * @fileOverview Define API of the server-client communication
 */
 import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react'
-import { Connection } from '../connection'

 export interface GameInfo {
  title: null|string,
@@ -57,40 +56,22 @@ interface Doc {
  category: string,
 }

-
-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: customBaseQuery,
+  baseQuery: fetchBaseQuery({ baseUrl: window.location.origin + "/api" }),
  endpoints: (builder) => ({
    getGameInfo: builder.query<GameInfo, {game: string}>({
-      query: ({game}) => {return {game, method: 'info', params: {}}},
+      query: ({game}) => `${game}/game`,
    }),
    loadLevel: builder.query<LevelInfo, {game: string, world: string, level: number}>({
-      query: ({game, world, level}) => {return {game, method: "loadLevel", params: {world, level}}},
+      query: ({game, world, level}) => `${game}/level/${world}/${level}`,
    }),
    loadInventoryOverview: builder.query<InventoryOverview, {game: string}>({
-      query: ({game}) => {return {game, method: "loadInventoryOverview", params: {}}},
+      query: ({game}) => `${game}/inventory`,
    }),
    loadDoc: builder.query<Doc, {game: string, name: string, type: "lemma"|"tactic"}>({
-      query: ({game, name, type}) => {return {game, method: "loadDoc", params: {name, type}}},
+      query: ({game, type, name}) => `${game}/doc/${type}/${name}`,
    }),
  }),
 })
@@ -245,7 +245,11 @@ That way, the game will replace it with the actual name the assumption has in th

 ## 7. Update your game

-In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](https://github.com/leanprover-community/lean4game/blob/main/doc/update_game.md).
+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)

 ## Further Notes

@@ -0,0 +1,30 @@
+# 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!
@@ -85,7 +85,7 @@ git clone https://github.com/hhu-adam/GameSkeleton.git
 Download dependencies and build the game:
 ```bash
 cd GameSkeleton
-lake update
+lake update -R
 lake exe cache get   # if your game depends on mathlib
 lake build
 ```
@@ -113,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 setting `export LEAN4GAME=local` inside your local game before building it:
+When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by using `lake update -R -Klean4game.local`:

 ```bash
 cd NNG4
-export LEAN4GAME=local
-lake update
+lake update -R -Klean4game.local
 lake build
 ```
-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`.
+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.
@@ -0,0 +1,28 @@
+
+# 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.
@@ -10,28 +10,44 @@ 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: run `lake update` (followed by `lake exe cache get` if you depend on mathlib.)
+* Local Setup: run
+  ```
+  lake update -R
+  lake build
+  ```
+  in your game folder.
+
+  * Additionally, if you have a local copy of the server `lean4game`,
+    you should update this one to the matching version, too:
+    ```
+    git fetch
+    git checkout {VERSION_TAG}
+    npm install
+    ```
+    where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
 * Gitpod/Codespaces: Create a fresh one

-This will update `lean4game` and `mathlib` in your project to the new lean version.
+This will your game (and the mathlib version you might be using) to the new lean version.

 ## Newest developing setup

 There are a few files in your game repository which are used for the developing setup
-(dev container/codespaces/gitpod). If you need to update your're developing setup, for example because it doesn't work
+(dev container/codespaces/gitpod). If you need to update your 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.
+simply copy them from the `GameSkeleton` into your game and proceed as above,
+i.e. `lake update -R && lake build`.

 (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.)
+where you need to add any dependencies of your game, or remove mathlib if you don't need it.)
@@ -4,8 +4,10 @@ module.exports = {
    name   : "lean4game",
    script : "server/index.mjs",
    env: {
-       NODE_ENV: "production",
-       PORT: 8002
+      LEAN4GAME_GITHUB_USER: "",
+      LEAN4GAME_GITHUB_TOKEN: "",
+      NODE_ENV: "production",
+      PORT: 8002
    },
  }]
 }
@@ -40,6 +40,7 @@
        "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",
@@ -56,7 +57,7 @@
        "concurrently": "^7.6.0",
        "css-loader": "^6.7.3",
        "file-loader": "^6.2.0",
-        "nodemon": "^2.0.20",
+        "nodemon": "^3.0.1",
        "react-refresh": "^0.14.0",
        "style-loader": "^3.3.1",
        "ts-loader": "^9.4.2",
@@ -6014,7 +6015,6 @@
      "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,6 +6183,22 @@
      "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",
@@ -6212,6 +6228,11 @@
      "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",
@@ -6224,12 +6245,40 @@
        "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": "0.24.0",
-      "resolved": "https://registry.npmjs.org/axios/-/axios-0.24.0.tgz",
-      "integrity": "sha512-Q6cWsys88HoPgAaFAVUb0WpPk0O8iTeisR9IMqy9G8AbO4NlpVknrnQS03zzF9PGAWgO3cgletO3VjV/P7VztA==",
+      "version": "1.6.2",
+      "resolved": "https://registry.npmjs.org/axios/-/axios-1.6.2.tgz",
+      "integrity": "sha512-7i24Ri4pmDRfJTR7LDBhsOTtcm+9kjX5WiY1X3wIisx6G9So3pfMkEiU7emUBe46oceVImccTEM3k6C5dbVW8A==",
      "dependencies": {
-        "follow-redirects": "^1.14.4"
+        "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"
      }
    },
    "node_modules/babel-core": {
@@ -6381,6 +6430,14 @@
      "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",
@@ -6671,6 +6728,11 @@
        }
      ]
    },
+    "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",
@@ -6908,6 +6970,17 @@
      "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",
@@ -7424,6 +7497,17 @@
        "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",
@@ -7590,6 +7674,14 @@
        "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",
@@ -7748,6 +7840,15 @@
        "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",
@@ -8136,11 +8237,18 @@
      "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==",
-      "dev": true
+      "integrity": "sha512-f3qQ9oQy9j2AhBe/H9VC91wLmKBCCU/gDOnKNAYG5hswO7BLKj09Hc5HYNz9cGI++xlpDCIgDaitVs03ATR84Q=="
    },
    "node_modules/fast-glob": {
      "version": "3.3.1",
@@ -8160,8 +8268,7 @@
    "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==",
-      "dev": true
+      "integrity": "sha512-lhd/wF+Lk98HZoTCtlVraHtfh5XYijIjalXck7saUtuanSDyLMxnHhSXEDJqHxD7msR8D0uCmqlkwjCV8xvwHw=="
    },
    "node_modules/fast-plist": {
      "version": "0.1.3",
@@ -8346,6 +8453,27 @@
        "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",
@@ -8475,6 +8603,14 @@
        "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",
@@ -8545,6 +8681,27 @@
      "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",
@@ -8975,6 +9132,20 @@
        "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",
@@ -9482,6 +9653,11 @@
        "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",
@@ -9542,6 +9718,11 @@
        "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",
@@ -9950,6 +10131,11 @@
        "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",
@@ -10077,11 +10263,20 @@
      "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==",
-      "dev": true
+      "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=="
    },
    "node_modules/json5": {
      "version": "2.2.3",
@@ -10153,6 +10348,20 @@
      "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",
@@ -10229,22 +10438,22 @@
      }
    },
    "node_modules/lean4": {
-      "version": "0.0.99",
-      "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?79d345c739bf707024eef5057ccef81b404a2ddf",
-      "integrity": "sha512-jgl4gGQXvP+RhdAr9r0+K6I5SpPkad++zAql9BawHI7OE7vMwK+7GbYXoa5aAP8T1BSIZQ+y3w0cl8FCk5C++A==",
+      "version": "0.0.119",
+      "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985",
+      "integrity": "sha512-hA7bb0EFlNwtk7+/7gO5OZS7HtrhmoRacE/b2etFBYG4FbkZd/NKTcs5PHGcKsYXeVghkOOZjw0uhNWaeW3gvw==",
      "license": "Apache-2.0",
      "dependencies": {
-        "@leanprover/infoview": "~0.3.0",
-        "@leanprover/infoview-api": "~0.2.0",
-        "axios": "~0.24.0",
+        "@leanprover/infoview": "~0.4.3",
+        "@leanprover/infoview-api": "~0.2.1",
+        "axios": "^1.6.2",
        "cheerio": "^1.0.0-rc.10",
-        "es-module-shims": "^1.6.2",
        "mobx": "5.15.7",
-        "semver": "=7.3.5",
-        "vscode-languageclient": "=8.0.2"
+        "semver": "^7.5.4",
+        "vscode-languageclient": "=8.0.2",
+        "zod": "^3.22.4"
      },
      "engines": {
-        "vscode": "^1.70.0"
+        "vscode": "^1.75.0"
      }
    },
    "node_modules/lean4-infoview": {
@@ -10263,19 +10472,6 @@
        "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",
@@ -10297,9 +10493,9 @@
      }
    },
    "node_modules/lean4/node_modules/semver": {
-      "version": "7.3.5",
-      "resolved": "https://registry.npmjs.org/semver/-/semver-7.3.5.tgz",
-      "integrity": "sha512-PoeGJYh8HK4BTO/a9Tf6ZG3veo/A7ZVsYrSA6J8ny9nb3B1VrpkuN+z9OE5wfE5p6H4LchYZsegiQgbJD94ZFQ==",
+      "version": "7.5.4",
+      "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.4.tgz",
+      "integrity": "sha512-1bCSESV6Pv+i21Hvpxp3Dx+pSD8lIPt8uVjRrxAUt/nbswYc+tK6Y2btiULjd4+fnq15PX+nqQDC7Oft7WkwcA==",
      "dependencies": {
        "lru-cache": "^6.0.0"
      },
@@ -10317,7 +10513,7 @@
    },
    "node_modules/lean4web": {
      "version": "0.1.0",
-      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#b02044f3a3b9130b663c3619ce56c603fa3a4cf4",
+      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#6fc9c11179934cce7ca1f78140c57b6931186b42",
      "dependencies": {
        "@emotion/react": "^11.11.1",
        "@emotion/styled": "^11.11.0",
@@ -10326,12 +10522,13 @@
        "@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.1",
+        "@leanprover/infoview": "^0.4.3",
        "@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?79d345c739bf707024eef5057ccef81b404a2ddf",
+        "lean4": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985",
        "mobx": "^6.6.2",
        "moment-timezone": "^0.5.39",
        "monaco-editor": "^0.34.1",
@@ -10346,6 +10543,7 @@
        "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"
      }
@@ -12611,9 +12809,9 @@
      }
    },
    "node_modules/nodemon": {
-      "version": "2.0.22",
-      "resolved": "https://registry.npmjs.org/nodemon/-/nodemon-2.0.22.tgz",
-      "integrity": "sha512-B8YqaKMmyuCO7BowF1Z1/mkPqLk6cs/l63Ojtd6otKjMx47Dq1utxfRxcavH1I7VSaL8n5BUaoutadnsX3AAVQ==",
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/nodemon/-/nodemon-3.0.1.tgz",
+      "integrity": "sha512-g9AZ7HmkhQkqXkRc20w+ZfQ73cHLbE8hnPbtaFbFtCumZsjyMhKk9LajQ07U5Ux28lvFjZ5X7HvWR1xzU8jHVw==",
      "dev": true,
      "dependencies": {
        "chokidar": "^3.5.2",
@@ -12621,8 +12819,8 @@
        "ignore-by-default": "^1.0.1",
        "minimatch": "^3.1.2",
        "pstree.remy": "^1.1.8",
-        "semver": "^5.7.1",
-        "simple-update-notifier": "^1.0.7",
+        "semver": "^7.5.3",
+        "simple-update-notifier": "^2.0.0",
        "supports-color": "^5.5.0",
        "touch": "^3.1.0",
        "undefsafe": "^2.0.5"
@@ -12631,7 +12829,7 @@
        "nodemon": "bin/nodemon.js"
      },
      "engines": {
-        "node": ">=8.10.0"
+        "node": ">=10"
      },
      "funding": {
        "type": "opencollective",
@@ -12647,15 +12845,39 @@
        "ms": "^2.1.1"
      }
    },
-    "node_modules/nodemon/node_modules/semver": {
-      "version": "5.7.2",
-      "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.2.tgz",
-      "integrity": "sha512-cBznnQ9KjJqU67B52RMC65CMarK2600WFnbkcaiwWq3xy/5haFJlshgnpjovMVJ+Hff49d8GEn0b87C5pDQ10g==",
+    "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,
-      "bin": {
-        "semver": "bin/semver"
+      "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==",
+      "dev": true,
+      "dependencies": {
+        "lru-cache": "^6.0.0"
+      },
+      "bin": {
+        "semver": "bin/semver.js"
+      },
+      "engines": {
+        "node": ">=10"
+      }
+    },
+    "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",
@@ -12706,6 +12928,14 @@
      "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",
@@ -13114,6 +13344,11 @@
        "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",
@@ -13344,6 +13579,16 @@
        "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",
@@ -13354,7 +13599,6 @@
      "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"
      }
@@ -14066,6 +14310,37 @@
        "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",
@@ -14074,6 +14349,23 @@
        "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",
@@ -14577,26 +14869,50 @@
      "integrity": "sha512-wnD2ZE+l+SPC/uoS0vXeE9L1+0wuaMqKlfz9AMUo38JsyLSBWSFcHR1Rri62LZc12vLr1gb3jl7iwQhgwpAbGQ=="
    },
    "node_modules/simple-update-notifier": {
-      "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==",
+      "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==",
      "dev": true,
      "dependencies": {
-        "semver": "~7.0.0"
+        "semver": "^7.5.3"
      },
      "engines": {
-        "node": ">=8.10.0"
+        "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_modules/simple-update-notifier/node_modules/semver": {
-      "version": "7.0.0",
-      "resolved": "https://registry.npmjs.org/semver/-/semver-7.0.0.tgz",
-      "integrity": "sha512-+GB6zVA9LWh6zovYQLALHwv5rb2PHGlJi3lfiqIHxR0uuwCgefcOJc59v9fv1w8GbStwxuuqqAjI9NMAOOgq1A==",
+      "version": "7.5.4",
+      "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.4.tgz",
+      "integrity": "sha512-1bCSESV6Pv+i21Hvpxp3Dx+pSD8lIPt8uVjRrxAUt/nbswYc+tK6Y2btiULjd4+fnq15PX+nqQDC7Oft7WkwcA==",
      "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",
@@ -14729,6 +15045,30 @@
      "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",
@@ -15132,6 +15472,18 @@
        "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",
@@ -15301,6 +15653,22 @@
      "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",
@@ -15598,7 +15966,6 @@
      "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"
      }
@@ -15695,6 +16062,24 @@
        "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",
@@ -16640,6 +17025,14 @@
        "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",
@@ -1,6 +1,7 @@
 {
  "name": "lean4-game",
  "version": "0.1.0",
+  "type": "module",
  "private": true,
  "homepage": ".",
  "dependencies": {
@@ -36,6 +37,7 @@
    "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",
@@ -52,7 +54,7 @@
    "concurrently": "^7.6.0",
    "css-loader": "^6.7.3",
    "file-loader": "^6.2.0",
-    "nodemon": "^2.0.20",
+    "nodemon": "^3.0.1",
    "react-refresh": "^0.14.0",
    "style-loader": "^3.3.1",
    "ts-loader": "^9.4.2",
@@ -64,6 +66,7 @@
    "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 server/index.mjs"
@@ -1,3 +1,3 @@
-build
-adam
-nng
+build/
+games/
+.lake
@@ -644,6 +644,44 @@ elab "Template" tacs:tacticSeq : tactic => 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
+
+  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
@@ -923,6 +961,7 @@ elab "MakeGame" : command => do
  -- 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

@@ -1052,6 +1091,9 @@ 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 -/

@@ -108,6 +108,12 @@ 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 :
@@ -135,7 +141,12 @@ 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 -/

@@ -256,6 +267,55 @@ structure GameLevel where
  template: Option String := none
  deriving 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
+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
+  }

 /-! ## World -/

@@ -298,6 +358,13 @@ structure Game where
  worlds : Graph Name World := 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 : β → β → β) :
@@ -1,6 +1,7 @@
 /- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/
 import Lean.Server.FileWorker
 import GameServer.Game
+import GameServer.ImportModules

 namespace MyModule
 open Lean
@@ -412,7 +413,7 @@ section Initialization
    -- Set the search path
    Lean.searchPathRef.set paths

-    let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
+    let env ← importModules' #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }]
    -- return (env, paths)

    -- use empty header
@@ -25,53 +25,6 @@ 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
@@ -91,11 +44,6 @@ 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
@@ -131,86 +79,10 @@ 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
@@ -221,30 +93,6 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
        fw.stdin.writeLspMessage msg

      return true
-    | Message.request id "loadInventoryOverview" _ =>
-      let s ← get
-      let some game ← getGame? s.game
-        | 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

@@ -0,0 +1,108 @@
+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
@@ -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 Bool := do
+def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM (Option FVarBijection) := 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 false
+    if ! bij.forward.contains pattern.fvarId! then return none

-  if strict then
-    return fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
-  return true
+  if !strict || fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
+  then return some bij
+  else return none

 unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
  evalExpr (Array Expr → MessageData)
@@ -122,9 +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 ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
+          if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
          then
-            let text := (← evalHintMessage hint.text) hintFVars
+            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 := ← getLCtx, opts := {}}
            let text ← (MessageData.withContext ctx text).toString
            return some { text := text, hidden := hint.hidden }
@@ -2,11 +2,13 @@

 ELAN_HOME=$(lake env printenv ELAN_HOME)

+
+
 (exec bwrap\
-  --ro-bind ../../lean4game /lean4game \
-  --ro-bind ../../$1 /game \
-  --ro-bind $ELAN_HOME /elan \
-  --ro-bind /usr /usr \
+  --bind $2 /lean4game \
+  --bind $1 /game \
+  --bind $ELAN_HOME /elan \
+  --bind /usr /usr \
  --dev /dev \
  --proc /proc \
  --symlink usr/lib /lib\
@@ -22,6 +24,6 @@ ELAN_HOME=$(lake env printenv ELAN_HOME)
  --unshare-uts  \
  --unshare-cgroup \
  --die-with-parent \
-  --chdir "/lean4game/server/build/bin/" \
+  --chdir "/lean4game/server/.lake/build/bin/" \
  ./gameserver --server /game
 )
@@ -11,6 +11,7 @@ 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
 })
@@ -41,9 +42,10 @@ async function download(id, url, dest) {
    requestProgress(request({
      url,
      headers: {
-        'User-Agent': 'abentkamp',
+        'accept': 'application/vnd.github+json',
+        'User-Agent': USERNAME,
        'X-GitHub-Api-Version': '2022-11-28',
-        'Authorization': 'Bearer '+TOKEN
+        'Authorization': 'Bearer ' + TOKEN
      }
    }))
    .on('progress', function (state) {
@@ -76,35 +78,45 @@ 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
-    if (!fs.existsSync("tmp")){
-      fs.mkdirSync("tmp");
+    // Make sure the download folder exists
+    if (!fs.existsSync(`${__dirname}/../games`)){
+      fs.mkdirSync(`${__dirname}/../games`);
+    }
+    if (!fs.existsSync(`${__dirname}/../games/tmp`)){
+      fs.mkdirSync(`${__dirname}/../games/tmp`);
    }
    progress[id].output += `Download from ${url}\n`
-    await download(id, url, `tmp/artifact_${artifactId}.zip`)
+    await download(id, url, `${__dirname}/../games/tmp/${owner.toLowerCase()}_${repo.toLowerCase()}_${artifactId}.zip`)
    progress[id].output += `Download finished.\n`
-    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`])
+
+    await runProcess(id, "/bin/bash", [`${__dirname}/unpack.sh`, artifactId, owner.toLowerCase(), repo.toLowerCase()], `${__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`])
+
    progress[id].done = true
-    progress[id].output += `Done.\n`
+    progress[id].output += `Done!\n`
+    progress[id].output += `Play the game at: {your website}/#/g/${owner}/${repo}\n`
  } catch (e) {
    progress[id].output += `Error: ${e.toString()}\n${e.stack}`
  } finally {
-    if (artifactId) {
-      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});
-    }
+    // if (artifactId) {
+    //   // 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) => {
@@ -6,25 +6,20 @@ 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 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 queueLength = {
+  "g/hhu-adam/robo": 2,
+  "g/hhu-adam/nng4": 5,
+  "g/djvelleman/stg4": 2,
 }

 const __filename = url.fileURLToPath(import.meta.url);
@@ -36,8 +31,34 @@ 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)
+
+function loadJson(req, filename) {
+  const owner = req.params.owner;
+  const repo = req.params.repo
+  return JSON.parse(fs.readFileSync(path.join(getGameDir(owner,repo),".lake","gamedata",filename)))
+}
+
+router.get("/api/g/:owner/:repo/game", (req, res) => {
+  res.send(loadJson(req, `game.json`));
+});
+
+router.get("/api/g/:owner/:repo/inventory", (req, res) => {
+  res.send(loadJson(req, `inventory.json`));
+});
+
+router.get("/api/g/:owner/:repo/level/:world/:level", (req, res) => {
+  const world = req.params.world;
+  const level = req.params.level;
+  res.send(loadJson(req, `level__${world}__${level}.json`));
+});
+
+router.get("/api/g/:owner/:repo/doc/:type/:name", (req, res) => {
+  const type = req.params.type;
+  const name = req.params.name;
+  res.send(loadJson(req, `doc__${type}__${name}.json`));
+});

 const server = app
  .use(express.static(path.join(__dirname, '../client/dist/')))
@@ -54,39 +75,50 @@ const isDevelopment = environment === 'development'
 /** We keep queues of started Lean Server processes to be ready when a user arrives */
 const queue = {}

-function tag(owner, repo) {
+function getTag(owner, repo) {
  return `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
 }

-function startServerProcess(owner, repo) {
-  let game_dir = (owner == 'local') ?
-    repo : games[tag(owner, repo)]?.dir
-
+function getGameDir(owner, repo) {
+  owner = owner.toLowerCase()
  if (owner == 'local') {
    if(!isDevelopment) {
      console.error(`No local games in production mode.`)
      return
    }
-    // TODO: This test does not work
-    // if (!fs.existsSync(path.join("../", game_dir))) {
-    //   console.error(`Game folder does not exists: ${game_dir}`)
-    //   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
+    }
  }

-  if (!game_dir) {
-    console.error(`Unknown game: ${tag(owner, repo)}`)
+  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
  }

+  return game_dir;
+}
+
+function startServerProcess(owner, repo) {
+
+  let game_dir = getGameDir(owner, repo)
+  if (!game_dir) return;
+
  let serverProcess
  if (isDevelopment) {
-    let args = ["--server", path.join("../../../../", game_dir)]
+    let args = ["--server", game_dir]
    serverProcess = cp.spawn("./gameserver", args,
-        { cwd: path.join(__dirname, "./build/bin/") })
+        { cwd: path.join(__dirname, "./.lake/build/bin/") })
  } else {
    serverProcess =  cp.spawn("./bubblewrap.sh",
-      [game_dir],
+      [game_dir, path.join(__dirname, '..')],
      { cwd: __dirname })
  }
  serverProcess.on('error', error =>
@@ -101,15 +133,21 @@ function startServerProcess(owner, repo) {
 }

 /** start Lean Server processes to refill the queue */
-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)
+function fillQueue(tag) {
+  while (queue[tag].length < queueLength[tag]) {
+    let serverProcess
+    serverProcess = startServerProcess(tag)
+    if (serverProcess == null) {
+      console.error('serverProcess was undefined/null')
+      return
    }
+    queue[tag].push(serverProcess)
+  }
 }

+// // TODO: We disabled queue for now
 // if (!isDevelopment) { // Don't use queue in development
-//   for (let tag in games) {
+//   for (let tag in queueLength) {
 //     queue[tag] = []
 //     fillQueue(tag)
 //   }
@@ -122,19 +160,21 @@ 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()}`

-    // // TODO
-    // if (isDevelopment && process.env.DEV_CONTAINER) {
-    //     tag = `g/local/game`
-    // }
+    const tag = getTag(owner, repo)

-    let ps;
-    if (!queue[tag(owner, repo)] || queue[tag(owner, repo)].length == 0) {
-        ps = startServerProcess(owner, repo)
+    let ps
+    if (!queue[tag] || queue[tag].length == 0) {
+      ps = startServerProcess(owner, repo)
    } else {
-        ps = queue[tag(owner, repo)].shift() // Pick the first Lean process; it's likely to be ready immediately
-        fillQueue(owner, repo)
+        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
    }

    socketCounter += 1;
@@ -147,14 +187,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;
@@ -165,9 +205,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())
 })
@@ -1,4 +1,14 @@
-{"version": 6,
- "packagesDir": "lake-packages",
- "packages": [],
- "name": "GameServer"}
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/std4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.3.0-rc2",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "GameServer",
+ "lakeDir": ".lake"}
@@ -3,6 +3,11 @@ 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
+
 lean_lib GameServer

@[default_target]
@@ -1 +1 @@
-leanprover/lean4:v4.2.0
+leanprover/lean4:v4.3.0-rc2
@@ -1,13 +1,30 @@
 #/bin/bash

 ARTIFACT_ID=$1
+OWNER=$2
+REPO=$3
+
+# mkdir -p games
+cd games
+pwd
+# mkdir -p tmp
+mkdir -p ${OWNER}

 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
+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"
-  mkdir tmp/artifact_${ARTIFACT_ID}_inner
-  tar -xvf $f -C tmp/artifact_${ARTIFACT_ID}_inner
+  #tar -xvzf $f -C games/${OWNER}/${REPO}
+  unzip -q -o $f -d ${OWNER}/${REPO}
 done
@@ -5,6 +5,12 @@ 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 `server/index.mjs`
+    outDir: 'client/dist',
+  },
  plugins: [
    react(),
    svgr({
@@ -22,6 +28,9 @@ export default defineConfig({
    })
  ],
  publicDir: "client/public",
+  optimizeDeps: {
+    exclude: ['games']
+  },
  server: {
    port: 3000,
    proxy: {
@@ -29,6 +38,12 @@ export default defineConfig({
        target: 'ws://localhost:8080',
        ws: true
      },
+      '/import': {
+        target: 'http://localhost:8080',
+      },
+      '/api': {
+        target: 'http://localhost:8080',
+      },
    }
  },
  resolve: {
@@ -1,106 +0,0 @@
-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/]
-  };
-}
Author	SHA1	Message	Date
Jon Eugster	622e9d3897	Update update_game.md	2023-11-30 19:32:38 +01:00
joneugster	7f91ae7da8	Merge branch 'dev'	2023-11-30 19:29:18 +01:00
joneugster	28a7c65db2	update doc, including #148	2023-11-30 19:26:42 +01:00
joneugster	56525c6234	update doc	2023-11-30 17:39:29 +01:00
joneugster	44f7b6703e	Revert "fix variables in hints" This reverts commit `8851cd8b1f`.	2023-11-30 12:16:06 +01:00
joneugster	8851cd8b1f	fix variables in hints	2023-11-30 11:18:56 +01:00
Alexander Bentkamp	bae360874c	json api	2023-11-30 10:51:03 +01:00
joneugster	07b6525c58	fix local setup	2023-11-30 09:20:16 +01:00
joneugster	8e8026aa38	more fixing	2023-11-29 15:17:16 +01:00
joneugster	a3a421f504	fix bubblewrap script	2023-11-29 15:14:00 +01:00
joneugster	084e25c0dc	wip on imports	2023-11-29 14:43:33 +01:00
Alexander Bentkamp	6580afb622	fix names in hints Fixes #135	2023-11-28 20:51:44 +01:00
joneugster	0c0a7ab400	bubblewrap test	2023-11-28 16:32:19 +01:00
joneugster	dfb2f10219	correct std version	2023-11-28 16:27:20 +01:00
Alexander Bentkamp	a57a5af111	also display loading of constants	2023-11-28 14:53:05 +01:00
joneugster	946a7fa673	update gitignore	2023-11-28 14:26:41 +01:00
Alexander Bentkamp	244c373192	model.dispose()	2023-11-28 14:05:15 +01:00
Alexander Bentkamp	374afa318a	fix gameserver path	2023-11-28 13:55:24 +01:00
joneugster	d0636b1d85	update workflow	2023-11-28 13:45:13 +01:00
joneugster	2e121363b3	update workflow	2023-11-28 13:45:13 +01:00
Alexander Bentkamp	590d68ccfb	gitignore .lake	2023-11-28 11:43:55 +01:00
Alexander Bentkamp	f6727e5c9f	loading progress	2023-11-28 11:43:32 +01:00
joneugster	241ef4b67a	bump to v4.3.0-rc2	2023-11-28 11:29:40 +01:00
joneugster	ea4250f38d	modify message of import script	2023-11-28 11:26:07 +01:00
joneugster	1d2420331d	make URL case insensitive	2023-11-28 11:05:50 +01:00
joneugster	2213862998	disable bad try catch	2023-11-27 22:48:46 +01:00
joneugster	81073b24b8	fix bubblewrap script	2023-11-27 22:42:31 +01:00
joneugster	33068f1183	improve error message	2023-11-27 22:10:15 +01:00
joneugster	8ab37d4344	disable queue	2023-11-27 22:06:16 +01:00
joneugster	9d9902cce1	edit pm2 config	2023-11-27 21:29:22 +01:00
joneugster	f53316c591	fix paths	2023-11-27 20:57:18 +01:00
joneugster	427ce43e95	fix import mechanism	2023-11-27 17:22:02 +01:00
joneugster	15d79244d4	update workflow	2023-11-27 16:50:45 +01:00
joneugster	f13027f75c	update workflow	2023-11-27 16:47:35 +01:00
joneugster	5fcdee4f71	import seems to be working	2023-11-27 16:40:38 +01:00
joneugster	7ad23dab24	work on importing	2023-11-22 15:54:45 +01:00
joneugster	89e19cc019	update lean4web and npm packages	2023-11-22 13:14:18 +01:00
joneugster	4db5260ed8	shrink nng image	2023-11-20 12:31:37 +01:00
joneugster	d19046aebd	fix dist path	2023-11-20 12:27:23 +01:00
joneugster	6e0fcb1d50	fixes for vite	2023-11-20 11:19:25 +01:00
joneugster	04c70ba522	fix for STG on landing page	2023-11-18 12:12:19 +01:00
joneugster	1b3993ad3e	fix	2023-11-17 22:45:02 +01:00
joneugster	45a95bbdc4	update landing page	2023-11-17 22:27:29 +01:00
joneugster	7c9f3d7a0a	remove token	2023-11-17 16:43:42 +01:00
joneugster	823000d5d4	partial implementation of loading mechanism	2023-11-17 13:10:07 +01:00
joneugster	c706b66af1	update doc to use -K option for local setup	2023-11-14 21:52:23 +01:00
Jon Eugster	933394bb6f	Update running_locally.md	2023-11-10 11:16:25 +01:00
Jon Eugster	e09c016c4c	Update update_game.md	2023-11-10 11:15:53 +01:00