A model of the Lake workspace

This file introduces WorkspaceModel, which carries all of the packages, lean_libs, and modules of the lake workspace, together with dependency arrows extracted from imports.

We use Bitsets when possible for efficiency. Note that every module lives in a flat Array, as does every library, regardless of what package or library it comes from. Relationships between modules, libraries, and packages are stored in each, \using the (unique, global) index of a given module/library/package as a proxy wherever possible.

The toolchain is recorded as a "pseudo-package" with four libraries (Std, Init, Lean, and Lake).

Future work

• We currently ignore lean_libs which are not default lake targets. We should instead simply record whether a given library is default or not, and handle that in downstream logic.
• There is likely room for performance improvement by e.g. not eagerly computing certain data.
• We currently ignore targets that are not lean_libs entirely.
• We could make the indexing system more typesafe. Currently ModIdx/LibIdx/PkgIdx are just abbrev's for Nat.

We build a WorkspaceModel from a WorkspaceSummary using getWorkspaceModel in ImportGraph.WorkspaceModel.Build. The WorkspaceSummary itself is extracted from an external call to a lake process which loads the workspace, then cached in the build folder.

@[reducible, inline]

abbrev ImportGraph.PackageBitset : Type

A Bitset whose bit positions are indices for a WorkspaceModel's indexed datatypes (e.g. WorkspaceModel.packages). These indices are PkgIdxs.

@[reducible, inline]

abbrev ImportGraph.LibraryBitset : Type

A Bitset whose bit positions are indices for a WorkspaceModel's indexed datatypes (e.g. WorkspaceModel.libs). These indices are LibIdxs.

@[reducible, inline]

abbrev ImportGraph.ModuleBitset : Type

A Bitset whose bit positions are indices for a WorkspaceModel's indexed datatypes (e.g. WorkspaceModel.mods). These indices are ModIdxs (not to be confused with ModuleIdxs).

@[reducible, inline]

abbrev ImportGraph.LibIdx : Type

The index of a lean_lib in a WorkspaceModel's Bitsets and Arrays. Caution: simply an abbrev for Nat.

@[reducible, inline]

abbrev ImportGraph.PkgIdx : Type

The index of a lake package in a WorkspaceModel's Bitsets and Arrays.

@[reducible, inline]

abbrev ImportGraph.ModIdx : Type

The index of a module in a WorkspaceModel's Bitsets and Arrays.

Note that this is not the same as a ModuleIdx in a given environment. However, both are presently defs for Nats, so use caution to avoid using one in place of the other.

structure ImportGraph.WorkspaceModel.Package extends ImportGraph.Lake.BasePackage : Type

One package of the model: a Lake package, or the toolchain pseudo-package (last; see the module docstring). All paths are absolute.

• baseName : Lean.Name
• origName : Lean.Name
• wsIdx : Nat
• dir : System.FilePath
• leanLibDir : System.FilePath
• deps : PackageBitset

  Dependency arrows: the package's direct dependencies, as resolved by Lake (plus the toolchain pseudo-package).

• libs : LibraryBitset

  Workspace relation: the libraries belonging to the package.

• mods : ModuleBitset

  Workspace relation: the modules belonging to the package (the union over libs).

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instReprPackage : Repr Package

def ImportGraph.WorkspaceModel.instReprPackage.repr : Package → Nat → Std.Format

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instBEqPackage : BEq Package

def ImportGraph.WorkspaceModel.instBEqPackage.beq : Package → Package → Bool

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instInhabitedPackage : Inhabited Package

structure ImportGraph.WorkspaceModel.Library extends ImportGraph.Lake.BaseLibrary : Type

One Lean library of the model, including the pseudo-libraries Init/Std/Lean/Lake of the toolchain pseudo-package.

• name : Lean.Name
• srcDir : System.FilePath
• roots : Array Lean.Name
• globs : Array Lake.Glob
• revealedDeps : LibraryBitset

  The libraries transitively imported by modules in this library. (May not contain its own index if no module in the library imports something from the library.)

• mods : ModuleBitset

  Relational: the enumerated modules contained in the library (found on disk under its roots/globs). Not necessarily everything that gets built when the library is built.

• pkgIdx : PkgIdx

  Relational: the package the library belongs to.

def ImportGraph.WorkspaceModel.instReprLibrary.repr : Library → Nat → Std.Format

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instReprLibrary : Repr Library

def ImportGraph.WorkspaceModel.instBEqLibrary.beq : Library → Library → Bool

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instBEqLibrary : BEq Library

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instInhabitedLibrary : Inhabited Library

