widget for diagrams

Stream: general

[Johan Commelin]

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]

and then drag and drop to fill in commutative cells?

[Johan Commelin]

Well, that would be a follow-up feature.

[Johan Commelin]

But just displaying the diagram would be a first step

[Johan Commelin]

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]

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]

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

[Johan Commelin]

That would already be really nice

[Markus Himmel]

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

[Johan Commelin]

That means we can't have custom interactions?

[Johan Commelin]

I understand the security risk...

[Johan Commelin]

Time to fork VScode rofl?

[Gabriel Ebner]

It's enough to change the extension.

[Gabriel Ebner]

PRs to enable the remote code execution are welcome.

[Gabriel Ebner]

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

[Eric Wieser]

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

[Gabriel Ebner]

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]

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

[Chris Wong]

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

[Eric Wieser]

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

[Chris Wong]

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

[Chris Wong]

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

[Alex Peattie]

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]

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]

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]

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]

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]

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

[Edward Ayers]

How hard can it be?

[Edward Ayers]

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

[Alex Peattie]

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]

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]

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]

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.