Zulip Chat Archive

Stream: general

Topic: widget for diagrams


Johan Commelin (Aug 18 2020 at 06:29):

What do we need to do, to write a widget that turns

pullback.fst  pullback.fst  ex1  x.hom  pullback.snd = pullback.snd  pullback.snd  ey2  y.hom  pullback.snd

into a beautifully rendered diagram?

Scott Morrison (Aug 18 2020 at 06:32):

and then drag and drop to fill in commutative cells?

Johan Commelin (Aug 18 2020 at 06:33):

Well, that would be a follow-up feature.

Johan Commelin (Aug 18 2020 at 06:34):

But just displaying the diagram would be a first step

Johan Commelin (Aug 18 2020 at 06:34):

Now I need to grab pen and paper to be able to figure out what the next step is. And that feels like defeat to me.

Markus Himmel (Aug 18 2020 at 06:44):

Rendering a diagram is certainly possible using a widget that emits inline svg. Rendering a beautiful diagram is another matter entirely, since graph drawing is a difficult problem.

Johan Commelin (Aug 18 2020 at 06:47):

Maybe, if we use D3, we can let the user push around the nodes?

Johan Commelin (Aug 18 2020 at 06:48):

That would already be really nice

Markus Himmel (Aug 18 2020 at 07:56):

Hmm.. I seems like script tags emitted by widgets don't get executed :/

Johan Commelin (Aug 18 2020 at 08:09):

That means we can't have custom interactions?

Johan Commelin (Aug 18 2020 at 08:09):

I understand the security risk...

Johan Commelin (Aug 18 2020 at 08:10):

Time to fork VScode rofl?

Gabriel Ebner (Aug 18 2020 at 08:10):

It's enough to change the extension.

Gabriel Ebner (Aug 18 2020 at 08:10):

PRs to enable the remote code execution are welcome.

Gabriel Ebner (Aug 18 2020 at 08:11):

But maybe @Edward Ayers has some thoughts on this as well.

Eric Wieser (Aug 18 2020 at 09:02):

Which part of the vs-code extension currently forbids script tags?

Gabriel Ebner (Aug 18 2020 at 09:04):

It's not forbidden. In fact, we already use <script> to include react, the infoview javascript, etc. It's just that the script tags in the widgets are not rendered as script tags apparently.

Gabriel Ebner (Aug 18 2020 at 09:05):

This is the code that renders the widget:
https://github.com/leanprover/vscode-lean/blob/f30589f89c3a1c7d95b160eb0b42ad25cc0527d2/infoview/widget.tsx#L173

Chris Wong (Aug 18 2020 at 09:08):

Related: https://stackoverflow.com/q/40989629/617159

Eric Wieser (Aug 18 2020 at 09:08):

Looks like it's possible by setting the dangerouslySetInnerHTML attribute to a string like <script>...</script>

Chris Wong (Aug 18 2020 at 09:09):

It looks like the issue is that script tags don't appear in the DOM

Chris Wong (Aug 18 2020 at 09:10):

So React has no way of seeing whether the tag has already been inserted beforehand

Alex Peattie (Aug 18 2020 at 10:49):

My instinct is that sending a <script> tag from Lean and injecting it into VSCode wouldn't be the best way to go :upside_down:. If I understand the way that widgets work currently, the Lean server sends some HTML back to VSCode which is then rendered by VSCode with fairly minimal post-processing.

For a diagrammatic widget, the best best would probably to send back something simple that VSCode can post-process, e.g. the Lean server sends:

<span class='widget widget-diagram'>
  digraph {
    a -> b;
    b -> c;
    c -> d;
    d -> a;
  }
</span>

And VSCode could then use any Graphviz compatible library (i.e. D3) to render the corresponding image.

Markus Himmel (Aug 18 2020 at 11:27):

Sure, but then you need to change the Lean server and/or the VS code extension for every visualization. I was hoping for something that can live in mathlib.

Alex Peattie (Aug 18 2020 at 11:40):

If I'm understanding right I don't think the Lean server would need to be changed, as I think the changes could go into tactic/interactive_expr.lean? You're right about needing VSCode changes, but unfortunately injecting a <script> tag inside of React, inside of a VSCode extension will really be a nightmare. (Especially because VSCode extensions are a sort of subprocess inside VSCode as well). For example, the <script> is likely to mess with React's rendering cycle, unless it's specifically rendered with React in mind...

Edward Ayers (Aug 18 2020 at 17:45):

Yeah I've been thinking about how to support 3rd party javascript libraries and I don't have any watertight ideas. There are two problems; how to specify which libraries you want (eg give some cdn addresses for D3, Katex etc), the second problem is figuring out how to get the lean widgets system to talk to it, because eg D3 relies on the developer being able to write some script, but atm widgets can only make some static html with simple event handlers.

Adding dangerouslySetInnerHTML with scripts won't work atm but I don't think it's as hacky as it sounds. The lean code is already trusted, eg it can meddle with the file system etc so having it be able to insert arbitrary scripts doesn't seem that bad. The problem is that dangerouslySetInnerHTML takes a JS object as an argument rather than a string, so some C++ would need to change. Even then, the script might be removed from the DOM when a rerender takes place which might be bad.

One idea: in lean you can write some html or javascript as a string and then you can pass it to vscode to insert statically before any widgets start rendering. There would still be a bit of work to get something like D3 working but you could then do it in principle. This would also solve some of the requests for people wanting to add their CSS to the infoview.

Edward Ayers (Aug 18 2020 at 17:51):

Also svg should just work (tm):

h "svg" [attr.val "height" "100", attr.val "width" "100"] [
     h "circle"
       [ attr.val "cx" "50"
       , attr.val "cy" "50"
       , attr.val "r" "40"
       , attr.val "stroke" "black"
       , attr.val "strokeWidth" "3"
       , attr.val "fill" "red"
       ] []
]

Edward Ayers (Aug 18 2020 at 17:52):

So another approach would be to write a whole diagram rendering library in Lean

Edward Ayers (Aug 18 2020 at 17:52):

How hard can it be?

Edward Ayers (Aug 18 2020 at 17:54):

I deffo want to support KaTeX ootb at some point though.

Alex Peattie (Aug 18 2020 at 18:03):

Edward Ayers said:

One idea: in lean you can write some html or javascript as a string and then you can pass it to vscode to insert statically before any widgets start rendering. There would still be a bit of work to get something like D3 working but you could then do it in principle. This would also solve some of the requests for people wanting to add their CSS to the infoview.

I think the main blocker for this approach currently would be the fact that the Infoview uses React - React doesn't really like anyone controlling the DOM tree apart from itself... For example you can see here the sort of contortions you usually have to do to get D3 to work in a React context (basically you get D3 to write a "faux DOM" first rather than inserting things on the page directly). The Infoview could be rewritten to just use plain JS, which would make it much easier to have 3rd party scripts change things in the infoview.

Alex Peattie (Aug 18 2020 at 18:03):

Yet another idea (if the main goal is visualizations in the short term) could be to extend VSCode to support a visualization grammar like Vega Lite or Penrose...

Alex Peattie (Aug 18 2020 at 18:03):

Edward Ayers said:

I deffo want to support KaTeX ootb at some point though.

That would be cool, I see there's an open PR to add commutative diagrams to KaTeX too :grinning:

Bryan Gin-ge Chen (Aug 18 2020 at 18:47):

One thought is that maybe the VS Code extension could support plugging in other JS apps that talk to the Lean server in place of the info view. Or possibly the info view should support passing messages to some other webview panel with other JS / HTML code.


Last updated: Dec 20 2023 at 11:08 UTC