Zulip Chat Archive
Stream: general
Topic: latex \sum
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?
Sebastien Gouezel (Dec 17 2020 at 07:55):
It works in other files such as docs#bernoulli
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.
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.
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: Dec 20 2023 at 11:08 UTC