structure ImportGraph.WorkspaceModel.Module extends Lean.ModuleHeader : Type

One module of the model. Modules enter the model by enumerating the source trees of a chosen set of libraries (see ImportGraph.WorkspaceModel.Build); imports of modules outside that enumeration remain visible in imports but have no bits anywhere.

• imports : Array Import
• isModule : Bool
• name : Lean.Name

  The module's name.

• srcFile : System.FilePath

  The module's source filepath (absolute).

• isPrelude : Bool

  Whether the module has the prelude keyword (and hence no implicit Init imports).

• transDeps : Shake.Provides

  Dependency arrows: Transitive dependencies in the module system.

• transLibDeps : LibraryBitset

  Dependency arrows: The transitively reachable libraries this module depends on. Does not necessarily include its own library.

• transPkgDeps : PackageBitset

  Dependency arrows: The transitively reachable packages this module depends on. Does not necessarily include its own package.

• prevs : ModuleBitset

  Dependency arrows: Every module that must be built before the current module.

• depthsPerLib : Array Nat

  Dependency statistic: Per library, the longest chain of modules from that library that must be built before building this modules, including this module. 0 indicates non-dependence on the library. The Array index is the library's LibIdx.

• depthsPerPkg : Array Nat

  Dependency statistic: Per package, the longest chain of modules from a given package that must be built before building this modules, including this module. 0 indicates non-dependence on the package. The Array index is the package's PkgIdx.

• libIdx : LibIdx

  Workspace relation: The library this module belongs to.

• pkgIdx : PkgIdx

  Workspace relation: the package the module belongs to. Redundant, but we store it here for convenience.

def ImportGraph.WorkspaceModel.instReprModule.repr : Module → Nat → Std.Format

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instReprModule : Repr Module

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instInhabitedModule : Inhabited Module

inductive ImportGraph.WorkspaceModel.Error : Type

Errors that may be produced when creating the WorkspaceModel.

• readImportsFailure (mod : Lean.Name) (modPath : System.FilePath) (ioError : IO.Error) : Error

  Failed to read the imports from a given file (possibly because we failed to locate the file).

• noLibOfModule (mod : Lean.Name) : Error

  The given module does not participate in a lean_lib.

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instReprError : Repr Error

def ImportGraph.WorkspaceModel.instReprError.repr : Error → Nat → Std.Format

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instInhabitedError : Inhabited Error

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instToJsonError : Lean.ToJson Error

def ImportGraph.WorkspaceModel.instToJsonError.toJson : Error → Lean.Json

def ImportGraph.WorkspaceModel.instFromJsonError.fromJson : Lean.Json → Except String Error

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instFromJsonError : Lean.FromJson Error

@[instance_reducible]

instance ImportGraph.instToMessageDataError : Lean.ToMessageData WorkspaceModel.Error

structure ImportGraph.WorkspaceModel extends ImportGraph.Lake.BaseWorkspace : Type

A model of the lake workspace, containing all packages, libraries, and modules and their relationships, as well as dependency arrows between them extracted from parsed source imports.

• dir : System.FilePath
• sysroot : System.FilePath
• leanLibDir : System.FilePath
• lakeSrcDir : System.FilePath
• leanSrcDir : System.FilePath
• version : Option Lake.ToolchainVer
• leanGitHash : String
• manifestFile : System.FilePath
• packages : Array Package

  The packages: Lake packages in Lake's order, with the toolchain "package" last. The index in this array is a PkgIdx and matches the index used in other package Arrays and PackageBitsets.

• libs : Array Library

  The libraries of all packages in package order (toolchain libraries last). The index of the library in this array is a LibIdx and matches its index in other library Arrays and LibraryBitsets.

• mods : Array Module

  The modules of all packages and libraries in some topological order, with imported modules coming first and the modules that import them afterwards. The index of a module in this array is a ModIdx and matches the index in other module Arrays and ModuleBitsets.

• idxOfMod : Std.HashMap Lean.Name ModIdx

  Module name → module index.

• errors : Array Error

  Errors collected when creating the workspace model.

def ImportGraph.instReprWorkspaceModel.repr : WorkspaceModel → Nat → Std.Format

@[instance_reducible]

instance ImportGraph.instReprWorkspaceModel : Repr WorkspaceModel

@[instance_reducible]

instance ImportGraph.instInhabitedWorkspaceModel : Inhabited WorkspaceModel

@[inline]

def ImportGraph.WorkspaceModel.hasErrors (w : WorkspaceModel) : Bool

Whether errors have been produced when creating the WorkspaceModel.

@[inline]

