lake icon indicating copy to clipboard operation
lake copied to clipboard

`lake graph`

Open hargoniX opened this issue 2 years ago • 0 comments

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

hargoniX avatar Jul 09 '22 11:07 hargoniX