I've broken a documentation page

Stream: mathlib4

[Mitchell Lee]

I recently merged in a pull request that affected Mathlib.GroupTheory.Coxeter.Basic.
https://github.com/leanprover-community/mathlib4/blob/03b471425ef6894a1385678605489d7ef289754b/Mathlib/GroupTheory/Coxeter/Basic.lean#L74-L74

Unfortunately, it seems to have broken the documentation page.
https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Coxeter/Basic.html

Somehow, the expression $M = (M_{i,i'})_{i, i' \in B}$ is not treated as math mode, and it has some very strange italicization. A similar issue occurs multiple times throughout the page. Also, $S = \{s_i : i \in B\} \subseteq W$ is rendered without the curly braces.

The page looks just fine in the Lean doc preview (https://observablehq.com/@bryangingechen/github-lean-doc-preview). How can I fix this?

[Eric Wieser]

This is a bug in docgen4, the fix is to teach docgen4 to parse LaTeX correctly: https://github.com/leanprover/doc-gen4/issues/178

[Utensil Song]

Underscores and other conflicting syntax in LaTeX will confuse most markdown parsers, include the markdown parser that docgen4 is using.

IIUC, github-lean-doc-preview avoided this issue by replacing everything between single/double dollar pairs with placeholders, running the markdown doc through markdown parser, then putting them back where they were in the resulting HTML.

If you are working on a mathlib PR, and you have some formulas that render fine with lean doc preview, I'm told that in this situation, you can safely leave the "broken" formulas there for the PR merge, so that once docgen4 has fixed the issue, all "broken" formulas will be rendered correctly like they were in docgen 3.

[Mitchell Lee]

Thanks.

[Utensil Song]

Recently I became aware of how they did it in Hugo as hugo-goldmark-extensions, see gohugoio/hugo#10894 for more background.

This seems simple and robust enough.

[Eric Wieser]

I think the issue is that doc-gen uses the (C code) reference implementation of the commonmark spec, which is not really extensible