Update docs

Minor: correct error in markdown

README.md

@@ -1,6 +1,6 @@
 # Lean 4 Game
 
-This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
+This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
 
 ## Creating a Game
 
@@ -28,7 +28,9 @@ should be up-to-date:
 
 ### Backend
 
-not written yet
+not fully written yet.
+
+* [Server](doc/DOCUMENTATION.md): describes the server part (i.e. the content of `server/` und `relay/`).
 
 ## Contributing
 
@@ -40,7 +42,8 @@ Providing the use access to a Lean instance running on the server is a severe se
 
 ## Credits
 
-The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
+The project has pimarily been developed by Alexander Bentkamp and Jon Eugster.
+
+It is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
 (NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
-by Kevin Buzzard and Mohammad Pedramfar.
-The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
+by Kevin Buzzard and Mohammad Pedramfar, and on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).

client/src/app.tsx

@@ -11,7 +11,6 @@ import './css/app.css';
 import { MobileContext } from './components/infoview/context';
 import { useMobile } from './hooks';
 import { AUTO_SWITCH_THRESHOLD, getWindowDimensions} from './state/preferences';
-import { connection } from './connection';
 
 export const GameIdContext = React.createContext<string>(undefined);
 
@@ -37,10 +36,6 @@ function App() {
     }
   }, [lockMobile])
 
-  React.useEffect(() => {
-    connection.startLeanClient(gameId);
-  }, [gameId])
-
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>

client/src/components/level.tsx

@@ -18,7 +18,6 @@ import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-info
 import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event'
 
 import { GameIdContext } from '../app'
-import { ConnectionContext, connection, useLeanClient } from '../connection'
 import { useAppDispatch, useAppSelector } from '../hooks'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'
 import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited,
@@ -44,6 +43,15 @@ import 'lean4web/client/src/editor/infoview.css'
 import 'lean4web/client/src/editor/vscode.css'
 import '../css/level.css'
 import { LevelAppBar } from './app_bar'
