lake
lake copied to clipboard
`lake graph`
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
andws.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