Building a WorkspaceModel

This file builds a WorkspaceModel (the import hierarchy and other intradependencies) from a WorkspaceSummary (bare information about the lake workspace, such as library globs). This means traversing the modules for all packages and libraries and parsing their imports, then recording these relationships in the WorkspaceModel.

Future work

Functionality

• We could preserve shake annotations, as these are relevant to the hierarchy

Performance

• We could probably parallelize the import source reading.
• We could possibly hybridize with reading oleans when available instead of re-parsing imports.
• We could cache the component of the model for upstream packages more persistently, since those dependency graphs are (probably) not going to change
• We could consider bundling this all into the exe, and see if it's actually more performant to just push it all over json

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instHierarchy : Shake.Hierarchy WorkspaceModel

Equations

• One or more equations did not get rendered due to their size.

def ImportGraph.WorkspaceModel.mainToolchainLibs (withInit withLake : Bool := false) : Lean.NameSet

The "main" user-facing toolchain libraries, Lean and Std, with Init and Lake if their corresponding flags are true (false by default).

Equations

• One or more equations did not get rendered due to their size.

def ImportGraph.Lake.WorkspaceSummary.getToolchainLibs (ws : WorkspaceSummary) : IO (Array LibrarySummary)

Infers the toolchain's libraries (e.g. Lean, Lake, Init, Std, etc.).

Since lean toolchains do not ship with a lakefile, we infer the libraries obtained by looking for top-level directories and *.olean files in the toolchain's build directory (since there is only one build directory).

We model the library with synthetic globs that match the structure we found in the build directory, so that the model will at least accurately cover the real modules present, even if core's actual lakefile goes about building these differently (assuming core does not contain unbuilt modules, or modules apparently in one library that are actually built by another).

The source files live in either ws.lakeSrcDir or ws.leanSrcDir. We match the stem of anything we find from the build directory to the contents of both to figure out which one is the correct source directory for the given library.

Equations

• One or more equations did not get rendered due to their size.

def ImportGraph.Lake.WorkspaceSummary.toWorkspaceModel (ws : WorkspaceSummary) (extraMods : Array Lean.Name := #[]) : IO WorkspaceModel

Compute a rich WorkspaceModel from a WorkspaceSummary. This iterates through all the modules and parses all imports, incorporating them into an import hierarchy. Any modules in extraMods are absorbed into the model as well.

Equations

• One or more equations did not get rendered due to their size.

opaque ImportGraph.WorkspaceModel.cacheRef : IO.Ref (Option WorkspaceModel)

An interactive cache for the WorkspaceModel.

def ImportGraph.getWorkspaceModel (extraMods : Array Lean.Name := #[]) (readInteractiveCache readPersistentCache : Bool := true) (cwd : Option System.FilePath := none) : IO WorkspaceModel

Gets the workspace model. This reads the workspaceModelCache IO.Ref if useCache := true (the default). Note that this does not perform validation. However, note that at least if the imports to the current file are changed, the file will be restarted. We do not yet guarantee validity of the cache in the case where adjacent file imports are changed.

Note that this also implicitly relies on the workspace summary json cache, but that cache does not contain module data and is validated (by getWorkspaceSummary).

Equations

• One or more equations did not get rendered due to their size.