Doc improvements

[JadAbouHawili]

This came out of the issue #235, but some changes extend beyond the issue there.

I explicitly mentioned that KateX does not support the entirety of latex, because that was what i assumed(not familiar with KateX, until now at least).

I moved a note about latex that was in creating_game.md because it doesn't seem like a good place for it.

Added truth table example , explicitly mentioning that tabular is not supported because that is something that stumped me for a bit and probably stumped other people.

More changes?(either too drastic or i never used the feature to be able to document it):

• add an example where curly braces are escaped in a hint, i never used this before so i preferred not to do it and mess it up.
• create_game.md seems like a tutorial walkthrough of making your own game, until the 'test game locally heading' where it switches gears and reads like documentation. This slightly confused me the first time i read it, and I think a walkthrough should be included in a separate file. Maybe remove the walkthrough to a separate file and merge the rest in writing_exercises.md?
• DOCUMENTATION.md contains stuff about servers, should it be in server.md?
• Do markdown features inside quotes require their own file? I have heard there are variants for markdown, should it be explicitly mentioned which one is supported?

Thoughts?

[joneugster]

Thank you, I'll look at it in more detail when I'm back in a few days

[JadAbouHawili]

@joneugster any comments or suggestions?

[JadAbouHawili]

willing to iterate on this

[JadAbouHawili]

Found an undocumented feature, having '/-- text here -/' above 'Statement' makes it appear above the problem. Here's a screenshot:

[joneugster]

Thank you very much for your contribution! and sorry for the slow replies. I just came back from vacation and I have a more urgent project first, but I'll look at all PRs here early next week!

The feature is documented here:
https://github.com/leanprover-community/lean4game/blob/main/doc/create_game.md#doc-string--exercise-statement
although arguably this entire file is growing quite a bit and is not the easiest to search through

[JadAbouHawili]

oh, i missed that.
To state the obvious, i guess the heading you referenced should go to writing_exercises.md and not be in create_game.md.
I'll keep thinking about how to break up the docs into more readable chunks, but won't do any other pull requests until this one is resolved.

No worries about the late replies.

[joneugster]

Thanks for the PR, and sorry for the slow reply!

I now pushed a commit that should include your suggestions. Maybe you can have a look and if you either have corrections or any other suggestion, I think it's best if you add a new PR about that.

---

Here are my thoughts to your questions:

add an example where curly braces are escaped in a hint, i never used this before so i preferred not to do it and mess it up.

There might still not be any such example explicitely, and it would be welcomed to add such examples. Especially also if you want to write "${$" as LaTeX in a Hint, then it would become Hint "$\\\{$" (\ -> \\ and { -> \{, so 3 in total!)

create_game.md seems like a tutorial walkthrough of making your own game, until the 'test game locally heading' where it switches gears and reads like documentation. This slightly confused me the first time i read it, and I think a walkthrough should be included in a separate file. Maybe remove the walkthrough to a separate file and merge the rest in writing_exercises.md?

I'm open to reorganisation of the docs!

DOCUMENTATION.md contains stuff about servers, should it be in server.md?

That is an old file that should be probably removed and a server.md needs to be written from scratch. I do have to do that in the next two months still.

Do markdown features inside quotes require their own file? I have heard there are variants for markdown, should it be explicitly mentioned which one is supported?

Maybe latex.md could be more a formatting.md and contain doc/examples for Markdown+KaTeX