From 8c5e47dd7b1d86ef562ffbd06bddec7ec9f70957 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 31 Jul 2024 17:13:24 +0200 Subject: [PATCH] improve doc, adaptation of #250 Co-authored-by: JadAbouHawili --- doc/create_game.md | 22 ++++++++----- doc/hints.md | 41 +++++++----------------- doc/latex.md | 78 ++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 105 insertions(+), 36 deletions(-) create mode 100644 doc/latex.md diff --git a/doc/create_game.md b/doc/create_game.md index 8d2c3f79..1a68ceb7 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. See [LaTeX in Games](latex.md) for more details on formatting. ```lean /-- The exercise statement in natural language using latex: $\iff$. -/ @@ -265,13 +265,21 @@ 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 +## 10. Advanced Topics -Here are some random further things you should consider designing a new game: +### Escaping -* Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you +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. + +### LaTeX support + +LaTeX is rendered using the [KaTeX library](https://katex.org/), +see [Using LaTeX in the Game](latex.md) for details. + +### 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..75e95c09 100644 --- a/doc/hints.md +++ b/doc/hints.md @@ -49,6 +49,9 @@ Statement .... := by 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. +*Note*: This means you need to escape any other uses of **opening** curly brackets (i.e. `\{`). See also [LaTeX in Games](latex.md) for +examples of this. + For example, if the sample proof contains ``` @@ -84,39 +87,19 @@ 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`. +You can use Markdown to format your hints and you can +use LaTeX. See [LaTeX in Games](latex.md) for more details. -TODO: Write a doc about latex/markdown options available. +### Images -### Commutative diagrams +Hints and introductions/conclusions can also contain images. -Here is an example of how to write a commutative diagram in KaTeX: - -$$ -\begin{CD} - A @>{f}>> B @<{g}<< C \\ - @V{h}VV @V{i}VV @V{j}VV \\ - D @<{k}<< E @>{l}>> F \\ - @A{m}AA @A{n}AA @V{p}VV \\ - G @<{q}<< H @>{r}>> I -\end{CD} -$$ +For remote images, simply add: ``` -$$ -\\begin{CD} - A @>{f}>> B @<{g}<< C \\\\ - @V{h}VV @V{i}VV @V{j}VV \\\\ - D @<{k}<< E @>{l}>> F \\\\ - @A{m}AA @A{n}AA @V{p}VV \\\\ - G @<{q}<< H @>{r}>> I -\\end{CD} -$$ + ``` -See https://www.jmilne.org/not/Mamscd.pdf +Local images can currently only be included with a hack: + +Images in the game's `images/` folder will be accessible at `data/g/[user]/[repo]/[image].[png|jpg|…]` and thus can be included as if they were external images. diff --git a/doc/latex.md b/doc/latex.md new file mode 100644 index 00000000..250c9b11 --- /dev/null +++ b/doc/latex.md @@ -0,0 +1,78 @@ +There are multiple ways how to format the text content of your game. Notably Markdown with KaTeX. + +# 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! + +This means for example you'd write `/-- $\iff$ -/` but `"$\\iff$"`. + +Furthermore, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`. + +# KaTeX + +LaTeX syntax is provided trough the [KaTeX library](https://katex.org). KateX supports most but not all of latex and its packages. +See [supported](https://katex.org/docs/supported.html). + +## Examples + +### Commutative diagrams + +Here is an example of how to write a commutative diagram in KaTeX: + +$$ +\begin{CD} + A @>{f}>> B @<{g}<< C \\ + @V{h}VV @V{i}VV @V{j}VV \\ + D @<{k}<< E @>{l}>> F \\ + @A{m}AA @A{n}AA @V{p}VV \\ + G @<{q}<< H @>{r}>> I +\end{CD} +$$ + +``` +$$ +\begin{CD} + A @>{f}>> B @<{g}<< C \\ + @V{h}VV @V{i}VV @V{j}VV \\ + D @<{k}<< E @>{l}>> F \\ + @A{m}AA @A{n}AA @V{p}VV \\ + G @<{q}<< H @>{r}>> I +\end{CD} +$$ +``` + +Again, note that inside a string like `Hint`/`Introduction`/`Conclusion`/etc. you need to escape `\` and potentially `{`. + +E.g. `\begin` as `\\begin`, `\\` as `\\\\` and inside a +`Hint`, `@>{f}>>` as `@>\{f}>>`. + +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} +$$ + +``` +$$ +\begin{array}{|c|c|} + \hline + P & ¬P \\ + \hline + T & F \\ + F & T \\ + \hline +\end{array} +$$ +```