@ -8,7 +8,7 @@ relays messages between the lean server and the client. `index.mjs` is the file
be run, which is done for example using `pm2` or by calling `npm run start_server` or
`npm run production`, see more later.
The latter, "server", is the lean server which has two jobs. For one it produces the "gameserver"
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`.
@ -27,7 +27,7 @@ saved to lean env-extensions which the lean server has access to after loading t
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`.
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
@ -50,7 +50,7 @@ npm run start_client
npm run production
```
(in two separate terminals) to test the production modus of the server. This way it will only
(in two separate terminals) to test the production mode of the server. This way it will only
@ -98,7 +98,7 @@ This introduction text is shown when one first enters a world.
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
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
@ -125,26 +125,32 @@ The player has an inventory with tactics, theorems, and definitions that unlock
```lean
NewTactic induction simp
NewLemma Nat.zero_mul
NewTheorem 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`.
to be **fully qualified**. For example `NewTheorem Nat.zero_mul` and not `NewTheorem 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.
You'll see a warning about a missing Theorem 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"
/--
some description
-/
TheoremDoc Nat.zero_mul as "zero_mul" in "Mul"
/--
some description
-/
TacticDoc simp
"some description"
/--
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)
@ -156,7 +162,7 @@ If you do not provide any content for the inventory, the game will try to find a
You have a few options to disable inventory items that have been unlocked in previous levels:
have the same syntax as above. The former two disable items for this level, the latter two
@ -164,7 +170,7 @@ 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.
Theorems are sorted into tabs. With `TheoremTab "Mul"` you specify which tab should be open by default in this level.
#### HiddenTactic
@ -179,7 +185,7 @@ 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
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
@ -210,12 +216,12 @@ Statement my_simp_lemma ...
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:
There are a few extra tactics that help you with 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
helps to set `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
@ -230,7 +236,7 @@ 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.
Read [More about Hints](doc/hints.md) for how they work and what the options are.
Read [More about Hints](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.
@ -242,11 +248,11 @@ NOTE: At present, only the images for a world are displayed. They appear in the
## 7. Update your game
In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](doc/update_game.md).
In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](update_game.md).
## 8. Publish your game
To publish your game on the official server, see [Publishing a game](doc/publish_game.md)
To publish your game on the official server, see [Publishing a game](publish_game.md)
There are a few more options you can add in `Game.lean` before the `MakeGame` command, which describe the tile that is visible on the server's landing page:
@ -258,7 +264,7 @@ Prerequisites "NNG"
CoverImage "images/cover.png"
```
* `Languages`: Currently only a single language (capital English name). The tile will show a corresponding flag.
* `CaptionShort`: One catchphrase. Appears above the image.
* `CaptionShort`: One catchphrase. Appears above the image.
* `CaptionLong`: 2-4 sentences to describe the game.
* `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text.
* `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens.
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.
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 to place hints outside the sample solution's proof.
## 1. When do hints show?
@ -19,7 +19,7 @@ sample solutions and the entire context from the sample solutions is present in
player's context. The player's context may contain additional items.
This means if you have multiple identical
subgoals, you should only place a single hint in one of them and it will be displayed in
subgoals, you should only place a single hint in one of them, and it will be displayed in
all of them.
However, identical (non-hidden) hints which where already present in the step
@ -32,12 +32,12 @@ Hidden hints are not filtered.
You can use `Branch` to place hints
in dead ends or alternative proof strands.
A proof inside a `Branch`-block is normally evaluated by lean but it's discarded at the end
A proof inside a `Branch`-block is normally evaluated by lean, but it's discarded at the end
so that no progress has been made on proofing the goal.
The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
Please also consult the [Troubleshooting Collection](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
@ -31,24 +33,14 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta
* The first start will take a while, ca. 2-15 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.
* 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)
* 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".
You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). 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, which might take a good while.
@ -108,6 +100,29 @@ Run the game:
npm start
```
You should see a message like this:
```bash
[server] > lean4-game@0.1.0 start_server
[server] > (cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec "node ./index.mjs")
[server]
[client]
[client] > lean4-game@0.1.0 start_client
[client] > cross-env NODE_ENV=development vite --host
[client]
[server] [nodemon] 3.0.#
[server] [nodemon] to restart at any time, enter `rs`
[server] (node:#####) [DEP0040] [server] Listening on 8080
```
This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/GameSkeleton. Replace `GameSkeleton` with the folder name of your local game.
* 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)
* 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.
# Publication
Errors concerning uploads to the server.
* Your game overview loads but the server crashes on loading a level: Check your game's github action is identical to the [GameSkeleton's](https://github.com/hhu-adam/GameSkeleton/blob/main/.github/workflows/build.yml), in particular that there is a step about building the "`gameserver`-executable".
Jon Eugster
1 year ago