leanprover-community/doc-gen#145 Graph links

Stream: PR reviews

[Eric Wieser]

leanprover-community/doc-gen#145 adds links to my import graph visualization with the current module highlighted, currently in the sidebar. The link is currently here, which looks a bit ugly:

image.png

Are people in favor of having this link? Do I need to move the graph project to the leanprover-community organization first? Any suggestions for placing the link somewhere less ugly?

[Yaël Dillies]

I am really excited about this kind of visualisation arriving (although I'm not quite satisfied with how it looks yet). Moving the project to leanprover-community sounds wise. I would also put the link right below source. They look like they belong together.

[Eric Wieser]

A related comment is that none of the links in that sidebar are visible on mobile; while that's fine for the alphabetic listing which is redundant anyway, it means the import information isn't accessible at all. Any ideas for where else to expose that info?