Zulip Chat Archive

Stream: general

Topic: latex \sum


view this post on Zulip Sebastien Gouezel (Dec 17 2020 at 07:34):

In #5397, I have fixed a latex issue, but it just revealed another one. In the docstring just below docs#formal_multilinear_series.continuous_on, a latex command \sum shows like a text sum instead of a nice Sigma. I had checked my latex using https://observablehq.com/@bryangingechen/github-lean-doc-preview?url=%22https%3A%2F%2Fgithub.com%2Fleanprover-community%2Fmathlib%2Fblob%2Fmaster%2Fsrc%2Fanalysis%2Fanalytic%2Fbasic.lean%22#docs before submitting the PR, and there the Sigma shows up. Do you understand what is going on here?

view this post on Zulip Sebastien Gouezel (Dec 17 2020 at 07:55):

It works in other files such as docs#bernoulli

view this post on Zulip Bryan Gin-ge Chen (Dec 17 2020 at 07:59):

Unfortunately the previewer does not reproduce all the quirks of markdown2. I suspect this may be the same issue as doc-gen#62.

view this post on Zulip Bryan Gin-ge Chen (Dec 17 2020 at 08:06):

It would be a good idea to switch the markdown renderer to mistletoe to match the community website, but that might be a big project.

view this post on Zulip Sebastien Gouezel (Dec 17 2020 at 08:48):

The problem is definitely not with the previewer, it is really on the community website side! Although I have no clue what I am doing wrong here.


Last updated: May 09 2021 at 20:11 UTC