Merge branch 'main' into dev
This commit is contained in:
Jon Eugster
@@ -10,20 +10,25 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular,
|
||||
* Step 7: [How to Update an existing Game](doc/update_game.md)
|
||||
* Step 8: [How to Publishing a Game](doc/publish_game.md)
|
||||
|
||||
### Publishing a Game
|
||||
|
||||
We encourage anybody to have games hosted on our [Lean Game Server](https://adam.math.hhu.de) for anybody to play. For that you simply need to contact us with the link to your game repo. We are also happy to add work-in-progress games and games in any language.
|
||||
|
||||
For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).
|
||||
|
||||
## Documentation
|
||||
|
||||
The documentation for the game engine itself is still missing, but there is [Creating a Game](doc/create_game.md) explaining the API to create a game.
|
||||
The documentation is very much work in progress but the linked documentation here
|
||||
should be up-to-date:
|
||||
|
||||
Some documentation:
|
||||
### Game creation API
|
||||
|
||||
- [NPM Scripts](doc/npm_scripts.md)
|
||||
- [Old documentation](doc/DOCUMENTATION.md)
|
||||
- [Creating a Game](doc/create_game.md): **the main document to consult**.
|
||||
- [More about Hints](doc/hints.md): describes the `Hint` and `Branch` tactic.
|
||||
|
||||
### Frontend API
|
||||
|
||||
* [How to Run Games Locally](doc/running_locally.md): play a game on your computer
|
||||
* [How to Update an existing Game](doc/update_game.md): update to a new lean version
|
||||
* [How to Publishing a Game](doc/publish_game.md): load your game to adam.math.hhu.de for others to play
|
||||
|
||||
### Backend
|
||||
|
||||
not written yet
|
||||
|
||||
## Contributing
|
||||
|
||||
@@ -37,5 +42,5 @@ Providing the use access to a Lean instance running on the server is a severe se
|
||||
|
||||
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/)
|
||||
of Kevin Buzzard and Mohammad Pedramfar.
|
||||
by Kevin Buzzard and Mohammad Pedramfar.
|
||||
The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
|
||||
|
||||
@@ -1,6 +1,8 @@
|
||||
**NOTE! This document is deprecated! The current documentation is [How To Create A Game](create_game.md)**
|
||||
|
||||
# Creating a game.
|
||||
|
||||
Ideally one takes the [NNG template](https://github.com/hhu-adam/NNG4) to create a new game.
|
||||
Ideally one takes the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new game.
|
||||
|
||||
## Game Structure
|
||||
|
||||
|
||||
+22
-15
@@ -223,25 +223,17 @@ One thing to keep in mind is that the game will look at the main proof to figure
|
||||
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
|
||||
placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands.
|
||||
|
||||
```
|
||||
Hint (strict := true) "some hidden hint"
|
||||
```
|
||||
Read [More about Hints](doc/hints.md) for how they work and what the options are.
|
||||
|
||||
a hint only matches iff the assumptions match exactly one-to-one. (Otherwise, it does not care if there are additional assumptions in context)
|
||||
### 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.
|
||||
|
||||
Further, you can choose to hide hints and only have them displayed when the player presses "More Help":
|
||||
```
|
||||
Hint (hidden := true) "some hidden hint"
|
||||
```
|
||||
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).
|
||||
|
||||
Lastly, you should put variable names in hints inside 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.
|
||||
NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world.
|
||||
|
||||
## 7. Update your game
|
||||
|
||||
@@ -251,6 +243,21 @@ In principle, it is as simple as modifying `lean-toolchain` to update your game
|
||||
|
||||
To publish your game on the official server, see [Publishing a game](doc/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:
|
||||
|
||||
```lean
|
||||
Languages "English"
|
||||
CaptionShort "Game Template"
|
||||
CaptionLong "You should use this game as a template for your own game and add your own levels."
|
||||
Prerequisites "NNG"
|
||||
CoverImage "images/cover.png"
|
||||
```
|
||||
* `Languages`: Currently only a single language (capital English name). The tile will show a corresponding flag.
|
||||
* `CaptionShort`: One catch phrase. 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.
|
||||
|
||||
## Further Notes
|
||||
|
||||
Here are some random further things you should consider designing a new game:
|
||||
|
||||
@@ -0,0 +1,87 @@
|
||||
# Hints
|
||||
|
||||
Most important for game development are probably the "Hints". You can add Hints at any place in your proof using the `Hint` tactic
|
||||
|
||||
```
|
||||
Statement .... := by
|
||||
Hint "Hint to show at the start"
|
||||
rw [h]
|
||||
Hint "some tip after using rw"
|
||||
...
|
||||
```
|
||||
|
||||
## 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
|
||||
sample solutions and the entire context from the sample solutions is present in the
|
||||
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
|
||||
all of them.
|
||||
|
||||
However, identical (non-hidden) hints which where already present in the step
|
||||
before are omitted. This is to allow a player to add new assumptions to context, for example
|
||||
with `have`, without seeing the same hint over and over again.
|
||||
Hidden hints are not filtered.
|
||||
|
||||
## 2. Alternative Proofs / `Branch`
|
||||
|
||||
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
|
||||
so that no progress has been made on proofing the goal.
|
||||
|
||||
```
|
||||
Statement .... := by
|
||||
Hint "Huse `rw` or `rewrite`."
|
||||
Branch
|
||||
rewrite [h]
|
||||
Hint "now you still need `rfl`"
|
||||
rw [h]
|
||||
```
|
||||
|
||||
## 3. Variables names
|
||||
|
||||
Put variables in the hint text inside brackets like this: `{h}`! This way the server can replace
|
||||
the variable's name with the one the user actually used.
|
||||
|
||||
For example, if the sample proof contains
|
||||
|
||||
```
|
||||
have h : True := trivial
|
||||
Hint "Now use `rw [{h}]` to use your assumption `{h}`."
|
||||
```
|
||||
|
||||
but the player writes `have g : True := trivial`, they will see a hint saying
|
||||
"Now use `rw [g]` to use your assumption `g`."
|
||||
|
||||
## 4. Hidden hints
|
||||
|
||||
Some hints can be hidden, and only show after the user clicks on a button to get additional
|
||||
help. You mark a hint as hidden with `(hidden := true)`:
|
||||
|
||||
```
|
||||
Hint (hidden := true) "some hidden hint"
|
||||
```
|
||||
|
||||
## 5. Strict context matching
|
||||
|
||||
If you use the attribute `(strict := true)` a hint is only shown if the entire context
|
||||
matches exactly the one where the hint is placed. With `(hint := false)`, which is the default,
|
||||
it does not matter if additional assumptions are present in the player's context.
|
||||
|
||||
```
|
||||
Hint (strict := true) "now use `have` to create a new assumption."
|
||||
```
|
||||
|
||||
You should probably use `(strict := true)` if you want to give fine-grained details about
|
||||
tactics like `have` which do not modify the goal or any existing assumptions, but only
|
||||
create new assumptions.
|
||||
|
||||
## 6. Formatting
|
||||
|
||||
You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$`
|
||||
|
||||
TODO: Write a doc about latex/markdown options available.
|
||||
@@ -28,3 +28,5 @@ Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITOR
|
||||
|
||||
Adding games to the main page happens manually by the server maintainers. Tell us if you want us
|
||||
to add a tile for your game!
|
||||
|
||||
For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).
|
||||
|
||||
Reference in New Issue
Block a user