import probe

Stream: general

[Yaël Dillies]

Could we have a page on the website that allows to

• check whether file A imports file B
• determine all the imports of a file
• determine all the files importing a file
  ?
  This is an extension of the idea of having a page reporting the import stats of all files in a table, similar to the contribution table.

[Floris van Doorn]

It's right there on the top-right of the mathlib documentation pages image.png

[Floris van Doorn]

you want all this information on a single page?

[Yaël Dillies]

No, I mean all imports, not just the direct ones.

[Yaël Dillies]

This is really to better grasp the library's architecture, quickly check for (accidentally introduced) cyclic imports, and know where we can put results that we want in a specific file.

[Scott Morrison]

The list of all imports quickly gets extremely large, and as an unstructured list is going to be very hard to understand.

[Scott Morrison]

You know about leanproject import-graph?

[Yaël Dillies]

Eheh, not really! I should probably look into that.

[Scott Morrison]

I prefer to output pdf. The output is just barely comprehensible. :-)

[Eric Wieser]

It would be really cool to get a d3js visualization of the import graph in doc-gen

[Eric Wieser]

The data is all there, but it's really hard to know how to show it

[Patrick Massot]

The full graph is too big to be legible

[Eric Wieser]

Showing 3 levels of ancestors and three levels of descendants would probably be legible

[Patrick Massot]

If you want to play with this then we already have all pieces (either in leanproject or in lean-blueprint)

[Alex J. Best]

I've been playing with this recently using webcola and clustering based on directory structure, as Patrick says it's very annoying to try and lay things out in a legible way, but I hope a useful tool is possible, at least something that can allow local exploration