katex parse error: \hline valid only within array environment

[JadAbouHawili]

The following used to work in a doc comment: /-- -/

$$
\begin{array}{|c c|c|}
\hline
P & Q & \text{P and Q} \\
\hline
T & T & T \\
T & F & F \\
F & T & F \\
F & F & F \\
\hline
\end{array}
$$

but now must be:

$$
\\begin{array}{|c|c|c|}
\\hline
x=2 & y=6 & x=2 ∧ y=6 \\\\
\\hline
T & T & T \\\\
\\hline
T & F & F \\\\
\\hline
F & T & F \\\\
\\hline
F & F & F \\\\
\\hline
\\end{array}
$$

The documentation currently says:
"
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!
"

Moreover , the escaped backslashes version does not work in Introduction and non-escaped backslashes would error with 'invalid escape sequence'. At a loss on what to do to make latex work in Introduction...

[joneugster]

Likely due to another layer of escaping added in the feature which extracts code blocks from the translation keys.

Sounds like a bug that needs to be adressed

[JadAbouHawili]

what about Introduction? katex doesn't seem to be working there at all,

[TentativeConvert]

I can confirm something is wrong with latex parsing in the version tagged v4.29.1. This diagram from Robo, Implis L05, here rendered correctly by the live version at adam.math.hhu.de

is rendered as follows by the version tagged v4.29.1:

[TentativeConvert]

This parsing error also appeared in the brief period when the newest version of Robo was deployed on the live server (with the older undefined version of lean4game that's currently deployed there). Now that Robo is back to a pre-lean-4,29 version on the live server, the diagram gets rendered correctly.

[JadAbouHawili]

The issues I'm having were with v4.28.0 , i'll upgrade to v4.29.0 and see how it goes

edit: I can't checkout to v4.29.0 or v4.29.1 , git does not find them. Is it because they aren't 'verified' on github? I don't know what that means but this is what I noticed

[JadAbouHawili]

This parsing error also appeared in the brief period when the newest version of Robo was deployed on the live server (with the older undefined version of lean4game that's currently deployed there). Now that Robo is back to a pre-lean-4,29 version on the live server, the diagram gets rendered correctly.

on latest commit(v4.29.1) and still having the same issues , from your comment and what I tried I can conclude that checking out at v4.28.0 has the error then somewhere along the way before v4.29.0 it was working for you although for me the latex doesn't even render

[TentativeConvert]

No, you misunderstood about the versions. But the current situation is so confusing that my explanations below may not be correct either.

The version of lean4game currently deployed on the live server does not correspond to any version in the github repository. It's a patched version of some fairly old repository version, certainly from before lean 4.28. This live version of lean4game rendered all diagrams in [Robo with lean 4.28.0] correctly, but does something strange for one specific diagram in [Robo with lean 4.29.1]. The same misrendering occurs locally with [lean4game version v4.29.1] and [Robo with lean 4.29.1]. So this makes it look like the version of lean4game is not relevant here, only the version of the game. The different game versions use different versions of lean-i18n, so I perhaps that is where the error comes from.

My bad diagram is a commutative diagram set with the CD environment. The fix for me was to introduce 8-fold backslashes for line breaks instead of the 4 backslashes I used previously; see the changes to L05_Apply.lean in this commit.

[TentativeConvert]

Looking at your screenshot, I'm a bit confused why you have \ \hline showing up rather than \\hline.

[JadAbouHawili]

Looking at your screenshot, I'm a bit confused why you have \ \hline showing up rather than \\hline.

tldr; newlines are 4 backslashes in /-- -/ and 8 backslashes everywhere else(Introduction , Conclusion, Hint)

Here's the block of katex you referred to,
(works in /-- -/ but not Introduction)

$$
\\begin{array}{|c|c|c|}
\\hline
x=2 & y=6 & x=2 ∧ y=6 \\\\
\\hline
T & T & T \\\\
\\hline
T & F & F \\\\
\\hline
F & T & F \\\\
\\hline
F & F & F \\\\
\\hline
\\end{array}
$$

This works in doc comments found in the right pane but does not within the levels text(e.g in Hint or Introduction). As you have pointed out @TentativeConvert there's \ \hline , it seems like 4 backslashes give 1 backslash as output. trying 8 backslashes instead of 4 renders with no error.(as you have suggested @TentativeConvert in the linked commit)

For reference here's working katex truth table in Introduction in a level(with 8 backslashes)

$$
\\begin{array}{|c|c|c|}
\\hline
x=2 & y=6 & x=2 ∧ y=6 \\\\\\\\
\\hline
T & T & T \\\\\\\\
\\hline
T & F & F \\\\\\\\
\\hline
F & T & F \\\\\\\\
\\hline
F & F & F \\\\\\\\
\\hline
\\end{array}
$$

I think there's enough context mentioned in this issue to identify the cause of this error, I don't know if the fix would be to update the documentation to indicate that newlines are 8 backslashes or having to resolve something with lean-i18n or something else.

I'll keep this issue open, and it's up to you to decide what option to go with and close this issue when you see fit. katex is working on my end now.

[TentativeConvert]

Thank you for the update! I'm glad 8 backslashes worked for you. Unfortunately, the situation seems more complex than you describe – I have lots of display math at my end where 4 backslashes suffice, even in Hints and Introductions. So my best summary at the moment is:

Newlines are 8 backslashes in array and CD environments within Introductions, Conclusions, and Hints, and 4 backslashes everywhere else.

We will investigate what causes this strange behaviour before editing the docs.