documentation: structure / class heirarchy

Stream: general

[Eric Wieser]

It would be great if there was some way to get a graphviz diagram of "everything that extends add_hom" or "everything extending has_add". Does this exist already?

[Johan Commelin]

Yup, in some form

[Johan Commelin]

Floris created some nice graphs for the mathlib paper from last year

[Johan Commelin]

And there is this PR, which turns his script into a JSON scraper https://github.com/leanprover-community/doc-gen/pull/52

[Johan Commelin]

But doing anything with it has been dormant for a while

[Bryan Gin-ge Chen]

Yeah, I promised to look at it months back but haven't gotten to it :/

[Johan Commelin]

No worries... it's not like I was waiting for it to get merged (-;
It's mostly there so that we don't loose the script.

[Eric Wieser]

What I was after:

digraph G {

  # defs added by inheritance, transitive edges pruned
  add_monoid_hom -> add_hom;
  add_monoid_hom -> zero_hom;
  add_equiv -> add_hom;
  add_equiv -> equiv;
  monoid_hom -> mul_hom;
  monoid_hom -> one_hom;
  mul_equiv -> mul_hom;
  mul_equiv -> equiv;
  ring_hom -> add_monoid_hom;
  ring_hom -> monoid_hom;
  ring_equiv -> add_equiv;
  ring_equiv -> mul_equiv;
  linear_map -> add_hom;
  linear_equiv -> add_equiv;
  linear_equiv -> linear_map;
  alg_hom -> ring_hom;
  alg_equiv -> ring_equiv;

  # defs added manually
  {
    edge [color=gray];
    alg_hom -> linear_map;
    ring_equiv -> ring_hom;
    add_equiv -> add_monoid_hom;
    mul_equiv -> monoid_hom;
    linear_map -> add_monoid_hom;
    alg_equiv -> linear_equiv;
    alg_equiv -> alg_hom;
  }
}

graphviz.svg