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).