improve doc, adaptation of #250
Co-authored-by: JadAbouHawili <jad-abou-hawili@hotmail.com>
This commit is contained in:
co-authored by
JadAbouHawili
parent
a46840d327
commit
8c5e47dd7b
+15
-7
@@ -194,7 +194,7 @@ You can but a `Statement` inside namespaces like you would with `theorem`.
|
|||||||
|
|
||||||
#### Doc String / Exercise statement
|
#### 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
|
```lean
|
||||||
/-- The exercise statement in natural language using latex: $\iff$. -/
|
/-- 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.
|
* `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.
|
* `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
|
would write `Introduction "some latex here: $\\iff$."` but
|
||||||
`/-- some latex here: $\iff$. -/ Statement ...`
|
`/-- 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
|
### LaTeX support
|
||||||
of control.
|
|
||||||
|
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.
|
||||||
|
|||||||
+12
-29
@@ -49,6 +49,9 @@ Statement .... := by
|
|||||||
Put variables in the hint text inside brackets like this: `{h}`! This way the server can replace
|
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.
|
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
|
For example, if the sample proof contains
|
||||||
|
|
||||||
```
|
```
|
||||||
@@ -84,39 +87,19 @@ create new assumptions.
|
|||||||
|
|
||||||
## 6. Formatting
|
## 6. Formatting
|
||||||
|
|
||||||
You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$`
|
You can use Markdown to format your hints and you can
|
||||||
|
use LaTeX. See [LaTeX in Games](latex.md) for more details.
|
||||||
|
|
||||||
**Escaping**: Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
|
### Images
|
||||||
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.
|
Hints and introductions/conclusions can also contain images.
|
||||||
|
|
||||||
### Commutative diagrams
|
For remote images, simply add:
|
||||||
|
|
||||||
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}
|
|
||||||
$$
|
|
||||||
|
|
||||||
```
|
```
|
||||||
$$
|
<img src=\"https://url.com/to/image\"/>
|
||||||
\\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.
|
||||||
|
|||||||
@@ -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}
|
||||||
|
$$
|
||||||
|
```
|
||||||
Reference in New Issue
Block a user