$/game/setInventory no longer needed

README.md

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

doc/DOCUMENTATION.md

@@ -1,67 +1,335 @@
-# Server
+**NOTE! This document is deprecated! The current documentation is [How To Create A Game](create_game.md)**
 
-The server is made out of two parts, named "relay" and "server".
+# Creating a 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.
+Ideally one takes the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new game.
 
-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`.
+## Game Structure
 
+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.
 
-## Integration into Games
+### Level
 
-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
+A level file is a lean file that imports at least `import GameServer.Commands` and starts with the following Lean commands.
 
+```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 way any changes to files in `client/` or `relay/` will cause the server to restart automatically.
+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.
 
-Alternative, you can run `npm run build` followed by the commands
+### Modifying the GameServer
 
+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
 ```
-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.
+This causes lake to search locally for the `GameServer` lake package instead of using the version from github.

doc/create_game.md

@@ -129,9 +129,6 @@ 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.
@@ -185,8 +182,6 @@ 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.
@@ -235,7 +230,7 @@ Read [More about Hints](doc/hints.md) for how they work and what the options are
 ### 6. e) Extra: Images
 You can add images on any layer of the game (i.e. game/world/level). These will be displayed in your game.
 
-The images need to be placed in `images/` and you need to add a command like `Image "images/path/to/myWorldImage.png"`
+The images need to be placed in `images/` and you need to add a command like `Image "images/path/to/myWorldImage.png"` 
 in one of the files you created in 2), 3), or 4) (i.e. game/world/level).
 
 NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world.

doc/hints.md

@@ -10,8 +10,6 @@ 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/troubleshoot.md

@@ -1,23 +0,0 @@
-# Troubleshooting
-
-Here are some issues experienced by users.
-
-# VSCode Dev-Container
-* 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.
-
-
-# Manual Installation
-Here are known issues/pitfalls with the local setup using `npm`.
-
-* If `CDPATH` is set on your mac/linux system, it might provide issues with `npm start` resulting in a server crash or blank screen. In particular `npm start` will display
-  ```
-  [server] sh: line 0: cd: server: No such file or directory
-  [server] npm run start_server exited with code 1
-  ```
-  As a fix you might need to delete your manually set `CDPATH` environment variable.

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 (without Cache!).
-* **Local Setup**: in your game's folder run the following:
+* Dev Container: Rebuild the VSCode Devcontainer.
+* 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.
 

relay/unpack.sh

@@ -28,7 +28,3 @@ 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/FileWorker.lean

@@ -489,8 +489,6 @@ section Initialization
     return (ctx,
     { doc             := doc
       initHeaderStx   := headerStx
-      currHeaderStx      := headerStx
-      importCachingTask? := none
       pendingRequests := RBMap.empty
       rpcSessions     := RBMap.empty
     })

server/lake-manifest.json

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

server/lean-toolchain

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