switch from markdown2 to mistletoe #110
Conversation
|
I'm going to try to modify the markdown processor so that it's as close to the behavior on https://math.stackexchange.com and https://mathoverflow.net as possible, since (in my opinion) those sites are the most significant places on the web right now where users frequently input LaTeX embedded in markdown. This is likely to break some of the LaTeX we currently have, but I think the consistency will be worth it. edit: After doing some more digging and experimentation, References:
edit 2: Welp, the naïve approach I had in mind of just using regex to protect the math failed, so I ended up just porting some of the code used by StackExchange to Python. |
|
@bryangingechen thank you for taking this on! This change is definitely overdue. I'm happy to merge this as soon as there's no obvious breakage worse than what it fixes. I see you marked this as a draft, is there more you're planning to change? |
|
Ok, let's try this out! #deploy 🐙 |
|
Ok, the trigger seems to work! I've canceled the workflow, because I realized that we still need to merge master here in order to get the new |
|
#deploy |
|
Okay, this failed because #deploy |
|
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! |
|
Oh, this new test workflow is cool!
Yeah, I still haven't finished the changes described in my second comment above. The good news is I think I've already managed to fix #10. I'll try to clean things up and push a commit with my progress tonight. |
|
#deploy and fix the $4 |
|
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! |
|
#deploy 🙏 |
|
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! |
With leanprover-community/doc-gen#110, these should no longer be needed.
| ds_no_math, math = remove_math(ds, '$') | ||
| # We have to run `mathjax_editing.replace_math` on the text in code | ||
| # blocks before passing it to Pygments (see `render_block_code`), | ||
| # otherwise `replace_math` will be confused by the added syntax | ||
| # highlighting `<span>`s and won't be able to splice in those blocks. | ||
| self.math = math | ||
| html = self.render(Document(ds_no_math)) | ||
| return replace_math(html, self.math) |
There was a problem hiding this comment.
I don't quite follow why this is necessary - does mistletoe.latex_token.Math not work here?
With leanprover-community/doc-gen#110, these should no longer be needed. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
With leanprover-community/doc-gen#110, these should no longer be needed. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
markdown2 has a lot of trouble with latex+mathjax, see e.g. #10, #62 and various issues on Zulip. mistletoe is what leanprover-community.github.io uses and it seems to do better with these examples.
As part of this effort, I copied some of the implementation of Markdown + LaTeX from StackExchange's code math.stackexchange and mathoverflow. I believe #10 and #62 are now fixed, though some workarounds that were committed are now broken, e.g. the module doc string right before
formal_multilinear_series.change_origininanalysis.analytic.basic. Compare mathlib_docs to mathlib_docs_demo.For a bunch of LaTeX examples (including ones copied from the issues above), see the new test page, latex.html.
Since I was making a bunch of changes to the markdown rendering anyways, I went ahead and factored it all out into a separate file.
Some smaller changes:
Markdown headings now have a
#link after them, which allows linking to the middle of a page (as in make markdown headings linkable leanprover-community.github.io#11).The syntax highlighting now defaults to
lean.Some dead code was removed.
I plan to follow this up with a PR to our naming conventions with some advice on LaTeX + Markdown, now that things should be more consistent.