def ImportGraph.WorkspaceModel.hasModule (mod : Lean.Name) (w : WorkspaceModel) : Bool

Whether the WorkspaceModel contains the given module.

Lookups

def ImportGraph.WorkspaceModel.toolchainPkgIdx (m : WorkspaceModel) : PkgIdx

The index of the toolchain pseudo-package (the last package).

@[inline]

def ImportGraph.WorkspaceModel.getModIdx? (m : WorkspaceModel) (mod : Lean.Name) : Option ModIdx

The index of the module named mod, if it is in the model.

@[inline]

def ImportGraph.WorkspaceModel.getPkgIdx? (m : WorkspaceModel) (origName : Lean.Name) : Option PkgIdx

The index of the package with original name name, if any.

@[inline]

def ImportGraph.WorkspaceModel.getLibIdx? (m : WorkspaceModel) (pkgIdx : PkgIdx) (libName : Lean.Name) : Option LibIdx

The index of the library named name, if any. (Library names are not necessarily unique across packages, so we ask for the package index as well.)

@[inline]

def ImportGraph.WorkspaceModel.getMod! (m : WorkspaceModel) (modIdx : ModIdx) : Module

@[inline]

def ImportGraph.WorkspaceModel.getLib! (m : WorkspaceModel) (libIdx : LibIdx) : Library

@[inline]

def ImportGraph.WorkspaceModel.getPkg! (m : WorkspaceModel) (pkgIdx : PkgIdx) : Package

@[inline]

def ImportGraph.WorkspaceModel.libOfMod! (m : WorkspaceModel) (mod : Module) : Library

@[inline]

def ImportGraph.WorkspaceModel.pkgOfMod! (m : WorkspaceModel) (mod : Module) : Package

@[inline]

def ImportGraph.WorkspaceModel.pkgOfLib! (m : WorkspaceModel) (lib : Library) : Package

@[inline]

def ImportGraph.WorkspaceModel.libIdxOfModIdx! (m : WorkspaceModel) (modIdx : ModIdx) : LibIdx

@[inline]

def ImportGraph.WorkspaceModel.pkgIdxOfModIdx! (m : WorkspaceModel) (modIdx : ModIdx) : PkgIdx

@[inline]

def ImportGraph.WorkspaceModel.pkgIdxOfLibIdx! (m : WorkspaceModel) (libIdx : LibIdx) : PkgIdx

@[inline]

def ImportGraph.WorkspaceModel.libOfModIdx! (m : WorkspaceModel) (modIdx : ModIdx) : Library

@[inline]

def ImportGraph.WorkspaceModel.pkgOfModIdx! (m : WorkspaceModel) (modIdx : ModIdx) : Package

@[inline]

def ImportGraph.WorkspaceModel.pkgOfLibIdx! (m : WorkspaceModel) (libIdx : LibIdx) : Package

@[inline]

def ImportGraph.WorkspaceModel.libDepth! (m : WorkspaceModel) (modIdx : ModIdx) (libIdx : LibIdx := m.libIdxOfModIdx! modIdx) : Nat

@[inline]

def ImportGraph.WorkspaceModel.pkgDepth! (m : WorkspaceModel) (modIdx : ModIdx) (pkgIdx : PkgIdx := m.pkgIdxOfModIdx! modIdx) : Nat

Lake lifts

This section contains lifts of basic lake functions (usually of the same name) to WorkspaceModel.

@[inline]

def ImportGraph.WorkspaceModel.Library.isLocalModule (l : Library) (mod : Lean.Name) : Bool

LeanLib.isLocalModule, but lifted to WorkspaceModel.Library.

@[inline]

def ImportGraph.WorkspaceModel.rawLibIdxOfMod? (libs : Array Library) (mod : Lean.Name) : Option LibIdx

@[inline]

def ImportGraph.WorkspaceModel.libIdxOfMod? (m : WorkspaceModel) (mod : Lean.Name) : Option LibIdx

@[inline]

def ImportGraph.WorkspaceModel.Module.leanLibFile (m : WorkspaceModel) (mod : Module) (ext : String) : System.FilePath

Like Lake.Module.leanLibFile, but for WorkspaceModel.Module.

@[inline]

def ImportGraph.WorkspaceModel.Library.srcPathOfMod (lib : Library) (mod : Lean.Name) : System.FilePath

@[inline]

def ImportGraph.WorkspaceModel.srcPathOfMod? (m : WorkspaceModel) (mod : Lean.Name) : Option System.FilePath

@[inline]

def ImportGraph.WorkspaceModel.Module.srcPath (m : WorkspaceModel) (mod : Module) : System.FilePath