diff --git a/.vscode/ltex.dictionary.en-US.txt b/.vscode/ltex.dictionary.en-US.txt new file mode 100644 index 0000000..c1cff73 --- /dev/null +++ b/.vscode/ltex.dictionary.en-US.txt @@ -0,0 +1,7 @@ +GameSkeleton +HiddenTactic +subgoals +KaTex +gameserver +lakefile +Zulip diff --git a/doc/DOCUMENTATION.md b/doc/DOCUMENTATION.md index 2364920..153756d 100644 --- a/doc/DOCUMENTATION.md +++ b/doc/DOCUMENTATION.md @@ -8,7 +8,7 @@ relays messages between the lean server and the client. `index.mjs` is the file be run, which is done for example using `pm2` or by calling `npm run start_server` or `npm run production`, see more later. -The latter, "server", is the lean server which has two jobs. For one it produces the "gameserver" +The latter, "server", is the lean server which has two jobs. For one, it produces the "gameserver" executable which is the lean server that handles the files the player plays on. The second job is to provide the lean commands which are used when creating a game. These are located in `Commands.lean`. @@ -27,7 +27,7 @@ saved to lean env-extensions which the lean server has access to after loading t For games to be run successfully, it is important that the "gameserver" executable inside the game's `.lake` folder is actually built. -Currently this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`. +Currently, this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`. (both commands are to be executed in the game's directory!) ## Modifying the server @@ -50,7 +50,7 @@ npm run start_client npm run production ``` -(in two separate terminals) to test the production modus of the server. This way it will only +(in two separate terminals) to test the production modes of the server. This way it will only change once you build and restart the server. ### Modifying the lean server diff --git a/doc/create_game.md b/doc/create_game.md index e3caf07..0fc347f 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -221,7 +221,7 @@ There are a few extra tactics that help you with structuring the proof: - `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches the one where `Hint` is placed. For more options about hints, see below. - `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which - helps setting `Hints` in different places. The `Branch` does not affect the main + helps to set `Hints` in different places. The `Branch` does not affect the main proof and does not need to finish any goals. - `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template` will be copied into the editor with all `Hole`s replaced with `sorry`. Note that @@ -264,7 +264,7 @@ 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. +* `CaptionShort`: One catchphrase. 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. diff --git a/doc/hints.md b/doc/hints.md index 591edb1..9e3a937 100644 --- a/doc/hints.md +++ b/doc/hints.md @@ -10,7 +10,7 @@ Statement .... := by ... ``` -Note that hints are only **context-aware but not history-aware**. In particular they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps placing hints outside the sample solution's proof. +Note that hints are only **context-aware but not history-aware**. In particular, they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps to place hints outside the sample solution's proof. ## 1. When do hints show? @@ -19,7 +19,7 @@ sample solutions and the entire context from the sample solutions is present in 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 +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 @@ -32,12 +32,12 @@ Hidden hints are not filtered. 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 +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`." + Hint "use `rw` or `rewrite`." Branch rewrite [h] Hint "now you still need `rfl`" diff --git a/doc/publish_game.md b/doc/publish_game.md index 368d299..bd017fe 100644 --- a/doc/publish_game.md +++ b/doc/publish_game.md @@ -11,7 +11,7 @@ tab. ## 2. Import the game -You call the URL that's listed under "What's Next?" in the latest action run. Explicitely you call +You call the URL that's listed under "What's Next?" in the latest action run. Explicitly you call the URL of the form > adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY} diff --git a/doc/server.md b/doc/server.md index e706e47..509c902 100644 --- a/doc/server.md +++ b/doc/server.md @@ -22,7 +22,7 @@ where you replace: > https://{website}/#/g/{owner}/{repo} -## data management +## Data management Everything downloaded remains in the folder `lean4game/games`. The subfolder `tmp` contains downloaded artifacts and can be deleted without loss. The other folders should only contain the built lean-games, sorted by owner and repo.