def
ImportGraph.Lake.getWorkspaceSummary
(wsDir : Option System.FilePath := none)
(readCache : Bool := true)
:
Get the workspace summary by calling out to lake exe import-graph-workspace-summary, which emits
json that this function parses. (This is a workaround for the fact that loading the language server
in the language server causes a crash.)
Before calling out to the executable, this function checks a cache file in the .lake folder and
determines whether it's up-to-date. If so, it skips the executable call. If not, and it does call
out to the executable, then we also write the result to that cache file.
If readCache := false, do not read from the cache, but still write to it.
Equations
- One or more equations did not get rendered due to their size.