Skip to content

Commit

Permalink
improve doc, adaptation of #250
Browse files Browse the repository at this point in the history
Co-authored-by: JadAbouHawili <[email protected]>
  • Loading branch information
joneugster and JadAbouHawili committed Jul 31, 2024
1 parent a46840d commit 8c5e47d
Show file tree
Hide file tree
Showing 3 changed files with 105 additions and 36 deletions.
22 changes: 15 additions & 7 deletions doc/create_game.md
Original file line number Diff line number Diff line change
Expand Up @@ -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$. -/
Expand Down Expand Up @@ -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.
41 changes: 12 additions & 29 deletions doc/hints.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

```
Expand Down Expand Up @@ -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}
$$
<img src=\"https://url.com/to/image\"/>
```

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.
78 changes: 78 additions & 0 deletions doc/latex.md
Original file line number Diff line number Diff line change
@@ -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}
$$
```

0 comments on commit 8c5e47d

Please sign in to comment.