LaTeX problem in docstring

Stream: mathlib4

[Michael Stoll]

I've noticed that the docstrings for docs#Finset.card_erase_of_mem and docs#Finset.cast_card_erase_of_mem give an error message "You can't use 'macro parameter character #' in math mode" in the html docs. I assume the \#s there need another escaping \. Would it be OK to add this fix to the somewhat unrelated #8252, or is this rather not done?

[Patrick Massot]

I vote ok. In principle it is nice to keep PRs with only related changes, but this is simply too much energy waste in such trivial cases.

[Eric Wieser]

I don't think we should be changing the comments here; this looks like a bug in our markdown renderer (https://github.com/xubaiw/CMark.lean)

[Eric Wieser]

(or at least, a missing feature; it presumably doesn't have any Math support, so we've just tried to glue support on top in another layer)

[Michael Stoll]

The lean doc preview shows it correctly (and gives an error with a double backslash). So it's hard to test any changes. (I did notice that when github renders md files containing LaTeX, some symbols need an additional backslash to be rendered correctly, but I don't know if this is related.)

[Michael Stoll]

Eric Wieser said:

I don't think we should be changing the comments here; this looks like a bug in our markdown renderer (https://github.com/xubaiw/CMark.lean)

So I'll undo the attempted fix, and we wait until this is solved in The Right Way :tm: ?

[Eric Wieser]

If nothing else I think we shouldn't be putting hacks in unrelated PRs

[Bryan Gin-ge Chen]

A few years back I spent some time getting LaTeX working properly with markdown in doc-gen3 (and the Lean doc preview), and what I ended up doing there was just to adapt code from StackExchange's LaTex + markdown handling. As Eric says, it looks like this hasn't made it to doc-gen4 (yet?).

I unfortunately don't have time at the moment to dig into how doc-gen4 / CMark.lean does things, but for anyone who wants to try fixing LaTeX in markdown in doc-gen4, the following might be useful. First, this notebook gives a very brief explanation of the basic strategy I used, and also includes some JS code used in the Lean doc preview. Second, here's our (less-well-documented) Markdown handling code in doc-gen3 as well as my Python port of StackExchange's code

Of course anyone should feel free to ping me / PM me with any questions.

[Eric Wieser]

I think the difficulty here is that we're using the reference implementation of commonmark written in C, and commonmark isn't showing any signs of agreeing how to represent math

[Bryan Gin-ge Chen]

With the caveat that I haven't looked at doc-gen4's code at all, I think the basic strategy of stripping out chunks of math, sending everything else to CMark.lean to generate HTML, and then putting the math back should hopefully work there too.

Regarding conventions on how to represent math in Markdown, with doc-gen3, I decided to just go with StackExchange's conventions since it was what we were already writing in docstrings. If commonmark decides on something else down the line, then I guess things will get even messier...

[Eric Wieser]

I would imagine it's probably easier to fork cmark and duplicate these code-parsing lines for LaTeX

[Eric Wieser]

Then we have to fork / push to CMark.lean, since that contains copies of the files in cmark

[Bhavik Mehta]

Note earlier discussion about this: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Docs.20.22.23.22.20in.20math.20mode.20errors