graphs

Stream: general

[Johan Commelin]

A long time ago, I have played with d3.js. But by now d3 has a new versions out and I've lost all my muscle memory. Is there anyone with experience with d3.js? It would be great if we could enhance our new community website with

• interactive import graphs
• interactive graph of the algebraic hierarchy

I can look into this myself, but wouldn't mind capitalising on expert knowledge in this fascinating community :stuck_out_tongue_wink: :grinning_face_with_smiling_eyes:

[Bryan Gin-ge Chen]

I have some experience with newer versions of D3. If you describe what you want (and help set up suitable JSON data for it) I can give it a shot.

[Johan Commelin]

Cool! I think we should add a json export to leanproject import-graph.

[Johan Commelin]

Besides that... I guess we should start with a simple force layout

[Johan Commelin]

But then, we probably want to be able to filter the graph to show subgraphs, similar to --from and --to.

[Bryan Gin-ge Chen]

That sounds pretty doable.

[Johan Commelin]

Maybe the option to fix a certain node to the center?

[Johan Commelin]

Generating a graph of the type class hierarchy should be similar, accept that we cannot simply reuse work on the leanproject side

[Johan Commelin]

Also, the type class hierarchy should probably not be a force layout, but a d3.hierarchy?

[Johan Commelin]

We could show the priority of instances along the edges of the graph.

[Bryan Gin-ge Chen]

These collections might be useful for inspiration: https://observablehq.com/collection/@d3/d3-hierarchy https://observablehq.com/collection/@d3/d3-force

[Johan Commelin]

The force directed tree looks nice: https://observablehq.com/@d3/force-directed-tree?collection=@d3/d3-force But I'm not sure if we can automatically decide what the clusters should be.

[Johan Commelin]

Also... the import graph is not a tree.

[Johan Commelin]

I guess that's the biggest problem

[Johan Commelin]

A treemap of the directory structure might also be a nice UI on top of the docs.

[Kenny Lau]

@Kevin Buzzard what's the graph in NNG?

[Kevin Buzzard]

No idea

[Johan Commelin]

It's also D3

[Kenny Lau]

cheers

[Bryan Gin-ge Chen]

There are notebooks where people play around with visualizing DAGs as well: https://observablehq.com/@peatroot/interacting-with-directed-acyclic-graphs https://observablehq.com/@nitaku/tangled-tree-visualization-ii https://observablehq.com/@erikbrinkman/d3-dag-sugiyama

[Kevin Buzzard]

@Mohammad Pedramfar did all that stuff for NNG

[Johan Commelin]

The layout above took 151 milliseconds to compute.

(From the third link of Bryan's post above. And that's with 21 nodes... :sad: )

[Johan Commelin]

@Bryan Gin-ge Chen I really like the first one! Where you can collapse part of the DAG, but you get dashed edges for remaining transitive dependencies.

[Patrick Massot]

I'm working on a similar problem for the sphere eversion project and I found that https://github.com/magjac/d3-graphviz is promising

[Patrick Massot]

I really hate those observablehq demo. I never know how to get from there to code I could copy-paste.

[Johan Commelin]

@Patrick Massot That seems a very useful library. I remember searching for things like that 2 years ago, but not finding anything

[Bryan Gin-ge Chen]

Yeah, you can click on the left to see the code, but it's all tangled together with the notebook runtime. Anyways, all I wanted to demonstrate was that the sky's the limit.

[Mohammad Pedramfar]

NNG uses a very simple implementation of force-directed directed acyclic graphs with d3. I haven't worked with d3 too much, but it seems to be quite powerful.