LaTeX in Lean?

Stream: mathlib4

[Thomas Murrills]

I've been playing around with getting MathJax to run in the infoview, purely as a personal exercise to learn ProofWidgets:

This isn't an Expr pretty-printer—that's just the raw pretty-printed text fed naively to MathJax! The point here was just to learn ProofWidgets and see if I could even get MathJax running. :) (Has this been explored elsewhere already?)

But, beyond this extremely simple proof-of-viability, I was wondering if anyone had any thoughts about whether we actually want to pursue pretty-printing of math in the Lean interface in any way. Searching zulip reveals some interest, as well as a possible extant LaTeX pretty-printer for Expr (in the works as of Feb)? :eyes:

Some thoughts in this area:

• Presumably the first priority is not obscuring the underlying expression (as mentioned in the first linked thread). We'd definitely want to (at least) show the underlying Expr on hover (perhaps on click as well?), and have toggles in the infoview and/or a set_option for turning off this sort of pretty-printing quickly. An option to show both at once might even be useful.
• It would be powerful to have the option to "delaborate to interactive HTML" in the tactic state—expr_presenters but without the isolation in a separate panel. If all hypotheses could be displayed in LaTeX at once, that would be beautiful. (The ability to extensibly customize the rendering of the tactic state in general also might allow people to build some really interesting things.) Again, transparency and ease of turning this off would be essential.
• It's no more than an idea at this point, but I wonder if with some work we could eventually enable LaTeX-like input—and in-place rendering—in VS code by creating a VS code custom editor via the extension. Everything would look the same except for syntax/exprs which were deemed eligible for LaTeX pretty-printing, which would be replaced with nicely-rendered LaTeX. We'd probably want to maintain a strict correspondence between LaTeX and syntax/Expr's—that way, parsed and/or elaborated lean code could be automatically pretty-printed without special annotations everywhere, and latex input wouldn't have to be saved anywhere in the file (it could be recovered from ordinary lean syntax simply by re-parsing/elaborating and then pretty-printing). This would mean Lean and Lean code could remain fundamentally unchanged while the extension does the majority of the work. There would be challenges, of course, like saving size info to prevent major reflows upon re-elaboration and, of course, making the underlying lean code easily accessible through interactivity—but these are not insurmountable with some work, and it seems at least...plausible. :)

Thoughts?

[Kyle Miller]

@Thomas Murrills Great! We'd been wanting to connect up our LaTeX pretty printer to the info view using MathJax and ProofWidgets, but we hadn't gotten around to it yet. The main interface is basically a function Expr -> MetaM String, so it should be easy to hook it into what you have.

[Kyle Miller]

We've also been meaning to publish a repository for the LaTeX pretty printer portion of our project

[Kyle Miller]

Regarding hypotheses, we also have another sort of pretty printer that can be used for turning the whole local context into a mix of English and LaTeX, and we wanted to try hooking this into the info view as well.

[Kyle Miller]

Would you mind sharing the code at some point?

[Wojciech Nawrocki]

Whoa, nice!

We'd definitely want to (at least) show the underlying Expr on hover (perhaps on click as well?).

From the UI perspective I think this could work. MathJax wants to show its own dropdown on right-click, but it doesn't seem to handle click or hover. It would probably be a change to the ExprPresentation component in ProofWidgets.

and have toggles in the infoview and/or a set_option for turning off this sort of pretty-printing quickly

I was thinking of having a single dropdown which determines the default way to display Exprs. If you don't want LaTeX, you change the default to standard (or whichever word). There is a design issue here.

It would be powerful to have the option to "delaborate to interactive HTML" in the tactic state—expr_presenters but without the isolation in a separate panel.

I had written down some initial notes on the design of inline Expr presentations in ProofWidgets here. expr_presenters are definitely not tied to being in a separate panel :) That's just one way to display them.

[Thomas Murrills]

Kyle Miller said:

Would you mind sharing the code at some point?

