Stream: general

Topic: khatex

Patrick Massot (Aug 28 2020 at 13:52):

@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 (Aug 28 2020 at 13:53):

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

Edward Ayers (Aug 28 2020 at 13:54):

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

Edward Ayers (Aug 28 2020 at 13:56):

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 (Aug 28 2020 at 13:57):

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 (Aug 28 2020 at 13:57):

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

Edward Ayers (Aug 28 2020 at 13:57):

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

Edward Ayers (Aug 28 2020 at 14:00):

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

Patrick Massot (Aug 28 2020 at 14:00):

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

Edward Ayers (Aug 28 2020 at 14:04):

well triaging is a different question...

Patrick Massot (Aug 28 2020 at 14:04):

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

Reid Barton (Aug 28 2020 at 14:07):

I would totally use Khatex

Patrick Massot (Aug 28 2020 at 14:08):

I didn't think of it that way

Edward Ayers (Aug 28 2020 at 14:08):

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 (Aug 28 2020 at 14:12):

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

Patrick Massot (Aug 28 2020 at 14:12):

No, that's the old new mathjax

Patrick Massot (Aug 28 2020 at 14:12):

The new new mathjax is mathjax 3.0

Patrick Massot (Aug 28 2020 at 14:13):

But I'm not a specialist here.

Johan Commelin (Aug 28 2020 at 14:15):

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

Johan Commelin (Aug 28 2020 at 14:15):

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

Adam Topaz (Aug 28 2020 at 14:16):

Does mathjax 3 support tikz?!

Patrick Massot (Aug 28 2020 at 14:17):

No. plastex uses server-side tikz rendering.

Ah ok

Edward Ayers (Aug 28 2020 at 14:18):

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

Edward Ayers (Aug 28 2020 at 14:18):

That would be a game changer

Edward Ayers (Aug 28 2020 at 14:19):

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

Edward Ayers (Aug 28 2020 at 14:20):

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

Patrick Massot (Aug 28 2020 at 14:23):

It's probably pretty slow.

Bryan Gin-ge Chen (Aug 28 2020 at 15:24):

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

Patrick Massot (Aug 28 2020 at 15:37):

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

Edward Ayers (Aug 28 2020 at 15:54):

I don't think so.

Edward Ayers (Aug 28 2020 at 15:55):

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

Patrick Massot (Aug 28 2020 at 15:56):

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 (Aug 28 2020 at 15:58):

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 (Aug 28 2020 at 15:59):

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

Johan Commelin (Aug 28 2020 at 16:44):

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

Scott Morrison (Aug 28 2020 at 23:51):

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 (Aug 28 2020 at 23:52):

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 (Aug 29 2020 at 07:56):

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

Scott Morrison (Aug 29 2020 at 10:11):

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.

Last updated: May 14 2021 at 22:15 UTC