add mathjax to header so docs can use latex with the usual delimiters

[glangmead]

This is one way to enhance the docs with LaTeX. The authors of mathlib can simply add math in the comments with the usual delimiters. These pass through into json_export.txt (escaped appropriately for json), and then directly into the HTML. I confirmed this end to end. The only change I had to make was to add MathJax to the header of each page, so it can find the delimited math and render it.

[robertylewis]

Thanks for this! I think the ideal for @PatrickMassot and others would be "full" TeX support in the docs, i.e. the ability to draw diagrams and such. But MathJax is a big and apparently easy step toward that.

[robertylewis]

IIRC Zulip (and other LaTeX/makdown combos?) don't use single $ delimiters for inline MathJax. It results in a lot of false positives. I'm not sure how big a worry it is here. Is MathJax smart enough to avoid inserting itself in code blocks f $ g $ h a? If not, double $$ is safer.

[jcommelin]

Is there a way to see how the docs render with this patch in place? I.e., can we test what happens?

[robertylewis]

http://robertylewis.com/mathlib_docs/ is a build with @glangmead 's changes enabled.

[robertylewis]

Something funny is going on here. I don't think the parens are escaped in the markdown. Does ['\(', '\)'] mean that everything in parens will become Mathjax??

[jcommelin]

It should mean that \( x + \sqrt{y + z} \) is parsed as mathjax. So the \ has to be explicitly in the source before the parens.

[glangmead]

MathJax does exclude itself from <code> blocks and you can configure it to exclude more css classes. I'll test that out.

[robertylewis]

(Edit - oops, you beat me to it...) For what it's worth, MathJax is already smart enough to avoid running in <pre> or <code> blocks. So $ occurrences in Lean code shouldn't trigger it, unless someone has forgotten to put backticks around it. So maybe the simple solution is to keep single $ and remove \( as delimiters. I doubt there are many if any plain text lines in mathlib that have two $s.

[robertylewis]

Gosh is there an existing bug with parens? See https://leanprover-community.github.io/mathlib_docs/geometry/manifold/real_instances.html where the definition of euclidean_space in lean is def euclidean_space (n : ℕ) : Type := (fin n → ℝ) but on the web some of it is deleted: def euclidean_space : ℕ → Type.

This isn't a bug. The web docs are only displaying the type, which is ℕ → Type. The ℕ argument doesn't have to be bound to print Type, but in the source it's referenced in the body of the definition (fin n → ℝ).

[robertylewis]

It is maybe a badly phrased doc string though. It should "informally bind" n, i.e. "euclidean_space n is the space ℝ^n."

[glangmead]

I learned a few things and will update the PR shortly. First, I've swung back to wanting dollar signs and NOT the parens or brackets, since the latter do not pass cleanly through markdown. Stackoverflow has the same problem, see https://math.meta.stackexchange.com/a/18714. So: only single and double dollars should be processed, which will be what most people guess they should use anyway.

Further, I've added all the lean-related css classes Rob defined in the python script as exclusions for MathJax. Some of those do not also have pre or code around them, so this should help keep MathJax out of the Lean stuff entirely. It can be further tweaked later of course!

[jcommelin]

What is this polyfill thing? Is there a reason to grab mathjax from there? Should we self-host a copy?

[glangmead]

The MathJax docs said to put both these inclusions which surprised me. Polyfill is apparently there as a backoff for "older browsers". I don't know how necessary it really is, I'll find out. As for self-hosting I don't know all the tradeoffs. The authors of mathlib don't need to care of course.

[glangmead]

The docs http://docs.mathjax.org/en/latest/output/browser.html say that polyfill is there to support IE11. The stats here https://www.w3counter.com/globalstats.php say that IE11 is ranked 8th with 2.3% of... whatever they're counting.

[jcommelin]

Ok, thanks for explaining. In that case, I'm fine with using polyfill.

[glangmead]

Thanks for the question. I only followed up with that research once you asked, having merrily copied and pasted it.

[glangmead]

Attaching a zipped version of real_instances.html, where I have a test comment

# Constructing examples of manifolds over dollar $\mathbb{R}$ or double dollar $$\mathbb{R}$$. Or paren \(\mathbb{R}\) or bracket \[\mathbb{R}\]

and the rendered html attached here shows that dollars are processed by mathjax, double-dollars are processed and create display mode, and the paren/brackets are not processed by mathiax.

real_instances.html.zip

Happy also for @robertylewis to regenerate the docs so we can browse for issues again if desired.

[robertylewis]

I've regenerated the docs, with a few examples of good behavior: https://robertylewis.com/mathlib_docs/tactics.html

I don't know of any natural occurrences of $..$ in the library to check, but I'm pretty convinced that this will work! We'll keep an eye out for any breakage.

[PatrickMassot]

For the record, let me write that I think we should do server-side rendering here. There is no dynamic content in those pages, the doc generation script should call mathjax instead of asking all readers web browsers to do so. This allows opens up the possibility of having commutative diagrams or other fancier LaTeX. But I don't have time right now :-(

[glangmead]

When you say "render", what output format do you have in mind? To me LaTeX is a markup language like HTML and MathML that the browser's job is to render. Because it's left as markup the browser can change the font, colors, do screen reading for accessibility etc.

[urkud]

@PatrickMassot AFAIK, MathJax outputs different HTML in different browsers, so it can only run in browser. At least it worked that way a couple of years ago.