From 8b43aed596436888805c0d8e2de5f20643a72edc Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 01:57:47 +0100 Subject: [PATCH 1/5] Update publish_game.md --- doc/publish_game.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/doc/publish_game.md b/doc/publish_game.md index 684f5d6..141c87d 100644 --- a/doc/publish_game.md +++ b/doc/publish_game.md @@ -26,5 +26,4 @@ Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITOR ## 4. Main page -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! +Adding games to the main page happens manually by the server maintainers. Tell us if youwould like your game to appear on the start page. From c82a88867f8acc7b38d1eb07e0cd7b9c5451c7e0 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 02:12:09 +0100 Subject: [PATCH 2/5] Update create_game.md --- doc/create_game.md | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/doc/create_game.md b/doc/create_game.md index 0bf24d1..b4b98ca 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -243,6 +243,14 @@ 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. +### 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"` +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. + ## 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). @@ -251,6 +259,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: From e02e73c1c0bddaf3c2156ba8f00ae0ab5d7f47dc Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 02:17:30 +0100 Subject: [PATCH 3/5] Update DOCUMENTATION.md --- doc/DOCUMENTATION.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/DOCUMENTATION.md b/doc/DOCUMENTATION.md index 2cd8725..2ff0ab7 100644 --- a/doc/DOCUMENTATION.md +++ b/doc/DOCUMENTATION.md @@ -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 From bedb2ad5ec0099c3594fca7c69dd4a830735b5ae Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 02:22:10 +0100 Subject: [PATCH 4/5] Update README.md --- README.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 5ee0d7f..31c4f17 100644 --- a/README.md +++ b/README.md @@ -12,15 +12,17 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular, ### 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. +We encourage anybody to have games hosted on our [Lean Game Server](https://adam.math.hhu.de) for anybody to play. + +You can simply load your game to this server yourself following [How to Publishing a Game](doc/publish_game.md). However, to be featured on the server's starting page, you will need to reach out to be added manually. 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 main documentation is [Creating a Game](doc/create_game.md) which explains the API to a user who wants to create a game. -Some documentation: +Some random documentation: - [NPM Scripts](doc/npm_scripts.md) - [Old documentation](doc/DOCUMENTATION.md) @@ -37,5 +39,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). From 63cf5e8b72adb3d60a0382bc2f3a33fcaffbbb1d Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 9 Dec 2023 22:09:05 +0100 Subject: [PATCH 5/5] update docs --- README.md | 21 ++++++----- doc/create_game.md | 20 ++--------- doc/hints.md | 87 +++++++++++++++++++++++++++++++++++++++++++++ doc/publish_game.md | 5 ++- 4 files changed, 105 insertions(+), 28 deletions(-) create mode 100644 doc/hints.md diff --git a/README.md b/README.md index 31c4f17..b5a610a 100644 --- a/README.md +++ b/README.md @@ -10,22 +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 +## Documentation -We encourage anybody to have games hosted on our [Lean Game Server](https://adam.math.hhu.de) for anybody to play. +The documentation is very much work in progress but the linked documentation here +should be up-to-date: -You can simply load your game to this server yourself following [How to Publishing a Game](doc/publish_game.md). However, to be featured on the server's starting page, you will need to reach out to be added manually. +### Game creation API -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). +- [Creating a Game](doc/create_game.md): **the main document to consult**. +- [More about Hints](doc/hints.md): describes the `Hint` and `Branch` tactic. -## Documentation +### Frontend API -The main documentation is [Creating a Game](doc/create_game.md) which explains the API to a user who wants to create a game. +* [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 -Some random documentation: +### Backend -- [NPM Scripts](doc/npm_scripts.md) -- [Old documentation](doc/DOCUMENTATION.md) +not written yet ## Contributing diff --git a/doc/create_game.md b/doc/create_game.md index b4b98ca..303962e 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -223,25 +223,9 @@ 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" -``` - -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 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. +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. diff --git a/doc/hints.md b/doc/hints.md new file mode 100644 index 0000000..f980695 --- /dev/null +++ b/doc/hints.md @@ -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. diff --git a/doc/publish_game.md b/doc/publish_game.md index 141c87d..1afd3d9 100644 --- a/doc/publish_game.md +++ b/doc/publish_game.md @@ -26,4 +26,7 @@ Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITOR ## 4. Main page -Adding games to the main page happens manually by the server maintainers. Tell us if youwould like your game to appear on the start page. +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).