A widget to display output from `dot`

Stream: lean4

[Bhavik Mehta]

I just wrote some lean code which can turn a (finite, decidable) simple graph into a format that dot can handle. Is there a way that can render this in the infoview? Alternatively, is there a way we can render graphs in some other way, maybe using d3.js?

[Anand Rao Tadipatri]

The RB tree demo in ProofWidgets uses d3-tree to render a red-black tree in the infoview (the corresponding Lean file is here).

Widgets can take in JSON-encodable data on the Lean side and then process and render them on the TypeScript/JavaScript side.

[Bhavik Mehta]

Oh that's embarrassing, I'd already seen that one. Thanks for the reminder!!

[Kevin Buzzard]

@Katja Berčič was rendering graphs in the infoview in her talk in Bonn last week

[Adam Topaz]

@Bhavik Mehta there is a draft PR open in the proofwidgets repo that renders graphs with d3-graphviz

[Bhavik Mehta]

https://github.com/leanprover-community/ProofWidgets4/pull/60 to save other people from searching

[Adam Topaz]

I wrote it with the intention of showing dependencies between lean decls, but the graph widget itself takes a dot file as a string as input

[Katja Berčič]

Kevin Buzzard said:

Katja Berčič was rendering graphs in the infoview in her talk in Bonn last week

@Jure Taslak implemented the graph rendering in the infoview, in case that helps.

[Joseph Tooby-Smith]

I'm struggling to work out the current status of this.
I have a string which corresponds to a valid dot-file. Is there currently an easy way I can display this in the infoview?

[Adam Topaz]

As far as I know, @Joseph Tooby-Smith the PR is still open in the proofwidgets repo, so you would have to use the branch of that PR if you want to play around with this. That same branch has a demo illustrating usage. For unrelated reasons I am now also interested in getting some variant of this PR merged, if at all possible. @Wojciech Nawrocki what do you think?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Ah, my apologies, I totally forgot about this. I will make it a priority to merge this.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hi everyone, I just added a very customizable (and possibly somewhat overengineered) DigraphDisplay component here. It will be available in ProofWidgets v0.0.44. For example $K_{10}$ with one choice of layout looks like this.

The component does not support dot: you just pass it an array of vertices and edges instead, and layout is computed with a force simulation from d3.js. I have found that d3-graphviz looks quite out of place in the infoview: it does not fit, and does not dynamically adapt to the available space. If there is a strong need to support dot descriptions, we could revisit this choice.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

This is now in mathlib, and you can also try it out in the web editor :)

[Patrick Massot]

Does anyone see the node labels in the web editor? I don’t see them.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Patrick Massot said:

Does anyone see the node labels in the web editor? I don’t see them.

That's because none most of the nodes in the examples don't have label text! The 'labels' are just the circles. You can add text labels if you like, though.

[Patrick Massot]

Then where is the xyz from line 58 meant to show up for instance?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Patrick Massot said:

Then where is the xyz from line 58 meant to show up for instance?

Oh sorry, I forgot about that one. That should have label text, and it's not showing up because the web editor infoview is not up to date. It works in VSCode.

[Patrick Massot]

I can confirm it works for me in VSCode!

[Patrick Massot]

Would you have an example for more “rigid” graphs, like a commutative diagram, or printing an Expr as a tree?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Patrick Massot said:

Would you have an example for more “rigid” graphs, like a commutative diagram, or printing an Expr as a tree?

Not quite an Expr-tree, but @Adam Topaz wrote one for all the constants appearing in a term: demo.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

And I have commutative diagrams locally. They look a bit funny so that we can squeeze them into the available space: Screenshot 2024-11-08 at 12.08.12 PM.png

[Adam Topaz]

The original demo I wrote in that old proofwidgets PR allowed you to click on nodes to display additional info. Is that feature still available with your new approach @Wojciech Nawrocki ?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Adam Topaz said:

The original demo I wrote in that old proofwidgets PR allowed you to click on nodes to display additional info. Is that feature still available with your new approach Wojciech Nawrocki ?

Ah, yes, I forgot to set that option. You need to add showDetails={true} to the GraphDisplay props. It's a bit broken in the web editor, but works in VSCode.