+import { LeanClient } from 'lean4web/client/src/editor/leanclient'
+import { DisposingWebSocketMessageReader } from 'lean4web/client/src/reader'
+import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc'
+import { IConnectionProvider } from 'monaco-languageclient'
+import { monacoSetup } from 'lean4web/client/src/monacoSetup'
+import { onigasmH } from 'onigasm/lib/onigasmH'
+
+
+monacoSetup()
 
 function Level() {
   const params = useParams()
@@ -211,10 +219,8 @@ function PlayableLevel({impressum, setImpressum}) {
 
   const dispatch = useAppDispatch()
 
-  const difficulty = useSelector(selectDifficulty(gameId))
   const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
   const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
-  const inventory: Array<String> = useSelector(selectInventory(gameId))
 
   const typewriterMode = useSelector(selectTypewriterMode(gameId))
   const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
@@ -293,12 +299,6 @@ function PlayableLevel({impressum, setImpressum}) {
   // a hint at the beginning of the proof...
   const [selectedStep, setSelectedStep] = useState<number>()
 
-  // if the user inventory changes, notify the server
-  useEffect(() => {
-    let leanClient = connection.getLeanClient(gameId)
-    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty})
-  }, [inventory])
-
   useEffect (() => {
     // Lock editor mode
     if (level?.data?.template) {
@@ -372,7 +372,7 @@ function PlayableLevel({impressum, setImpressum}) {
 
   // Effect when command line mode gets enabled
   useEffect(() => {
-    if (editor && typewriterMode) {
+    if (onigasmH && editor && typewriterMode) {
       let code = editor.getModel().getLinesContent().filter(line => line.trim())
       editor.executeEdits("typewriter", [{
         range: editor.getModel().getFullModelRange(),
@@ -395,7 +395,7 @@ function PlayableLevel({impressum, setImpressum}) {
       //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
       // }
     }
-  }, [editor, typewriterMode])
+  }, [editor, typewriterMode, onigasmH == null])
 
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
@@ -531,21 +531,32 @@ function Introduction({impressum, setImpressum}) {
 
 function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {
 
-  const connection = React.useContext(ConnectionContext)
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
 
-
   const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
   const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
-  const [infoviewApi, setInfoviewApi] = useState<null|InfoviewApi>(null)
   const [editorConnection, setEditorConnection] = useState<null|EditorConnection>(null)
 
-  // Create Editor
+  const uriStr = `file:///${worldId}/${levelId}`
+  const uri = monaco.Uri.parse(uriStr)
+
+  const inventory: Array<String> = useSelector(selectInventory(gameId))
+  const difficulty: number = useSelector(selectDifficulty(gameId))
+
   useEffect(() => {
+    const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri)
+    if (onDidChangeContent) {
+      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
+    }
+
     const editor = monaco.editor.create(codeviewRef.current!, {
+      model,
       glyphMargin: true,
       quickSuggestions: false,
+      lineDecorationsWidth: 5,
+      folding: false,
+      lineNumbers: 'on',
       lightbulb: {
         enabled: true
       },
@@ -557,11 +568,61 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
         enabled: false
       },
       lineNumbersMinChars: 3,
+      tabSize: 2,
       'semanticHighlighting.enabled': true,
       theme: 'vs-code-theme-converted'
     })
+    if (onDidChangeSelection) {
+      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
+    }
+    if (initialSelections) {
+      console.debug("Initial Selection: ", initialSelections)
+      // BUG: Somehow I get an `invalid arguments` bug here
+      // editor.setSelections(initialSelections)
+    }
+    setEditor(editor)
+    const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
 
-    const infoProvider = new InfoProvider(connection.getLeanClient(gameId))
+    const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + gameId
+
+    const connectionProvider : IConnectionProvider = {
+      get: async () => {
+        return await new Promise((resolve, reject) => {
+          console.log(`connecting ${socketUrl}`)
+          const websocket = new WebSocket(socketUrl)
+          websocket.addEventListener('error', (ev) => {
+            reject(ev)
+          })
+          websocket.addEventListener('message', (msg) => {
+            // console.log(msg.data)
+          })
+          websocket.addEventListener('open', () => {
+            const socket = toSocket(websocket)
+            const reader = new DisposingWebSocketMessageReader(socket)
+            const writer = new WebSocketMessageWriter(socket)
+            resolve({
+              reader,
+              writer
+            })
+          })
+        })
+      }
+    }
+
+    // Following `vscode-lean4/webview/index.ts`
+    const client = new LeanClient(connectionProvider, showRestartMessage, {inventory, difficulty})
+    const infoProvider = new InfoProvider(client)
+    // const div: HTMLElement = infoviewRef.current!
+    const imports = {
+      '@leanprover/infoview': `${window.location.origin}/index.production.min.js`,
+      'react': `${window.location.origin}/react.production.min.js`,
+      'react/jsx-runtime': `${window.location.origin}/react-jsx-runtime.production.min.js`,
+      'react-dom': `${window.location.origin}/react-dom.production.min.js`,
+      'react-popper': `${window.location.origin}/react-popper.production.min.js`
+    }
+    // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi)
+    setInfoProvider(infoProvider)
+    client.restart()
 
     const editorApi = infoProvider.getApi()
 
@@ -606,54 +667,27 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
 
     setEditor(editor)
     setInfoProvider(infoProvider)
-    setInfoviewApi(infoviewApi)
 
-    return () => { infoProvider.dispose(); editor.dispose() }
-  }, [])
+    infoProvider.openPreview(editor, infoviewApi)
+    const taskgutter = new LeanTaskGutter(infoProvider.client, editor)
 
-  const {leanClient, leanClientStarted} = useLeanClient(gameId)
-  const uriStr = `file:///${worldId}/${levelId}`
-  const uri = monaco.Uri.parse(uriStr)
+    // TODO:
+    // setRestart(() => restart)
 
-  // Create model when level changes
-  useEffect(() => {
-    if (editor && leanClientStarted) {
-
-      let model = monaco.editor.getModel(uri)
-      if (!model) {
-        model = monaco.editor.createModel(initialCode, 'lean4', uri)
-      }
-      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
-      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
-      editor.setModel(model)
-      if (initialSelections) {
-        console.debug("Initial Selection: ", initialSelections)
-        // BUG: Somehow I get an `invalid arguments` bug here
-        // editor.setSelections(initialSelections)
-      }
-
-      return () => {
-        editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
-        model.dispose();
-      }
+    return () => {
+      editor.dispose();
+      model.dispose();
+      abbrevRewriter.dispose();
+      taskgutter.dispose();
+      infoProvider.dispose();
+      client.dispose();
     }
-  }, [editor, levelId, connection, leanClientStarted])
+  }, [gameId, worldId, levelId])
 
-
-  useEffect(() => {
-    if (editor && leanClientStarted) {
-
-      let model = monaco.editor.getModel(uri)
-      infoviewApi.serverRestarted(leanClient.initializeResult)
-
-      infoProvider.openPreview(editor, infoviewApi)
-
-      const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
-      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
-
-      return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
-    }
-  }, [editor, connection, leanClientStarted])
+  const showRestartMessage = () => {
+    // setRestartMessage(true)
+    console.log("TODO: SHOW RESTART MESSAGE")
+  }
 
   return {editor, infoProvider, editorConnection}
 }

client/src/connection.ts

@@ -1,68 +0,0 @@
-/**
- *  @fileOverview todo
- */
-
-import * as React from 'react';
-import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
-import { LeanClient } from 'lean4web/client/src/editor/leanclient';
-
-export class Connection {
-  private game: string = undefined // We only keep a connection to a single game at a time
-  private leanClient: LeanClient = null
-
-  getLeanClient(game): LeanClient {
-    if (this.game !== game) {
-      if (this.leanClient) {
-        this.leanClient.stop() // Stop previous Lean client
-      }
-      this.game = game
-      // Start a new Lean client for the new `gameId`.
-      const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + game
-      const uri = monaco.Uri.parse('file:///')
-      this.leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
-    }
-
-    return this.leanClient
-  }
-
-  /** If not already started, starts the Lean client. resolves the returned promise as soon as a
-   * Lean client is running.
-   */
-  startLeanClient = (game) => {
-    return new Promise<LeanClient>((resolve) => {
-      const leanClient = this.getLeanClient(game)
-      if (leanClient.isRunning()) {
-        resolve(leanClient)
-      } else {
-        if (!leanClient.isStarted()) {
-          leanClient.start()
-        }
-        leanClient.restarted(() => {
-          // This keep alive message is not recognized by the server,
-          // but it makes sure that the websocket connection does not
-          // time out after 60 seconds.
-          setInterval(() => {leanClient.sendNotification('$/keepAlive', {}) }, 5000)
-          resolve(leanClient)
-        })
-      }
-    })
-  }
-}
-
-export const connection = new Connection()
-
-export const ConnectionContext = React.createContext(null);
-
-export const useLeanClient = (gameId) => {
-  const leanClient = connection.getLeanClient(gameId)
-  const [leanClientStarted, setLeanClientStarted] = React.useState(leanClient.isStarted())
-
-  React.useEffect(() => {
-    const t1 = leanClient.restarted(() => { console.log("START"); setLeanClientStarted(true) })
-    const t2 = leanClient.stopped(() => { console.log("STOP"); setLeanClientStarted(false) })
-
-    return () => {t1.dispose(); t2.dispose()}
-  }, [leanClient, setLeanClientStarted])
-
-  return {leanClientStarted, leanClient}
-}

client/src/index.tsx

@@ -1,7 +1,6 @@
 import * as React from 'react'
 import { createRoot } from 'react-dom/client'
 import App from './app'
-import { ConnectionContext, connection } from './connection'
 import { store } from './state/store'
 import { Provider } from 'react-redux'
 import type { RouteObject } from "react-router"
@@ -10,11 +9,8 @@ import ErrorPage from './components/error_page'
 import Welcome from './components/welcome'
 import LandingPage from './components/landing_page'
 import Level from './components/level'
-import { monacoSetup } from 'lean4web/client/src/monacoSetup'
 
 
-monacoSetup()
-
 
 // If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
 // `/g/local/game`. This is used for the devcontainer setup
@@ -61,9 +57,7 @@ const root = createRoot(container!);
 root.render(
   <React.StrictMode>
     <Provider store={store}>
-      <ConnectionContext.Provider value={connection}>
-        <RouterProvider router={router} />
-      </ConnectionContext.Provider>
+      <RouterProvider router={router} />
     </Provider>
   </React.StrictMode>
 );

client/src/state/store.ts

@@ -19,11 +19,7 @@ export const store = configureStore({
   },
   // Make connection available in thunks:
   middleware: getDefaultMiddleware =>
-    getDefaultMiddleware({
-      thunk: {
-        extraArgument: { connection }
-      }
-    }).concat(apiSlice.middleware),
+    getDefaultMiddleware().concat(apiSlice.middleware),
 });
 
 /**

doc/DOCUMENTATION.md

@@ -1,335 +1,67 @@
-**NOTE! This document is deprecated! The current documentation is [How To Create A Game](create_game.md)**
+# Server
 
-# Creating a game.
+The server is made out of two parts, named "relay" and "server".
 
-Ideally one takes the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new game.
+The former, "relay", is the server which
+sets up a socket connection to the client, starts the lean servers to work on files and
+relays messages between the lean server and the client. `index.mjs` is the file that needs to
+be run, which is done for example using `pm2` or by calling `npm run start_server` or
+`npm run production`, see more later.
 
-## Game Structure
+The latter, "server", is the lean server which has two jobs. For one it produces the "gameserver"
+executable which is the lean server that handles the files the player plays on. The second job
+is to provide the lean commands which are used when creating a game. These are located in
+`Commands.lean`.
 
-A game consist of worlds which have multiple levels each. In the following we describe how to create a level file and how to combine these into a game.
 
-### Level
+## Integration into Games
 
-A level file is a lean file that imports at least `import GameServer.Commands` and starts with the following Lean commands.
+Games need the "server" as a lake-dependency, which is done in the game's lakefile.
+
+A game imports `GameServer.Commands` which provides to all the API required to
+create a game.
+
+In particular the lean command `MakeGame` compiles the entire game. Static information is
+stored as JSON files in `.lake/gamedata` for faster loading, while other data is only
+saved to lean env-extensions which the lean server has access to after loading the lean file.
+
+For games to be run successfully, it is important that the "gameserver" executable inside
+the game's `.lake` folder is actually built.
+Currently this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`.
+(both commands are to be executed in the game's directory!)
+
+## Modifying the server
+
+### Starting the server
+
+When using the [manual installation](running_locally.md#manual-installation) you can run the server
+using
 
-```lean
-Game "NNG"
-World "Addition"
-Level 1
-Title "The rfl tactic"
 ```
-
-Note that the levels inside a world must have consecutive numbering starting with `1`. The `Game`
-and `World` strings can be anything, see below.
-
-#### Statement
-
-The core of a level is the `Statement`, which is the exercise that should be proven.
-
-```lean
-/-- For all natural numbers $n$, we have $0 + n = n$. -/
-@[simp]
-Statement MyNat.zero_add
-    (n : ℕ) : 0 + n = n := by
-  Hint "You can start a proof by `induction n`."
-  induction n with n hn
-  · Hint "This is the base case."
-    rw [add_zero]
-    rfl
-  · Hint "This is the induction hypothesis"
-    rw [add_succ]
-    Branch
-      simp
-      Hint "A branch is an alternative tactic sequence. Does not need to finish the proof."
-    rw [hn]
-    rfl
-```
-
-##### Proof
-
-The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax.
-
-There are a few extra tactics that help you structuring the proof:
-
-- `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
-  the one where `Hint` is placed. For more options about hints, see below.
-- `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which
-  helps setting `Hints` in different   places. The `Branch` does not affect the main
-  proof and does not need to finish any goals.
-- `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template`
-  will be copied into the editor with all `Hole`s replaced with `sorry`. Note that
-  having a `Template` will force the user to use Editor-mode for this level.
-
-##### Statement Name (optional)
-
-If you specify a name (`MyNat.zero_add`), this lemma will be available in future levels.
-(Note that a future level must also import this level,
-so that Lean knows about the added statement).
-
-The name must be *fully qualified*. (TODO: is that still true? Did we implement namespaces?)
-
-##### Doc Comment (optional)
-
-There are three places where the documentation comment appears:
-
-1. as doc comment when hovering over the theorem
-2. as exercise description at the top of the level: ``Theorem `zero_add`: yada yada.``
-3. in the inventory. This can be overwritten by using
-  `LemmaDoc MyNat.zero_add "different yada yada"` as one might want to add a more detailed
-  description there including examples etc.
-
-Both latter points support Markdown (including katex).
-
-##### Attributes (optional)
-
-the `@[ attributes ]` prefix should work just like you know it from the `theorem` keyword.
-
-#### Introduction/Conclusion
-
-Optionally, you can add an `Introduction "some text"` and `Conclusion "some text"` to your level.
-The introduction will be shown at the beginning, the conclusion is displayed once the level
-is solved.
-
-#### Theorems/Tactics/Definitions
-
-Only enabled theorems/tactics/definitions (called "items" here) are available in a level.
-
-To add a new item in a level, you can add
-
-```lean
-NewTactic rfl simp
-NewLemma MyNat.add_zero MyNat.add_succ
-NewDefinition Nat Pow Mul
-```
-
-Once added, items will be available in all future levels/worlds,
-unless you disable them for a particular level with
-
-```lean
-DisabledTactic tauto
-DisabledLemma MyNat.add_zero
-```
-
-or specify explicitly which items should be available with
-
-```lean
-OnlyTactic rw rfl apply
-OnlyLemma MyNat.add_zero
-```
-
-Lastly, all items need documentation entries (which are imported in the level),
-see more about that below. There is also explains the `LemmaTab` keyword.
-
-### World
-
-Multiple levels are combined into a world and the worlds are then added to the game. It is recommended that all levels of a world are inside one folder (e.g. `NNG/Levels/Addition/`) and
-then there is one world file (`NNG/Levels/Addition.lean`) which contains the following
-
-```lean
-import NNG.Levels.Addition.Level_1
-import NNG.Levels.Addition.Level_2
-
-Game "NNG"
-World "Addition"
-Title "Addition World"
-
-Introduction "some text"
-```
-
-The `Title` is the world's display title. The `Introduction` is displayed before loading level 1.
-Note that all levels of a world should be imported by the world file.
-
-BUG: A level **must not** be imported in a different world's level. Instead, you have to import an entire world there: `import NNG.Levels.Addition`
-
-### Game
-
-The Game itself (i.e. the main file of you lake project, `NNG.lean`) should import all worlds and have the following layout, concluding with `MakeGame`:
-
-```lean
-import NNG.Levels.Addition
-import NNG.Levels.Multiplication
-import NNG.Levels.Power
-
-Game "NNG"
-Title "Natural Number Game"
-Introduction "some text"
-
-MakeGame
-```
-
-The game will automatically compute the order of the worlds depending on the sample proofs of the Levels (ignoring anything inside a `Branch`). You can add additional dependencies manually by adding `Dependency PowerWorld → ImpossibleWorld` before `MakeGame`.
-The order of worlds influences which tactics and lemmas will be unlocked in a given level.
-
-`MakeGame` will display warnings about things in the game that need to be fixed, like missing
-documentation or if a tactic is never introduced.
-
-### Documentation
-
-Each tactic, theorem, or definition (all called items here) that is introduced in the game
-needs a documentation entry. These are statements of the following form:
-
-```lean
-LemmaDoc MyNat.add_squared as "add_squared" in "Pow"
-"(missing)"
-
-TacticDoc constructor
-"(missing)"
-
-DefinitionDoc One as "1"
-"(missing)"
-```
-
-Notes:
-
-* The lemma name must be **fully qualified**. The string display name can be arbitrary.
-* Tactics must have their proper name. use `TacticDoc «have» ""` if it does not work
-  without french quotes.
-* Definition names can be arbitrary. E.g. I used `DefinitionDoc Symbol.Fun as "fun x ↦ x" "(missing)"` once.
-
-Moreover, the lemmas are in sorted in tabs (the `in "Pow`) part. In each level file, you
-can define which tab is open when the level is loaded by adding `LemmaTab "Pow"`.
-
-There will be features added to get automatic information from mathlib!
-
-## Escaping
-(TODO: Move)
-
-
-Inside the doc comment you don't need to escape the backslashes:
-
-```lean
-/-- $\operatorname{succ}(n)$. notation for naturals is `\N`. -/
-Statement ...
-```
-
-However, inside interpolated strings (e.g. in `Hint`, `Introduction` and `Conclusion`)
-you do need to escape backslashes
-with `\\` and `{` with `\{`:
-
-```lean
-Hint "This code has some $\\operatorname\{succ}(n)$ math. The value of `h` is {h}.
-Notation for naturals is `\\N`."
-```
-
-## Game design
-Here are some things you should consider designing a new game:
-
-* A world with more than 16 levels will be displayed with the levels spiraling outwards,
-  it might be desirable to stay below that bound. Above 22 levels the spiral start getting out
-  of control.
-
-# Running Games Locally
-
-The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
-
-## VSCode Dev Containers
-
-1.  **Install Docker and Dev Containers** *(once)*:<br/>
-    See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
-    Explicitly this means:
-    * Install docker engine if you have not yet: [Instructions](https://docs.docker.com/engine/install/).
-      I followed the "Server" instructions for linux.
-    * Note that on Linux you need to add your user to the `docker` group
-      ([see instructions](https://docs.docker.com/engine/install/linux-postinstall/)) and probably reboot.
-    * Open the games folder in VSCode: `cd NNG4 && code .` or "Open Folder" within VSCode
-    * a message appears prompting you to install the "Dev Containers" extension (by Microsoft).
-
-2.  **Open Project in Dev Container** *(everytime)*:<br/>
-    Once you have the Dev Containers Extension installed, (re)open the project folder of your game in VSCode.
-    A message appears asking you to "Reopen in Container".
-
-    * The first start will take a while, ca. 2-10 minutes. After the first
-      start this should be very quickly.
-    * Once built, it should open a tab "Simple Browser" inside VSCode displaying
-      the game. (Alternatively, open http://localhost:3000 in your browser).
-
-3.  **Editing Files** *(everytime)*:<br/>
-    After editing some files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`.
-    Now you can reload your browser to see the changes.
-
-### Errors
-
-* If you don't get the pop-up, you might have disabled them and you can reenable it by
-  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
-* If the starting the container fails, in particular with a message `Error: network xyz not found`,
-  you might have deleted stuff from docker via your shell. Try deleting the container and image
-  explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
-  container. (this will again take some time)
-
-
-## Without Dev Containers
-Install `nvm`:
-```bash
-curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
-```
-then reopen bash and test with `command -v nvm` if it is available (Should print "nvm").
-
-Now install node:
-```bash
-nvm install node
-```
-
-Clone the game (e.g. `NNG4` here):
-```bash
-git clone https://github.com/hhu-adam/NNG4.git
-# or: git clone git@github.com:hhu-adam/NNG4.git
-```
-
-Download dependencies and build the game:
-```bash
-cd NNG4
-lake update
-lake exe cache get   # if your game depends on mathlib
-lake build
-```
-
-Clone the game repository into a directory next to the game:
-```bash
-cd ..
-git clone https://github.com/leanprover-community/lean4game.git
-# or: git clone git@github.com:leanprover-community/lean4game.git
-```
-The folders `NNG4` and `lean4game` must be in the same directory!
-
-In `lean4game`, install dependencies:
-```bash
-cd lean4game
-npm install
-```
-
-TODO: This is outdated!
-If you are developing a game other than `Robo` or `NNG4`, adapt the
-code at the beginning of `lean4game/relay/index.mjs`:
-```typescript
-const games = {
-    "g/hhu-adam/robo": {
-        dir: "../../../../Robo",
-        queueLength: 5
-    },
-    "g/hhu-adam/nng4": {
-        dir: "../../../../NNG4",
-        queueLength: 5
-    }
-}
-```
-
-Run the game:
-```bash
 npm start
 ```
 
-This takes a little time. Eventually, the server is available on http://localhost:3000/
-and the game is available on http://localhost:3000/#/g/hhu-adam/NNG4.
+This way any changes to files in `client/` or `relay/` will cause the server to restart automatically.
 
-### Modifying the GameServer
+Alternative, you can run `npm run build` followed by the commands
 
-When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with this
-setup by setting `export NODE_ENV=development` inside your local game before building it:
-
-```bash
-cd NNG4
-export NODE_ENV=development
-lake update
-lake build
 ```
-This causes lake to search locally for the `GameServer` lake package instead of using the version from github.
+npm run start_client
+npm run production
+```
+
+(in two separate terminals) to test the production modus of the server. This way it will only
+change once you build and restart the server.
+
+### Modifying the lean server
+
+To test a modified lean server (i.e. content of `server/`), you can use the local dev setup and call
+`lake update -R -Klean4game.local` in your game followed by `lake build`.
+This will cause lake to look for the
+local lean server as a dependency instead of the version it downloaded from git.
+
+You can play a local game at https://localhost:3000/#/g/local/{FolderName} where you replace `{FolderName}` with the game folder name.
+
+After modifications in `server/`, you will need to call `lake build gameserver` (called in `server/` or in your game's folder) to rebuild
+the gameserver executable and
+`lake build` (called in the game's folder) to rebuild the game.

doc/create_game.md

@@ -129,6 +129,9 @@ NewLemma Nat.zero_mul
 NewDefinition Pow
 ```
 
+**Important:** All commands in this section 6a) expect the `Name` they take as input
+to be **fully qualified**. For example `NewLemma Nat.zero_mul` and not `NewLemma zero_mul`.
+
 #### Doc entries
 
 You'll see a warning about a missing Lemma documentation. You can fix it by adding doc-entries like the following somewhere above it.
@@ -182,6 +185,8 @@ The statement is the exercise of the level. the basics work the same as they wou
 
 You can give your exercise a name: `Statement my_first_exercise (n : Nat) ...`. If you do so, it will be added to the inventory and be available in future levels.
 
+You can but a `Statement` inside namespaces like you would with `theorem`.
+
 #### Doc String / Exercise statement
 
 Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports Latex.

doc/hints.md

@@ -10,6 +10,8 @@ Statement .... := by
   ...
 ```
 
+Note that hints are only **context-aware but not history-aware**. In particular they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps placing hints outside the sample solution's proof.
+
 ## 1. When do hints show?
 
 A hint will be displayed if the player's goal matches the one where the hint was placed in the

doc/publish_game.md

@@ -1,6 +1,6 @@
 # Publishing games
 
-You can publish your game on the official (Lean Game Server)[https://adam.math.hhu.de] in a few simple
+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

doc/running_locally.md

@@ -2,6 +2,8 @@
 
 The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
 
+Please also consult the [Troubleshooting Collection](doc/troubleshoot.md), where some known pitfalls are collected.
+
 There are several options to play a game locally:
 
 1. VSCode Dev Container: needs `docker` installed on your machine
@@ -36,16 +38,6 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta
 3.  **Editing Files** *(everytime)*:<br/>
     After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes.
 
-### Errors
-
-* If you don't get the pop-up, you might have disabled them and you can reenable it by
-  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
-* If the starting the container fails, in particular with a message `Error: network xyz not found`,
-  you might have deleted stuff from docker via your shell. Try deleting the container and image
-  explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
-  container. (this will again take some time)
-* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.
-
 ## Codespaces
 
 You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".

doc/update_game.md

@@ -9,8 +9,8 @@ Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https:
 
 Then, depending on the setup you use, do one of the following:
 
-* Dev Container: Rebuild the VSCode Devcontainer.
-* Local Setup: in your game's folder run the following:
+* **Dev Container**: Rebuild the VSCode Devcontainer (without Cache!).
+* **Local Setup**: in your game's folder run the following:
   ```
   lake update -R
   lake build
@@ -24,7 +24,7 @@ Then, depending on the setup you use, do one of the following:
     npm install
     ```
     where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
-* Gitpod/Codespaces: Create a fresh one
+* **Gitpod/Codespaces**: Create a fresh one
 
 This will update your game (and the mathlib version you might be using) to the new lean version.
 

package-lock.json

@@ -31,7 +31,7 @@
         "debounce": "^1.2.1",
         "express": "^4.18.2",
         "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-        "lean4web": "github:hhu-adam/lean4web",
+        "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
         "octokit": "^2.0.14",
         "path-browserify": "^1.0.1",
         "react": "^18.2.0",
@@ -2539,9 +2539,9 @@
       }
     },
     "node_modules/@leanprover/infoview": {
-      "version": "0.4.3",
-      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.3.tgz",
-      "integrity": "sha512-SufdOr2myHAbZNUmobfQdAhsEC5H9ddi3KS0z1v/8riWSMm+yJk3u4LxVuzCmmSmV2QxFqtFzn5z+HQqj1Vo7g==",
+      "version": "0.4.4",
+      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.4.tgz",
+      "integrity": "sha512-OxHffFaHcEudLyBEWpicOl7TfXuTYxW5Sz1RkHdUINWJpQsQn60YDF5fNRKmSb0d/fm7p+LVeBvM273jvfR5wQ==",
       "dependencies": {
         "@leanprover/infoview-api": "~0.2.1",
         "@vscode/codicons": "^0.0.32",
@@ -10081,7 +10081,8 @@
     },
     "node_modules/lean4web": {
       "version": "0.1.0",
-      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#6fc9c11179934cce7ca1f78140c57b6931186b42",
+      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
+      "integrity": "sha512-s9qYeXuMNBGDPKC5IuFTjV/j8tQCRkZr+poYKEWljrM95rsz4JHIvjdEt891fE9JhPDLSN+iXNRXwIOCT6FlMg==",
       "dependencies": {
         "@emotion/react": "^11.11.1",
         "@emotion/styled": "^11.11.0",
@@ -10090,7 +10091,7 @@
         "@fortawesome/fontawesome-svg-core": "^6.2.0",
         "@fortawesome/free-solid-svg-icons": "^6.2.0",
         "@fortawesome/react-fontawesome": "^0.2.0",
-        "@leanprover/infoview": "^0.4.3",
+        "@leanprover/infoview": "^0.4.4",
         "@mui/material": "^5.13.7",
         "@vitejs/plugin-react-swc": "^3.4.0",
         "express": "^4.18.2",

package.json

@@ -28,7 +28,7 @@
     "debounce": "^1.2.1",
     "express": "^4.18.2",
     "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-    "lean4web": "github:hhu-adam/lean4web",
+    "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
     "octokit": "^2.0.14",
     "path-browserify": "^1.0.1",
     "react": "^18.2.0",

relay/unpack.sh

@@ -28,3 +28,7 @@ do
   #tar -xvzf $f -C games/${OWNER}/${REPO}
   unzip -q -o $f -d ${OWNER}/${REPO}
 done
+
+# Delete temporary files
+rm -f tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip
+rm -fr tmp/${OWNER}_${REPO}_${ARTIFACT_ID}

server/GameServer.lean

@@ -1,5 +1,4 @@
 import GameServer.FileWorker
-import GameServer.Watchdog
 import GameServer.Commands
 
 -- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`
@@ -10,13 +9,9 @@ unsafe def main : List String → IO UInt32 := fun args => do
 
   Lean.enableInitializersExecution
 
+  -- TODO: remove this argument
   if args[0]? == some "--server" then
-    MyServer.Watchdog.watchdogMain args
-  else if args[0]? == some "--worker" then
-    MyServer.FileWorker.workerMain {}
+    MyServer.FileWorker.workerMain {} args
   else
-    e.putStrLn s!"Expected `--server` or `--worker`"
+    e.putStrLn s!"Expected `--server`"
     return 1
-
-
--- TODO: Potentially it could be useful to pass in the `gameName` via the websocket connection

server/GameServer/EnvExtensions.lean

@@ -293,6 +293,7 @@ structure LevelInfo where
   descrText : Option String := none
   descrFormat : String := ""
   lemmaTab : Option String
+  module : Name
   displayName : Option String
   statementName : Option String
   template : Option String
@@ -317,6 +318,7 @@ def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
       | some tile => tile.category
       | none => none
     statementName := lvl.statementName.toString
+    module := lvl.module
     displayName := match lvl.statementName with
       | .anonymous => none
       | name => match (inventoryExt.getState env).find?
@@ -381,7 +383,7 @@ structure GameTile where
 
   TODO: What's the format? -/
   image: String := default
-deriving Inhabited, ToJson
+deriving Inhabited, ToJson, FromJson
 
 structure Game where
   /-- Internal name of the game. -/
@@ -401,7 +403,7 @@ structure Game where
   tile : GameTile := default
   /-- The path to the background image of the world. -/
   image : String := default
-deriving Inhabited, ToJson
+deriving Inhabited, ToJson, FromJson
 
 def getGameJson (game : «Game») : Json := Id.run do
   let gameJson : Json := toJson game

server/GameServer/FileWorker.lean

@@ -1,7 +1,8 @@
-/- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/
+/- This file is adapted from `Lean/Server/FileWorker.lean`. -/
 import Lean.Server.FileWorker
 import GameServer.Game
 import GameServer.ImportModules
+import GameServer.SaveData
 
 namespace MyModule
 open Lean
@@ -17,7 +18,7 @@ private def mkEOI (pos : String.Pos) : Syntax :=
   mkNode ``Command.eoi #[atom]
 
 partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
-  (mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) :
+  (mps : ModuleParserState) (messages : MessageLog) :
     Syntax × ModuleParserState × MessageLog × String.Pos := Id.run do
   let mut pos := mps.pos
   let mut recovering := mps.recovering
@@ -56,6 +57,20 @@ open IO
 open Snapshots
 open JsonRpc
 
+structure GameWorkerState :=
+  inventory : Array String
+  /--
+  Check for tactics/theorems that are not unlocked.
+  0: no check
+  1: give warnings
+  2: give errors
+  -/
+  difficulty : Nat
+  levelInfo : LevelInfo
+  deriving ToJson, FromJson
+
+abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
+
 section Elab
 
 def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
@@ -73,29 +88,30 @@ def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : Me
 /-- Find all tactics in syntax object that are forbidden according to a
 set `allowed` of allowed tactics. -/
 partial def findForbiddenTactics (inputCtx : Parser.InputContext)
-    (levelParams : Game.DidOpenLevelParams) (stx : Syntax) :
+    (gameWorkerState : GameWorkerState) (stx : Syntax) :
     Elab.Command.CommandElabM Unit := do
+  let levelInfo := gameWorkerState.levelInfo
   match stx with
   | .missing => return ()
   | .node _info _kind args =>
     for arg in args do
-      findForbiddenTactics inputCtx levelParams arg
+      findForbiddenTactics inputCtx gameWorkerState arg
   | .atom info val =>
     -- ignore syntax elements that do not start with a letter
     -- and ignore "with" keyword
     let allowed := ["with", "fun", "at", "only", "by", "to"]
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      match levelParams.tactics.find? (·.name.toString == val) with
+      match levelInfo.tactics.find? (·.name.toString == val) with
       | none =>
         -- Note: This case means that the tactic will never be introduced in the game.
-        match levelParams.inventory.find? (· == val) with
+        match gameWorkerState.inventory.find? (· == val) with
         | none =>
           addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
         | some _ => pure () -- tactic is in the inventory, allow it.
       | some tac =>
         if tac.locked then
-          match levelParams.inventory.find? (· == val) with
+          match gameWorkerState.inventory.find? (· == val) with
           | none =>
             addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
           | some _ => pure () -- tactic is in the inventory, allow it.
@@ -109,10 +125,10 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
         let some (.thmInfo ..) := (← getEnv).find? n
           | return () -- not a theorem -> ignore
         -- Forbid the theorem we are proving currently
-        if n = levelParams.statementName then
+        if some n = levelInfo.statementName then
           addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
 
-        let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions
+        let lemmasAndDefs := levelInfo.lemmas ++ levelInfo.definitions
         match lemmasAndDefs.find? (fun l => l.name == n) with
         | none => addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
         | some lem =>
@@ -121,7 +137,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
           else if lem.disabled then
             addWarningMessage info s!"The lemma/definition '{n}' is disabled in this level!"
 where addWarningMessage (info : SourceInfo) (s : MessageData) :=
-  let difficulty := levelParams.difficulty
+  let difficulty := gameWorkerState.difficulty
   if difficulty > 0 then
     modify fun st => { st with
       messages := st.messages.add {
@@ -137,7 +153,7 @@ where addWarningMessage (info : SourceInfo) (s : MessageData) :=
 
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
-    (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams)
+    (couldBeEndSnap : Bool) (gameWorkerState : GameWorkerState)
     (initParams : Lsp.InitializeParams) : IO Snapshot := do
   -- Recognize end snap
   if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
@@ -168,7 +184,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
     Elab.Command.catchExceptions
       (getResetInfoTrees *> do
         let some level ← GameServer.getLevelByFileName? initParams inputCtx.fileName
-          | throwError "Level not found: {inputCtx.fileName}"
+          | panic! s!"Level not found: {inputCtx.fileName} / {GameServer.levelIdFromFileName? initParams inputCtx.fileName}"
         let scope := level.scope
 
         -- use open namespaces and options as in the level file
@@ -186,12 +202,12 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
             currNamespace := scope.currNamespace,
             openDecls := scope.openDecls }
           let (tacticStx, cmdParserState, msgLog, endOfWhitespace) :=
-            MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap
+            MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog
           modify (fun s => { s with messages := msgLog })
           parseResultRef.set (tacticStx, cmdParserState)
 
           -- Check for forbidden tactics
-          findForbiddenTactics inputCtx levelParams tacticStx
+          findForbiddenTactics inputCtx gameWorkerState tacticStx
 
           -- Insert invisible `skip` command to make sure we always display the initial goal
           let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]
@@ -219,6 +235,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
     }
 
   let (tacticStx, cmdParserState) ← parseResultRef.get
+  if tacticStx.isMissing then throwServerError "Tactic execution went wrong. No stx found."
 
   let postCmdSnap : Snapshot := {
     beginPos := tacticStx.getPos?.getD 0
@@ -270,7 +287,7 @@ where
 
   /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
   private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-      (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams)
+      (gameWorkerState : GameWorkerState) (initParams : Lsp.InitializeParams)
       : AsyncElabM (Option Snapshot) := do
     cancelTk.check
     let s ← get
@@ -288,7 +305,7 @@ where
     -- we can see the current goal even on an empty document
     let couldBeEndSnap := s.snaps.size > 1
     let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
-      levelParams initParams
+      gameWorkerState initParams
     set { s with snaps := s.snaps.push snap }
     -- TODO(MH): check for interrupt with increased precision
     cancelTk.check
@@ -310,7 +327,7 @@ where
 
   /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
   def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
-      (startAfterMs : UInt32) (levelParams : Game.DidOpenLevelParams)
+      (startAfterMs : UInt32) (gameWorkerState : GameWorkerState)
       : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
     let ctx ← read
     let some headerSnap := snaps[0]? | panic! "empty snapshots"
@@ -326,21 +343,15 @@ where
       publishIleanInfoUpdate m ctx.hOut snaps
       return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
         IO.sleep startAfterMs
-        AsyncList.unfoldAsync (nextSnap ctx m cancelTk levelParams ctx.initParams) { snaps })
+        AsyncList.unfoldAsync (nextSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
 
 end Elab
 
-structure GameWorkerState :=
-(levelParams : Game.DidOpenLevelParams)
-
-abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
-
 section Updates
 
 /-- Given the new document, updates editable doc state. -/
   def updateDocument (newMeta : DocumentMeta) : GameWorkerM Unit := do
     let s ← get
-    let levelParams := s.levelParams
     let ctx ← read
     let oldDoc := (← StateT.lift get).doc
     oldDoc.cancelTk.set
@@ -382,7 +393,7 @@ section Updates
           validSnaps := validSnaps.dropLast
       -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
       -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
-      unfoldSnaps newMeta validSnaps.toArray cancelTk levelParams ctx
+      unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx
         (startAfterMs := ctx.initParams.editDelay.toUInt32)
     StateT.lift <| modify fun st => { st with
       doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
@@ -397,24 +408,23 @@ section Initialization
     fileMap  := default
 
   def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-      (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) :
+      (gameDir : String) (module : Name):
       IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
     -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
     let out ← IO.Process.output
-      { cwd := levelParams.gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
+      { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
     if out.exitCode != 0 then
       throwServerError s!"Error while running Lake: {out.stderr}"
 
     -- Make the paths relative to the current directory
     let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
     let currentDir ← IO.currentDir
-    let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p
+    let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
 
     -- Set the search path
     Lean.searchPathRef.set paths
 
-    let env ← importModules' #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }]
-    -- return (env, paths)
+    let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }]
 
     -- use empty header
     let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
@@ -458,10 +468,11 @@ section Initialization
       return (headerSnap, srcSearchPath)
 
   def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
-       (levelParams : Game.DidOpenLevelParams) : IO (WorkerContext × WorkerState) := do
+      (gameDir : String) (gameWorkerState : GameWorkerState) : IO (WorkerContext × WorkerState) := do
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
+
     let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-      levelParams initParams
+      gameDir gameWorkerState.levelInfo.module
     let cancelTk ← CancelToken.new
     let ctx :=
       { hIn  := i
@@ -472,12 +483,14 @@ section Initialization
         clientHasWidgets
       }
     let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk levelParams ctx (startAfterMs := 0)
+      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
       | Except.error e   => throw (e : ElabTaskError))
     let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
     return (ctx,
     { doc             := doc
       initHeaderStx   := headerStx
+      currHeaderStx      := headerStx
+      importCachingTask? := none
       pendingRequests := RBMap.empty
       rpcSessions     := RBMap.empty
     })
@@ -509,6 +522,7 @@ section MessageHandling
     match method with
     | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
     | "$/cancelRequest"        => handle CancelParams (handleCancelRequest ·)
+    | "$/setTrace"        => pure ()
     | "$/lean/rpc/release"     => handle RpcReleaseParams (handleRpcRelease ·)
     | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
     | _                        => throwServerError s!"Got unsupported notification method: {method}"
@@ -547,26 +561,32 @@ section MainLoop
       let doc := st.doc
       doc.cancelTk.set
       return ()
-    | Message.notification "$/game/setInventory" params =>
-      let p := (← parseParams Game.SetInventoryParams (toJson params))
-      let s ← get
-
-      set {s with levelParams := {s.levelParams with
-        inventory := p.inventory,
-        difficulty := p.difficulty}}
+    | Message.request id "shutdown" none =>
+      ctx.hOut.writeLspResponse ⟨id, Json.null⟩
       mainLoop
     | Message.notification method (some params) =>
       handleNotification method (toJson params)
       mainLoop
-    | _ => throwServerError "Got invalid JSON-RPC message"
+    | _ => throwServerError s!"Got invalid JSON-RPC message: {toJson msg}"
 end MainLoop
 
-def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
+def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
-  let initParams ← i.readLspRequestAs "initialize" InitializeParams
+  let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
+  o.writeLspResponse {
+    id     := initRequest.id
+    result := {
+      capabilities := Watchdog.mkLeanServerCapabilities
+      serverInfo?  := some {
+        name     := "Lean 4 Game Server"
+        version? := "0.1.1"
+      }
+      : InitializeResult
+    }
+  }
+  discard $ i.readLspNotificationAs "initialized" InitializedParams
   let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
-  let ⟨_, levelParams⟩ ← i.readLspNotificationAs "$/game/didOpenLevel" Game.DidOpenLevelParams
 
   let doc := param.textDocument
   /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
@@ -578,9 +598,24 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
-    let (ctx, st) ← initializeWorker meta i o e initParams.param opts levelParams
+    let game ← loadGameData gameDir
+    -- TODO: We misuse the `rootUri` field to the gameName
+    let rootUri? : Option String := some (toString game.name)
+    let initParams := {initRequest.param.toLeanInternal with rootUri?}
+    let some (levelId : LevelId) := GameServer.levelIdFromFileName?
+        initParams meta.mkInputContext.fileName
+      | throwServerError s!"Could not determine level ID: {meta.mkInputContext.fileName}"
+    let levelInfo ← loadLevelData gameDir levelId.world levelId.level
+    let some initializationOptions := initRequest.param.initializationOptions?
+      | throwServerError "no initialization options found"
+    let gameWorkerState : GameWorkerState:= {
+      inventory := initializationOptions.inventory
+      difficulty := initializationOptions.difficulty
+      levelInfo
+    }
+    let (ctx, st) ← initializeWorker meta i o e initParams opts gameDir gameWorkerState
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
-      StateT.run (s := {levelParams := levelParams}) <| (mainLoop)
+      StateT.run (s := gameWorkerState) <| (mainLoop)
     return (0 : UInt32)
   catch e =>
     IO.eprintln e
@@ -590,12 +625,13 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
       message := e.toString }] o
     return (1 : UInt32)
 
-def workerMain (opts : Options) : IO UInt32 := do
+def workerMain (opts : Options) (args : List String): IO UInt32 := do
   let i ← IO.getStdin
   let o ← IO.getStdout
   let e ← IO.getStderr
   try
-    let exitCode ← initAndRunWorker i o e opts
+    let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
+    let exitCode ← initAndRunWorker i o e opts gameDir
     -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't
     -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code
     o.flush

server/GameServer/Game.lean

@@ -25,75 +25,56 @@ open Lsp
 open JsonRpc
 open IO
 
-structure DidOpenLevelParams where
-  uri : String
-  gameDir : String
-  levelModule : Name
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  inventory : Array String
-  /--
-  Check for tactics/theorems that are not unlocked.
-  0: no check
-  1: give warnings
-  2: give errors
-  -/
+/- Game-specific version of `InitializeParams` that allows for extra options: -/
+
+structure InitializationOptions extends Lean.Lsp.InitializationOptions :=
   difficulty : Nat
-  /-- The name of the theorem to be proven in this level. -/
-  statementName : Name
+  inventory : Array String
   deriving ToJson, FromJson
 
-structure SetInventoryParams where
-  inventory : Array String
-  difficulty : Nat
-deriving ToJson, FromJson
+structure InitializeParams where
+  processId? : Option Int := none
+  clientInfo? : Option ClientInfo := none
+  /- We don't support the deprecated rootPath
+  (rootPath? : Option String) -/
+  rootUri? : Option String := none
+  initializationOptions? : Option InitializationOptions := none
+  capabilities : ClientCapabilities
+  /-- If omitted, we default to off. -/
+  trace : Trace := Trace.off
+  workspaceFolders? : Option (Array WorkspaceFolder) := none
+  deriving ToJson
 
-def handleDidOpenLevel (params : Json) : GameServerM Unit := do
-  let p ← parseParams _ params
-  let m := p.textDocument
-  -- Execute the regular handling of the `didOpen` event
-  handleDidOpen p
-  let fw ← findFileWorker! m.uri
-  -- let s ← get
-  let c ← read
-  let some lvl ← GameServer.getLevelByFileName? c.initParams ((System.Uri.fileUriToPath? m.uri).getD m.uri |>.toString)
-    | do
-      c.hLog.putStr s!"Level not found: {m.uri} {c.initParams.rootUri?}"
-      c.hLog.flush
-  -- Send an extra notification to the file worker to inform it about the level data
-  let s ← get
-  fw.stdin.writeLspNotification {
-    method := "$/game/didOpenLevel"
-    param  := {
-      uri := m.uri
-      gameDir := s.gameDir
-      levelModule := lvl.module
-      tactics := lvl.tactics.tiles
-      lemmas := lvl.lemmas.tiles
-      definitions := lvl.definitions.tiles
-      inventory := s.inventory
-      difficulty := s.difficulty
-      statementName := lvl.statementName
-      : DidOpenLevelParams
-    }
+instance : FromJson InitializeParams where
+  fromJson? j := do
+    let processId? := j.getObjValAs? Int "processId"
+    let clientInfo? := j.getObjValAs? ClientInfo "clientInfo"
+    let rootUri? := j.getObjValAs? String "rootUri"
+    let initializationOptions? := j.getObjValAs? InitializationOptions "initializationOptions"
+    let capabilities ← j.getObjValAs? ClientCapabilities "capabilities"
+    let trace := (j.getObjValAs? Trace "trace").toOption.getD Trace.off
+    let workspaceFolders? := j.getObjValAs? (Array WorkspaceFolder) "workspaceFolders"
+    return ⟨
+      processId?.toOption,
+      clientInfo?.toOption,
+      rootUri?.toOption,
+      initializationOptions?.toOption,
+      capabilities,
+      trace,
+      workspaceFolders?.toOption⟩
+
+def InitializeParams.toLeanInternal (p : InitializeParams) : Lean.Lsp.InitializeParams :=
+{
+  processId? := p.processId?
+  clientInfo? := p.clientInfo?
+  rootUri? := p.rootUri?
+  initializationOptions? := p.initializationOptions?.map fun o => {
+    editDelay? := o.editDelay?
+    hasWidgets? := o.hasWidgets?
   }
-
-partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
-  match ev with
-  | ServerEvent.clientMsg msg =>
-    match msg with
-    | Message.notification "$/game/setInventory" params =>
-      let p := (← parseParams SetInventoryParams (toJson params))
-      let s ← get
-      set {s with inventory := p.inventory, difficulty := p.difficulty}
-      let st ← read
-      let workers ← st.fileWorkersRef.get
-      for (_, fw) in workers do
-        fw.stdin.writeLspMessage msg
-
-      return true
-    | _ => return false
-  | _ => return false
+  capabilities := p.capabilities
+  trace := p.trace
+  workspaceFolders? := p.workspaceFolders?
+}
 
 end Game

server/GameServer/Graph.lean

@@ -18,6 +18,14 @@ instance [ToJson β] : ToJson (Graph Name β) := {
   ]
 }
 
+-- Just a dummy implementation for now:
+instance : FromJson (Graph Name β) := {
+  fromJson? := fun _ => .ok {
+    nodes := {}
+    edges := {}
+  }
+}
+
 instance  : EmptyCollection (Graph α β) := ⟨default⟩
 
 def Graph.insertNode (g : Graph α β) (a : α) (b : β) :=

server/GameServer/SaveData.lean

@@ -22,16 +22,21 @@ def copyImages : IO Unit := do
         let content ← readBinFile file
         writeBinFile outFile content
 
+namespace GameData
+  def gameDataPath : System.FilePath := ".lake" / "gamedata"
+  def gameFileName := s!"game.json"
+  def docFileName := fun (inventoryType : InventoryType) (name : Name) => s!"doc__{inventoryType}__{name}.json"
+  def levelFileName := fun (worldId : Name) (levelId : Nat) => s!"level__{worldId}__{levelId}.json"
+  def inventoryFileName := s!"inventory.json"
+end GameData
 
--- TODO: I'm not sure this should be happening here...
-#eval IO.FS.createDirAll ".lake/gamedata/"
-
+open GameData in
 -- TODO: register all of this as ToJson instance?
 def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
     (inventory : InventoryOverview): CommandElabM Unit := do
   let game ← getCurGame
   let env ← getEnv
-  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
+  let path := (← IO.currentDir) / gameDataPath
 
   if ← path.isDir then
     IO.FS.removeDirAll path
@@ -42,14 +47,32 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
 
   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 / levelFileName worldId levelId) (toString (toJson (level.toInfo env)))
 
-  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
+  IO.FS.writeFile (path / gameFileName) (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))
+      IO.FS.writeFile (path / docFileName inventoryType name) (toString (toJson item))
 
-  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))
+  IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
+
+open GameData
+
+def loadData (f : System.FilePath) (α : Type) [FromJson α] : IO α := do
+  let str ← IO.FS.readFile f
+  let json ← match Json.parse str with
+  | .ok v => pure v
+  | .error e => throw (IO.userError e)
+  let data ← match fromJson? json with
+  | .ok v => pure v
+  | .error e => throw (IO.userError e)
+  return data
+
+def loadGameData (gameDir : System.FilePath) : IO Game :=
+  loadData (gameDir / gameDataPath / gameFileName) Game
+
+def loadLevelData (gameDir : System.FilePath) (worldId : Name) (levelId : Nat) : IO LevelInfo :=
+  loadData (gameDir / gameDataPath / levelFileName worldId levelId) LevelInfo

server/GameServer/Watchdog.lean

@@ -1,158 +0,0 @@
-/- This file is mostly copied from `Lean/Server/Watchdog.lean`. -/
-import Lean.Server.Watchdog
-import GameServer.Game
-
-namespace MyServer.Watchdog
-open Lean
-open Server
-open Watchdog
-open IO
-open Lsp
-open JsonRpc
-open System.Uri
-
-  partial def mainLoop (clientTask : Task ServerEvent) : GameServerM Unit := do
-    let st ← read
-    let workers ← st.fileWorkersRef.get
-    let mut workerTasks := #[]
-    for (_, fw) in workers do
-      if let WorkerState.running := fw.state then
-        workerTasks := workerTasks.push <| fw.commTask.map (ServerEvent.workerEvent fw)
-
-    let ev ← IO.waitAny (clientTask :: workerTasks.toList)
-
-    if ← Game.handleServerEvent ev then -- handle Game requests
-      mainLoop (←runClientTask)
-    else
-      match ev with
-      | ServerEvent.clientMsg msg =>
-        match msg with
-        | Message.request id "shutdown" _ =>
-          shutdown
-          st.hOut.writeLspResponse ⟨id, Json.null⟩
-        | Message.request id method (some params) =>
-          handleRequest id method (toJson params)
-          mainLoop (←runClientTask)
-        | Message.response .. =>
-          -- TODO: handle client responses
-          mainLoop (←runClientTask)
-        | Message.responseError _ _ e .. =>
-          throwServerError s!"Unhandled response error: {e}"
-        | Message.notification method (some params) =>
-          if method == "textDocument/didOpen" then
-            -- for lean4game, we need to pass in extra information when a level is opened:
-            Game.handleDidOpenLevel (← parseParams _ (toJson params))
-          else
-            handleNotification method (toJson params)
-          mainLoop (←runClientTask)
-        | _ => throwServerError "Got invalid JSON-RPC message"
-      | ServerEvent.clientError e => throw e
-      | ServerEvent.workerEvent fw ev =>
-        match ev with
-        | WorkerEvent.ioError e =>
-          throwServerError s!"IO error while processing events for {fw.doc.uri}: {e}"
-        | WorkerEvent.crashed _ =>
-          handleCrash fw.doc.uri #[]
-          mainLoop clientTask
-        | WorkerEvent.terminated =>
-          throwServerError "Internal server error: got termination event for worker that should have been removed"
-        | .importsChanged =>
-          startFileWorker fw.doc
-          mainLoop clientTask
-
-def initAndRunWatchdogAux : GameServerM Unit := do
-  let st ← read
-  try
-    discard $ st.hIn.readLspNotificationAs "initialized" InitializedParams
-    let clientTask ← runClientTask
-    mainLoop clientTask
-  catch err =>
-    shutdown
-    throw err
-  /- NOTE(WN): It looks like instead of sending the `exit` notification,
-  VSCode just closes the stream. In that case, pretend we got an `exit`. -/
-  let Message.notification "exit" none ←
-    try st.hIn.readLspMessage
-    catch _ => pure (Message.notification "exit" none)
-    | throwServerError "Got `shutdown` request, expected an `exit` notification"
-
-def createEnv (gameDir : String) (module : String) : IO Environment := do
-  -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
-  let out ← IO.Process.output
-    { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
-  if out.exitCode != 0 then
-    throwServerError s!"Error while running Lake: {out.stderr}"
-
-  -- Make the paths relative to the current directory
-  let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
-  let currentDir ← IO.currentDir
-  let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
-
-  -- Set the search path
-  Lean.searchPathRef.set paths
-
-  let env ← importModules #[{ module := `Init : Import }, { module := module : Import }] {} 0
-  return env
-
-def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
-  if args.length < 2 then
-    throwServerError s!"Expected 1-3 command line arguments in addition to `--server`:
-      game directory, the name of the main module (optional), and the name of the game (optional)."
-  let gameDir := args[1]!
-  let module := if args.length < 3 then defaultGameModule else args[2]!
-  let gameName := if args.length < 4 then defaultGameName else args[3]!
-  let workerPath := "./gameserver"
-  -- TODO: Do the following commands slow us down?
-  let srcSearchPath ← initSrcSearchPath (← getBuildDir)
-  let references ← IO.mkRef (← loadReferences)
-  let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
-  let i ← maybeTee "wdIn.txt" false i
-  let o ← maybeTee "wdOut.txt" true o
-  let e ← maybeTee "wdErr.txt" true e
-  let state := {
-    env := ← createEnv gameDir module,
-    game := gameName,
-    gameDir := gameDir,
-    inventory := #[]
-    difficulty := 0
-    }
-  let initRequest ← i.readLspRequestAs "initialize" InitializeParams
-  -- We misuse the `rootUri` field to the gameName
-  let rootUri? := gameName
-  let initRequest := {initRequest with param := {initRequest.param with rootUri?}}
-  o.writeLspResponse {
-    id     := initRequest.id
-    result := {
-      capabilities := mkLeanServerCapabilities
-      serverInfo?  := some {
-        name     := "Lean 4 Game Server"
-        version? := "0.1.1"
-      }
-      : InitializeResult
-    }
-  }
-  let context : ServerContext := {
-    hIn            := i
-    hOut           := o
-    hLog           := e
-    args           := args
-    fileWorkersRef := fileWorkersRef
-    initParams     := initRequest.param
-    workerPath
-    srcSearchPath
-    references
-  }
-  discard $ ReaderT.run (StateT.run initAndRunWatchdogAux state) context
-
-def watchdogMain (args : List String) : IO UInt32 := do
-  let i ← IO.getStdin
-  let o ← IO.getStdout
-  let e ← IO.getStderr
-  try
-    initAndRunWatchdog args i o e
-    return 0
-  catch err =>
-    e.putStrLn s!"Watchdog error: {err}"
-    return 1
-
-end MyServer.Watchdog

server/lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
+   "rev": "af7f36db6e7e9e395710a70635f915e8e3a0e69b",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
+   "inputRev": "v4.4.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "GameServer",

server/lean-toolchain

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