`lake graph`

[hargoniX]

As discussed previously in the Zulip it would be beneficial if Lake could output a graph representation of the dependencies it has discovered. In order to replace the Lake dependency in doc-gen4 it would need to contain:

• The git hash of the Lean compiler used for this library which is IMO technically a dependency (doc-gen checks if this is equivalent to its own and outputs a warning if compiler versions don't match up since this could cause ABI issues etc.)
• The git remote URLs of all dependencies
• A map from dependency name to the modules they contain

Furthermore it also requires:

• The contents of ws.root.srcDir and ws.leanSrcPath which I use to search the source files LeanInk should highlight.
• A way to obtain Lake's search path

but afaik those are already covered by lake print-paths

[kim-em]

This is not a lake level solution, of course, but some readers encountering this issue may find the lake exe graph provided in Mathlib suitable. (It could easily be extracted into a separate repo if anyone needs that.)