From 2e1a35ecd0b0d4e3946cb70e6b3052843c4253d9 Mon Sep 17 00:00:00 2001 From: Jad Date: Sat, 13 Jul 2024 20:38:50 +0300 Subject: [PATCH 1/3] Latex Doc improvements --- doc/create_game.md | 16 +++++----------- doc/hints.md | 16 ++++++++++++++++ doc/latex.md | 8 ++++++++ 3 files changed, 29 insertions(+), 11 deletions(-) create mode 100644 doc/latex.md diff --git a/doc/create_game.md b/doc/create_game.md index 8d2c3f79..cb5c0c42 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -194,7 +194,7 @@ You can but a `Statement` inside namespaces like you would with `theorem`. #### Doc String / Exercise statement -Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports Latex. +Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports KateX. ```lean /-- The exercise statement in natural language using latex: $\iff$. -/ @@ -265,13 +265,7 @@ CoverImage "images/cover.png" * `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: - -* Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you - would write `Introduction "some latex here: $\\iff$."` but - `/-- some latex here: $\iff$. -/ Statement ...` -* A world with more than 16 levels will be displayed with the levels spiraling outwards, - it might be desirable to stay below that bound. Above 22 levels the spiral starts getting out - of control. +## Number Of Levels Limit +A world with more than 16 levels will be displayed with the levels spiraling outwards, +it might be desirable to stay below that bound. Above 22 levels the spiral starts getting out +of control. diff --git a/doc/hints.md b/doc/hints.md index 87bc7d98..bc1f2991 100644 --- a/doc/hints.md +++ b/doc/hints.md @@ -120,3 +120,19 @@ $$ ``` See https://www.jmilne.org/not/Mamscd.pdf + +### Truth Tables +KateX does not support the tabular environment. You can use the array environment instead. +``` +$$ +\\begin{array}{|c|c|} +\\hline +P & ¬P \\\\ +\\hline +T & F \\\\ +F & T \\\\ +\\hline +\\end{array} +$$ +``` + diff --git a/doc/latex.md b/doc/latex.md new file mode 100644 index 00000000..cb191a4d --- /dev/null +++ b/doc/latex.md @@ -0,0 +1,8 @@ +# Syntax +Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you + would write `Introduction "some latex here: $\\iff$."` but + `/-- some latex here: $\iff$. -/ Statement ...` + +# Support +It is important to mention that KateX supports most but not all of latex and its packages. +See [supported](https://katex.org/docs/supported.html). From 8a61ad6e5d5277495c8319fb96b42ca32c2cf2ff Mon Sep 17 00:00:00 2001 From: Jad Date: Sat, 13 Jul 2024 20:58:08 +0300 Subject: [PATCH 2/3] trying to centralize information --- doc/hints.md | 9 --------- doc/latex.md | 15 +++++++++++++-- doc/writing_exercises.md | 5 +++++ 3 files changed, 18 insertions(+), 11 deletions(-) diff --git a/doc/hints.md b/doc/hints.md index bc1f2991..cb885504 100644 --- a/doc/hints.md +++ b/doc/hints.md @@ -82,16 +82,7 @@ You should probably use `(strict := true)` if you want to give fine-grained deta 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$` - -**Escaping**: Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape -backslashes, but if you provide text inside a doc comment -`/-- -/` (e.g. in the `Statement` description) you do not! -Further, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`. - -TODO: Write a doc about latex/markdown options available. ### Commutative diagrams diff --git a/doc/latex.md b/doc/latex.md index cb191a4d..5e892dd5 100644 --- a/doc/latex.md +++ b/doc/latex.md @@ -1,8 +1,19 @@ -# Syntax +# Escaping +Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape +backslashes, but if you provide text inside a doc comment +`/-- -/` (e.g. in the `Statement` description) you do not! + +Furthermore, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`. + +## Example Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you - would write `Introduction "some latex here: $\\iff$."` but + would write `Introduction "some latex here: $\\iff$."` , but `/-- some latex here: $\iff$. -/ Statement ...` # Support It is important to mention that KateX supports most but not all of latex and its packages. See [supported](https://katex.org/docs/supported.html). + + + + diff --git a/doc/writing_exercises.md b/doc/writing_exercises.md index 8d8483e0..c3d85c57 100644 --- a/doc/writing_exercises.md +++ b/doc/writing_exercises.md @@ -54,3 +54,8 @@ You can add attributes as you would for a `theorem`. Most notably, you can make @[simp] Statement my_simp_lemma ... ``` + +## Formatting + +You can use markdown to format inside quotes like `Hint ""`. +Latex is also supported, see latex.md. From f0132b86424ff6f3a4be787061faa710e8e0df6c Mon Sep 17 00:00:00 2001 From: Jad Date: Sun, 14 Jul 2024 10:44:41 +0300 Subject: [PATCH 3/3] Adding link --- doc/create_game.md | 6 +++++- doc/latex.md | 4 ---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/create_game.md b/doc/create_game.md index cb5c0c42..3b562d99 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -265,7 +265,11 @@ CoverImage "images/cover.png" * `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. -## Number Of Levels Limit +## 10. Advanced Topics +### Number Of Levels Limit A world with more than 16 levels will be displayed with the levels spiraling outwards, it might be desirable to stay below that bound. Above 22 levels the spiral starts getting out of control. + +### Latex support +See latex.md diff --git a/doc/latex.md b/doc/latex.md index 5e892dd5..aedf081b 100644 --- a/doc/latex.md +++ b/doc/latex.md @@ -13,7 +13,3 @@ Inside strings, you need to escape backslashes, but not inside doc-strings, ther # Support It is important to mention that KateX supports most but not all of latex and its packages. See [supported](https://katex.org/docs/supported.html). - - - -