phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

documentation

Browse Source
This commit is contained in:
joneugster
2023-10-17 02:06:32 +02:00
parent 556c072cef
commit 19592668ae
5 changed files with 403 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files
doc/DOCUMENTATION.md
+332
View File
@@ -0,0 +1,332 @@
# Creating a game.
Ideally one takes the [NNG template](https://github.com/hhu-adam/NNG4) to create a new game.
## 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.
### Level
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 consequtive 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 alternativ 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 explicitely 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).
Explicitely 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
explicitely 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
```
If you are developing a game other than `Robo` or `NNG4`, adapt the
code at the beginning of `lean4game/server/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.
### 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
```
This causes lake to search locally for the `GameServer` lake package instead of using the version from github.
doc/create_game.md
+255
View File
@@ -0,0 +1,255 @@
# Creating a new game
This tutorial walks you through creating a new game for lean4. It covers from writing new levels, over testing the game locally, to publishing the game online.
## 1. Create the project
1. Use the [NNG template](https://github.com/hhu-adam/NNG4) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
2. Clone the game repo.
3. Call `lake update && lake exe cache get && lake build` to build the Lean project.
Note that you need to host your game's code on github to publish it online later on. If you only
want to play it locally, you can simply clone the NNG repo and start modifying that one.
## 2. Game.lean
The file `Game.lean` is the backbone of the game putting everything together.
1. `MakeGame`: This command is where the game gets built. If there are things to fix, they will be shown here as warnings or errors (orange/red squigglies in VSCode). Note that you might have to call "Lean: Restart File" (Ctrl+Shift+X) to reload the file and see changes made in other files.
1. `Title`: Set the display title of your game.
1. `Ìntroduction`: This is the text displayed at the beggining next to the world selection tree.
1. `Info`: This will be displayed in the game's menu as "Game Info". Use it for credits, funding and other meta information about the game.
1. Imports: The file needs to import all world files, which we look at in a second. If you add a new world, remember to import it here!
1. `Dependency`: (optional) This command adds another edge in the world tree. The game computes them automatically based on used tactics/theorems. However, sometimes you need a dependency the game can't compute, for example you explained `≠` in one world and in another world, the user is expected to know it already. The syntax is `Dependency World₁ → World₂ → World₃`.
So the `Game.lean` has the following structure:
```lean
import GameServer.Commands
-- import all worlds
import Game.Levels.Tutorial
Title "My Game"
Introduction "
Hi, nice you're here! Click on a world to start.
"
Info "
This game has been developed by me.
"
-- Dependency World₁ → World₂ -- because of `≠`
MakeGame
```
## 3. Creating a Level
In this tutorial we first learn about Levels. A game consists of a tree of worlds, each world has
a number of levels, enumerated 1 to n. Here we create level 1 of a world `MyWorld`. We add this world to the game in the next section.
A minimal level file looks like the following. There are many options to add, which we will dive
into in a later section
```lean
import GameServer.Commands
World "MyWorld"
Level 1
Title "Hello World"
Introduction "
A message shown at the beginning of the level. Use it to explain any new concepts.
"
/-- The exercise statement in natural language using latex: $\iff$. -/
Statement (n : Nat) : 0 + n = n := by
sorry
Conclusion "
The message shown when the level is completed
"
```
1. Create a folder `Game/Levels/MyWorld`
1. Create a file `Game/Levels/MyWorld/L01_hello.lean`
1. Copy the above inside your first level.
## 4. Creating a World
Now we create a world. For that we create a file `MyWorld.lean` that imports all levels of this world:
```lean
import Game.Levels.MyWorld.L01_hello
World "MyWorld"
Title "My First World"
Introduction
"
This introduction text is shown when one first enters a world.
"
```
1. Create a file `Game/Levels/MyWorld.lean`
1. Use the template above and make sure you import all levels of this world.
1. In `Game.lean` import the world with `import Game.Levels.MyWorld`
Now you created a world with one level and added it🎉 The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently it shows
```text
No world introducing sorry, but required by MyWorld
```
which means that the world `MyWorld` uses the tactic `sorry` in a proof, but `sorry` has not been
introduced anywhere.
## 5. Testing the Game Locally
Now it's time to test the game locally and play it.
There are multiple ways how you can start the game locally to test-play it described at [How to Run the Game Locally](running_locally.md). If you have problems getting one of the setups to work, please get in contact!
## 6. Dive into Level creation
Now that you have a running game, we have a closer look at the level files and all the options
you have to design your game.
### 6. a) Inventory
The player has an inventory with tactics, theorems, and definitions that unlock during the game. You can unlock/introduce such items in a Level by adding one of the following below the `Statement`.
```lean
NewTactic induction simp
NewLemma Nat.zero_mul
NewDefinition Pow
```
#### 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.
```lean
LemmaDoc Nat.zero_mul as "zero_mul" in "Mul"
"some description"
TacticDoc simp
"some description"
DefinitionDoc Pow as "^"
"some description"
```
(e.g. you could also create a file `Game/Doc/MyTheorems.lean`, add there your documentation and import it)
If you do not provide any content for the inventory, the game will try to find a docstring of that item and display that docstring.
#### Inventory management
You have a few options to disable inventory items that have been unlocked in previous levels:
```lean
DisableTactic, DisableLemma, OnlyTactic, OnlyLemma
```
have the same syntax as above. The former two disable items for this level, the latter two
disable all items except the ones specified.
#### Theorem Tab
Theorems are sorted into tabs. with `LemmaTab "Mul"` you specify which tab should be open by default in this level.
#### HiddenTactic
`NewHiddenTactic` lets you add a tactic without adding it to the inventory. This can be useful for variants of tactics. E.g. you could do
```lean
NewTactic rw
NewHiddenTactic rewrite nth_rewrite rwa
```
and only `rw` would show up in the inventory.
### 6. b) Statement
The statement is the exercise of the level. the basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax
#### Name
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.
#### 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.
```lean
/-- The exercise statement in natural language using latex: $\iff$. -/
Statement ...
sorry
```
#### Attributes
You can add attributes as you would for a `theorem`. Most notably, you can make your named exercise a `simp` lemma:
```lean
@[simp]
Statement my_simp_lemma ...
```
### 6. c) 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 alternativ 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.
One thing to keep in mind is that the game will look at the main proof to figure out which tactics and theorems are needed, but it ignores any `Branch`es.
### 6. d) Hints
Most important for game development are probably the `Hints`.
The hints will be displayed whenever the player's current goal matches the goal the hint is
placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands. If you specify
```
Hint (strict := true) "some hidden hint"
```
a hint only matches iff the assumptions match exactly one-to-one. (Otherwise, it does not care if there are additional assumptions in context)
Further, you can choose to hide hints and only have them displayed when the player presses "More Help":
```
Hint (hidden := true) "some hidden hint"
```
Lastly, you should put variable names in hints insid brackets:
```
Hint "now use `rw [{h}]` to use your assumption {h}."
```
That way, the game will replace it with the actual name the assumption has in the player's proof state.
## Further Notes
Here are some random further things you should consider designing a new game:
* Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you
would write `Introduction "some latex here: $\\iff$."` but
`/-- some latex here: $\iff$. -/ Statement ...`
* 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 starts getting out
of control.
doc/npm_scripts.md
+9
View File
@@ -0,0 +1,9 @@
## NPM Scripts
* `npm start`: Start the project in development mode. The browser will automatically reload when client files get changed. The Lean server will get recompiled and restarted when lean files get changed. The Lean server will be started without a container. The client and server can be started separately using the scripts `npm run start_client` and `npm run start_server`. The project can be accessed via `http://localhost:3000`.
Internally, websocket requests to `ws://localhost:3000/websockets` will be forwarded to a Lean server running on port `8080`.
* `npm run build`: Build the project in production mode. All assets of the client will be compiled into `client/dist`.
On the server side, the command will set up a docker image containing the Lean server. The two parts can be built separately using `npm run build_client` and `npm run build_server`.
* `npm run production`: Start the project in production mode. This requires that the build script has been run. It will start a server on the port specified in the `PORT` environment variable or by default on `8080`. You can run on a specifiv port by running `PORT=80 npm run production`. The server will serve the files in `client/dist` via http and give access to the bubblewrapped Lean server via the web socket protocol.
doc/running_locally.md
+121
View File
@@ -0,0 +1,121 @@
# Running Games Locally
The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
There are several options to play a game locally:
- VSCode Dev Container: needs `docker` installed on your machine
- Codespaces: Needs active internet connection and computing time is limited.
- Gitpod: does not work yet (I that true?)
- Manual installation: Needs `npm` installed on your system
The recommended option is "VSCode Dev containers" but you may choose any option above depending on your setup.
## VSCode Dev Containers
1. **Install Docker and Dev Containers** *(once)*:<br/>
See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
Explicitely 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). (Alternatively install it from the VSCode extensions).
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, you can open http://localhost:3000 in your browser. which should load the game
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)
## 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".
Note: You have to wait until npm started properly. In particular, this is after a message like `[client] webpack 5.81.0 compiled successfully in 38119 ms` appears in the terminal, which might take a good while.
As with devcontainers, you need to run `lake build` after changing any lean files and then reload the browser.
## Gitpod
TODO: Not sure this works yet!
Open the game clicking on the gitpod link. Again you will need to wait until it is fully built and then enter `lake build` in the shell whenever you made changes.
## Manual installation
This installs the `lean4game` manually on your computer. (It is the same installation as one would
use to setup a proper server online, only the run command (i.e. `npm start`) is different.)
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
```
Run the game:
```bash
npm start
```
This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/NNG4. Replace `NNG4` with the folder name of your local game.
## Modifying the GameServer
When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by setting `export 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. Therefore, when you `lake build` your game, it will rebuild with the modified `GameServer`.