diff --git a/README.md b/README.md index 5ee0d7f..b5a610a 100644 --- a/README.md +++ b/README.md @@ -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 +## Documentation -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. +The documentation is very much work in progress but the linked documentation here +should be up-to-date: -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). +### Game creation API -## Documentation +- [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 -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. +* [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 documentation: +### Backend -- [NPM Scripts](doc/npm_scripts.md) -- [Old documentation](doc/DOCUMENTATION.md) +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). 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 diff --git a/doc/create_game.md b/doc/create_game.md index 0bf24d1..303962e 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -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: 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 684f5d6..1afd3d9 100644 --- a/doc/publish_game.md +++ b/doc/publish_game.md @@ -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).