Of course! (I.e., I wouldn't mind!) :) I'll try to get it into a not-so-hacky state later today or tomorrow.

It's quite simple, but there are some implementation considerations to think about. Namely, this uses MathJax's conversion of tex to svg. I'm not sure if that's what we want—it might be better to use common html and fonts (I'm not sure what the tradeoffs are). However, I ran into some access-denied issues when trying to use the local copies of those fonts, possibly related to this issue. I tried solving it by modifying the MathJax source appropriately, but ran into some npm issues that I'm not sure how to debug—but this isn't to say that they're undebuggable! :)

[Matthew Ballard]

Nice! How easy would it be to swap out MathJax for Katex (or something else)?

[Kyle Miller]

@Thomas Murrills We're using the CDN in our own project because we ran into issues like that too, but it would be nice not to need Internet access when using this!

[Thomas Murrills]

Matthew Ballard said:

Nice! How easy would it be to swap out MathJax for Katex (or something else)?

It all depends on the internals! MathJax works by creating a global JS object, for example, and puts all its functionality in there; I'm not sure how KaTeX works.

[Thomas Murrills]

That reminds me of more implementation considerations: there might be a better way to set up this object; also, (a)synchronous concerns might be relevant. MathJax provides several ways to typeset math—typeset (which acts on the whole page or on selected elements), typesetPromise, and modular converters like tex2svg. If we have lots of LaTeX in view, when and how we render it (and how it gets stored—MathJax keeps track of what it renders!) will become relevant. It could be useful to do all the rendering "in one go" at the end if that would somehow be possible—or maybe that's not actually more efficient. I'm not sure yet! :)

[Eric Wieser]

I think when making conference presentations in html, I found that KaTeX was generally more performant than mathjax

[Eric Wieser]

I imagine a goal view being frequently changed might benefit from that performance

[Matthew Ballard]

I also found that their native node package was easier to work with.

[Thomas Murrills]

It would definitely be useful to experiment with both! I'll see if I can get them both working...

[Kyle Miller]

In our demo, we use a virtual dom (via mithril.js) and have a MathJaxComponent that manages the MathJax lifecycle (so calls MathJax.typesetPromise when contents change and MathJax.typesetClear when the dom element is being removed). It was fiddly to get it to work, and there are still some timing bugs in the mouseovers where the popups are in slightly different positions depending on whether it's showing equations that MathJax has rendered before.

[Peter Jipsen]

This is an excellent idea to do some (MathJaX/KaTeX) pretty-printing in infoview, and also possibly on the input editor side. It has the potential to make Lean notation considerably more readable for mathematicians and math students, and at the same time preserving the original Lean syntax.

[Eric Wieser]

I don't think it's really possible on the input editor

[François G. Dorais]

@Peter Jipsen It would be nice to have an ASCIIMathLean similar to your ASCIIMathML. Do you have thoughts about this?

[Peter Jipsen]

I think the "mathematical expression" syntax of Lean (i.e. some vaguely defined small subset of Lean syntax) is the appropriate analogue of ASCIIMathML, and the Lean->LaTeX translator that Kyle and Patrick have written already does the job. Whether this can be used for the VS code input editor is a technical question. It would be useful even if it is only a reading mode, as long as hovering on expressions still provides the same information (in infoview it can of course be used interactively, and in editing mode it could perhaps be used for all lines that do not currently contain the cursor).

[Thomas Murrills]

@Kyle Miller I have a somewhat busy weekend, but a basic/hacky version of the code—but with comments on what I've learned and tried so far (at least with respect to what I've committed; more to come)—is available in Mathlib.Tactic.Widget.LaTeX on the thorimur/latexperiments branch of mathlib4. (I'll leave it up to the reader to decide how to actually pronounce that portmanteau. :) )

I'm going to keep adding to this branch over the coming days to include the rest of what I've tried (incl. what I've noticed hasn't worked), different approaches, and KaTeX, which looks pretty painless. I'll update here as I do more experimenting. :)

[Thomas Murrills]

I've been hitting a bit of a wall with producing vscode URI's so that I can access fonts. (This is necessary for both MathJax and KaTeX.) This involves using definitions from the vscode API like Uri.file.

However, the vscode API is not accessible from the point at which the widget's javascript will be run. I tried creating a new package solely for bundling the vscode function(s) I needed, but rollup.js hits me with (!) Unresolved dependencies—it can't find vscode even though it's installed in the package. Maybe I'm doing something wrong? (This is with @types/vscode, vscode-test, and even the deprecated vscode (out of desperation) as a dependency, not a devDependency.)

I hardcoded my own local URI and got it to work, so if we can find a way to produce URIs, things will be possible! But is trying to bundle this functionality even the right way to go? Does this even make sense (maybe this kind of functionality is not even bundleable because it needs to run in an environment that can't exist here)? Should something else be done, somehow? E.g. should the extension expose this functionality to the javascript it runs somehow?

[Thomas Murrills]

(Also, maybe it's possible that the setting up of the relevant style tag should not even be done by a widget's javascript, but by some other means which would be more amenable to this kind of thing.)

[Wojciech Nawrocki]

Hm, what happens if you try to load the font from the web?

[Thomas Murrills]

I bet that would work, but I'm interested in making this available locally if possible! :) (I'll include the web version in the experimentation as well though.)

[Wojciech Nawrocki]

Ah gotcha! JS bundlers such as Rollup provide ways of bundling data in the .js output file. It should be possible to do that with a font as well. You should hopefully not have to worry about anything to do with vscode.

[Thomas Murrills]

Hmm, ok! Will it work (indirectly) with CSS? Is there a place “in the page” that I can put the fonts so that the CSS can refer to it? (I’ll look into this myself, just wasn’t sure if you had a strategy outlined off the top of your head! :) )

