instance graphs

Stream: mathlib4

[Floris van Doorn]

As preparation for writing instance priority linters, I wrote some code to generate the current algebraic hierarchy as a graph.
Here is the full "algebraic hierarchy" of mathlib:

FullInstanceGraph.pdf

What are you looking at here?

• All nodes are classes with 1 explicit type argument (and potentially other type-class arguments). So not e.g. Module
• Solid edges are "forgetful" instances from a class to another class (either generated by the extends syntax or by a user). Instances that have multiple source classes are not displayed.
• Dashed edges are classes that have another class as argument (e.g. there is a dashed edge T0Space -> TopologicalSpace)
• Edges in the transitive closure are removed (e.g. there is no direct edge from T1Space -> TopologicalSpace)
• Classes without any edges are not displayed

If this is too overwhelming, here is a subgraph where we only take the classes with 1 argument (no other type-class arguments). That one is almost manageable!

PartialInstanceGraph.pdf

Code and output (in dot format) here: (this also contains all the instances with multiple sources, that are not as easily visualizable in a graph)

https://gist.github.com/fpvandoorn/c398ea0a926a8b4013344d4a45bf9bbb

You can use tred full.dot | dot -y -T pdf > full.pdf to generate the graphs (requires graphviz)

[Martin Dvořák]

Thanks a lot!

I just printed the smaller graph on A3. It is barely readable. I will try A2 if I get a chance.

[Martin Dvořák]

Can we please put those PDFs somewhere more visibly? I often search for it on Zulip and end up opening this thread over and over again.

[Martin Dvořák]

Also, how hard would it be to automatically generate a new version of the graph every week or so?

[Damiano Testa]

Now that there is a cron job running in CI, I am fairly confident that we could probably set something up that would produce these graphs regularly and post them, if this is something desirable.

[Damiano Testa]

Honestly, I kind of liked the progress reports during the port and I think that some regular, global information on the "status" of mathlib is certainly added value.

[Matthew Ballard]

Post to LinkedIn?

[Martin Dvořák]

Does anybody have a newer version?

[Martin Dvořák]

Running the script by @Floris van Doorn on current Mathlib gave me:
Mathlib_classes.svg

[Martin Dvořák]

As the graph above is overwhelmingly large, I also post a graph with basic algebraic classes only (in particular, LinearOrderedField and everything upstream):
Mathlib_LinearOrderedField.svg

[Scott Carnahan]

It looks like CommGroupWithZero has an arrow to CommMonoidWithZero but not CancelCommMonoidWithZero, and GroupWithZero has an arrow to MonoidWithZero but not CancelMonoidWithZero. Should this be changed?

[Yaël Dillies]

Looks like Martin didn't import Mathlib but merely import Mathlib.Algebra.Field.Defs

[Martin Dvořák]

Yes, I thought it would be an easy way out. It turns out I have all the definitional relationships, but not all relationships.

[Martin Dvořák]

What I would like to do is to import entire Mathlib but draw only relationships between classes down of LinearOrderedField. Unfortunately, I don't know any easy way how to write such a script.

[Martin Dvořák]

I shouldn't have uploaded the second graph here, but for me, the graph of LinearOrderedField is still useful as it is. In a technical report I'm writing with Vladimir Kolmogorov, I want to document the definition of LinearOrderedField and the graph helps me to find the classes I need to document first. In fact, a graph containing only the definitional relationships ("extends") would me the most useful thing for me.

[Martin Dvořák]

Since I didn't find a way how to automatically filter for is-defined-using relationships only, I made the graph for LinearOrderedField by hand by following only the extends edges and ignoring all FooCast classes.
algebraic_hierarchy.svg
Please note that this graph is likely to contain mistakes, as I didn't use any software that could spot errors.

[Ching-Tsun Chou]

Hi all, are the script(s) that generated the diagrams given above available somewhere?