khatex

Stream: general

[Patrick Massot]

@Edward Ayers could you comment on https://github.com/leanprover/vscode-lean/pull/225? What do you want khatex for? And why not using mathjax instead, especially now that we have mathjax 3.0?

[Edward Ayers]

I guess I'm just more familiar with katex. I'm not married to it.

[Edward Ayers]

The plan is to try this out as a model for adding certain useful libraries to widgets.

[Edward Ayers]

The principled way would be to allow Lean to emit javascript that can run random libraries. But the thinking is that katex and D3 cover a lot of the use cases for having custom javascript libraries, so it makes sense to add them in directly to vscode-lean.

[Patrick Massot]

What do you have in mind using D3? This is a huge library (which very low-level and difficult to learn, but that's a different story).

[Edward Ayers]

If people don't like it (eg it bloats the vscode extension too much) then it is no problem to remove it.

[Edward Ayers]

There are some React wrappers for D3 that I was looking at

[Edward Ayers]

Even just being able to let Lean widgets render graphs would be really useful.

[Patrick Massot]

Wouldn't be easier to work on "jump to definition" in the info view?

[Edward Ayers]

well triaging is a different question...

[Patrick Massot]

Sure, you're free to work on anything you find most fun.

[Reid Barton]

I would totally use Khatex

[Patrick Massot]

I didn't think of it that way

[Edward Ayers]

Is there some beef around katex vs mathjax? Afaict they seem to be exactly the same but I'm not really paying attention

[Gabriel Ebner]

This was also my impression. I thought katex is the new, modern, cool, in rewrite of mathjax.

[Patrick Massot]

No, that's the old new mathjax

[Patrick Massot]

The new new mathjax is mathjax 3.0

[Patrick Massot]

But I'm not a specialist here.

[Johan Commelin]

https://pbelmans.ncag.info/blog/2015/12/21/on-towards-mathjax-3-0/ is 5 years old, but maybe still relevant

[Johan Commelin]

Written by the guy who does the frontend for Stacks Project and Kerodon

[Adam Topaz]

Does mathjax 3 support tikz?!

[Patrick Massot]

No. plastex uses server-side tikz rendering.

[Adam Topaz]

Ah ok

[Edward Ayers]

Looks like it's an open issue though: https://github.com/mathjax/MathJax/issues/41

[Edward Ayers]

That would be a game changer

[Edward Ayers]

This compiles tex to web assembly and then renders as an svg (!) https://github.com/kisonecat/tikzjax

[Edward Ayers]

So assuming that library works we could actually do this in theory

[Patrick Massot]

It's probably pretty slow.

[Bryan Gin-ge Chen]

Hopefully this makes it easier to tackle leanprover/vscode-lean#139 (on rendering LaTeX in doc strings on hover).

[Patrick Massot]

Speaking of slowness, did something happen in the last couple of days? The widget view sometimes lags like crazy.

[Edward Ayers]

I don't think so.

[Edward Ayers]

3.19 came out but idk what would have changed to cause it to be slow

[Patrick Massot]

Let's wait to see if anyone else noticed something, and if Gabriel has an idea. Maybe it's my computer.

[Bryan Gin-ge Chen]

mathlib master isn't on 3.19.0c yet anyways. Do you notice it happening on any specific files, or just all of them in general?

[Patrick Massot]

I've been working both on linear algebra and integration.

[Johan Commelin]

When Scott shared his screen this afternoon, he also had trouble with the widget view

[Scott Morrison]

Yeah, it was lagging badly. It seemed like when my mouse passed over the rendered goal, nothing would happen for 2-10 seconds, and then there would be a sudden burst of different highlighting passing through the rendered goal, presumably following the path of my mouse.

[Scott Morrison]

The other things I would really like in the goal view are:

1. whitespace and indenting matching the plain text view (I often turn off widgets because the expressions become unreadable without indenting)
2. coloured parentheses to show matching pairs!

[Alex Peattie]

@Scott Morrison (or anyone else) could you share an example of a theorem with a goal that's very laggy?

[Scott Morrison]

e.g. if I put the cursor at line 107 of src/topology/sheaves/sheaf_of_functions.lean in master, go to the first goal, then shake the mouse up and down over the goal, I can quickly get it to lag many seconds behind.