[Wojciech Nawrocki]

What I had in mind is that you can use a data: URI with base64, and rollup can build that for you. See here for example. You can then use that URI inside your CSS.

[Thomas Murrills]

Ah, gotcha, thx for the link and the pointer to data:! (That should hopefully be enough for me to go on—I’m just learning the landscape of HTML/CSS/JS here, so simply knowing what exists is often the missing link/crucial piece at this stage.)

[Thomas Murrills]

Alright, that worked! :) I've got a basic version of KaTeX working on my experimentation branch—I forked KaTeX to allow bundling of fonts during webpacking.

[Thomas Murrills]

Next I'll try to get a more polished version working, and maybe see if I can bundle the fonts in MathJax, too, though that's a little more opaque (and maybe not worth it). Currently I just use dangerouslySetInnerHTML, which sounds, well, dangerous, and I bet it can be done more safely (apparently, maybe, with a ref).

I'd also like to try to get e.g. katex.render working if possible, and maybe look more deeply into how the server works. E.g., if we can run the JS that loads katex and the CSS as soon as we start looking at the file, without using a widget/expr_presenter, that might be useful.

[Wojciech Nawrocki]

if we can run the JS that loads katex and the CSS as soon as we start looking at the file, without using a widget/expr_presenter, that might be useful.

I am not following here. If you want to run some JS in the infoview that's not builtin, the only way to do that is with a widget.

[Wojciech Nawrocki]

As far as execution of widget JS modules goes, a module will stick around in memory after the first time it is ran. So if you write an expr_presenter using a module that initializes some global katex state and stores that in a top-level var, that constant will persist.

[Thomas Murrills]

Ah, okay. I thought there might be some other way hidden deep in lean which widgets were built on top of. :)

[Thomas Murrills]

I suppose each expr_presenter can just check if katex exists each time it runs, as I currently have <AddKaTeX /> do. But I thought it might be possible to get the infoview to run JS based solely on the imports/something in the environment, and load everything up even before Expr’s are encountered/presented—do you think that kind of thing is possible? It might not matter if it’s just a small delay the first time we see any mathy Expr, though.

[Wojciech Nawrocki]

We have an issue open for having widgets that always show up in a given file. You could potentially use such a global widget with no associated UI, and which just runs some code under the hood, for this. However my intuition would be that this is premature optimization; I think an initial delay the first time katex shows up is perfectly fine. Let's only worry about it if it becomes too long and somebody complains!

[Wojciech Nawrocki]

I suppose each expr_presenter can just check if katex exists each time it runs

This is what I would do.

[Thomas Murrills]

I finally watched Patrick & Kyle's IPAM presentation and played with the demo, and wow! That's beautiful! I'd love to see that become fully realized and see what parts can be adapted for interactive use on the proofwriting side.

@Kyle Miller, if you're interested in sharing the code from the demo, maybe we could get LaTeX pretty-printing (at least for mathematical expressions in the infoview, as a first step) running in mathlib4 in the not-too-distant future! By the way—interactivity and UI/X is really what I'm interested in when it comes to proof assistants, so in general, feel free to reach out if/when you continue working on this kind of thing and if you would like some extra hands and/or ideas. (And likewise for anyone else pursuing similar projects!) Obviously I'm still learning about these technologies and best practices, but, you know, eager to learn, etc. :)