Merge branch 'v4.4.0'

bump to v4.4.0
Update update_game.md
2023-12-25 12:01:49 +01:00 · 2023-12-22 13:28:49 +01:00 · 2023-12-18 16:20:26 +01:00 · 2023-12-15 00:04:54 +01:00 · 2023-12-11 16:04:37 +01:00 · 2023-12-09 23:38:18 +01:00
8 changed files with 77 additions and 333 deletions
@@ -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.
+by Kevin Buzzard and Mohammad Pedramfar, and on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
 The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
@@ -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/
+This way any changes to files in `client/` or `relay/` will cause the server to restart automatically.
 and the game is available on http://localhost:3000/#/g/hhu-adam/NNG4.
-### 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.
@@ -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.
@@ -230,7 +235,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.
@@ -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
@@ -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.
+* **Dev Container**: Rebuild the VSCode Devcontainer (without Cache!).
-* Local Setup: in your game's folder run the following:
+* **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.
@@ -489,6 +489,8 @@ section Initialization
    return (ctx,
    { doc             := doc
      initHeaderStx   := headerStx
      currHeaderStx      := headerStx
      importCachingTask? := none
      pendingRequests := RBMap.empty
      rpcSessions     := RBMap.empty
    })
@@ -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",
@@ -1 +1 @@
-leanprover/lean4:v4.3.0
+leanprover/lean4:v4.4.0
Author	SHA1	Message	Date
Jon Eugster	e579071a3b	Merge branch 'v4.4.0'	2023-12-25 12:01:49 +01:00
Jon Eugster	8cdac88b5a	bump to v4.4.0	2023-12-22 13:28:49 +01:00
Jon Eugster	7882958f54	Update update_game.md	2023-12-18 16:20:26 +01:00
Jon Eugster	c4f4dbdc6b	update doc #171	2023-12-15 00:04:54 +01:00
Jon Eugster	5f52e23f29	Update hints.md	2023-12-11 16:04:37 +01:00
Jon Eugster	b067dea6e7	Update README.md	2023-12-09 23:38:18 +01:00
Jon Eugster	4edf67f0d6	Update README.md	2023-12-09 23:37:59 +01:00
Jon Eugster	004f81835f	write more docs	2023-12-09 23:34:39 +01:00
`@@ -1 +1 @@`
	`leanprover/lean4:v4.3.0`	`leanprover/lean4:v4.4.0`