From c82a88867f8acc7b38d1eb07e0cd7b9c5451c7e0 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 02:12:09 +0100 Subject: [PATCH] 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: