Zulip Chat Archive

Stream: general

Topic: khatex


view this post on Zulip 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?

view this post on Zulip Edward Ayers (Aug 28 2020 at 13:53):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Aug 28 2020 at 13:57):

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

view this post on Zulip Edward Ayers (Aug 28 2020 at 14:00):

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

view this post on Zulip Patrick Massot (Aug 28 2020 at 14:00):

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

view this post on Zulip Edward Ayers (Aug 28 2020 at 14:04):

well triaging is a different question...

view this post on Zulip Patrick Massot (Aug 28 2020 at 14:04):

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

view this post on Zulip Reid Barton (Aug 28 2020 at 14:07):

I would totally use Khatex

view this post on Zulip Patrick Massot (Aug 28 2020 at 14:08):

I didn't think of it that way

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 28 2020 at 14:12):

No, that's the old new mathjax

view this post on Zulip Patrick Massot (Aug 28 2020 at 14:12):

The new new mathjax is mathjax 3.0

view this post on Zulip Patrick Massot (Aug 28 2020 at 14:13):

But I'm not a specialist here.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 28 2020 at 14:15):

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

view this post on Zulip Adam Topaz (Aug 28 2020 at 14:16):

Does mathjax 3 support tikz?!

view this post on Zulip Patrick Massot (Aug 28 2020 at 14:17):

No. plastex uses server-side tikz rendering.

view this post on Zulip Adam Topaz (Aug 28 2020 at 14:18):

Ah ok

view this post on Zulip Edward Ayers (Aug 28 2020 at 14:18):

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

view this post on Zulip Edward Ayers (Aug 28 2020 at 14:18):

That would be a game changer

view this post on Zulip 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

view this post on Zulip Edward Ayers (Aug 28 2020 at 14:20):

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

view this post on Zulip Patrick Massot (Aug 28 2020 at 14:23):

It's probably pretty slow.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Aug 28 2020 at 15:54):

I don't think so.

view this post on Zulip Edward Ayers (Aug 28 2020 at 15:55):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Aug 28 2020 at 15:59):

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

view this post on Zulip Johan Commelin (Aug 28 2020 at 16:44):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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