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.

Equations

• ImportGraph.PackageBitset = ImportGraph.Shake.Bitset

@[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.

Equations

• ImportGraph.LibraryBitset = ImportGraph.Shake.Bitset

@[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).

Equations

• ImportGraph.ModuleBitset = ImportGraph.Shake.Bitset

@[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.

Equations

• ImportGraph.LibIdx = Nat

@[reducible, inline]

abbrev ImportGraph.PkgIdx : Type

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

Equations

• ImportGraph.PkgIdx = Nat

@[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.

Equations

• ImportGraph.ModIdx = Nat

structure ImportGraph.WorkspaceModel.Packageextends 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

Equations

• ImportGraph.WorkspaceModel.instReprPackage = { reprPrec := ImportGraph.WorkspaceModel.instReprPackage.repr }

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• ImportGraph.WorkspaceModel.instBEqPackage.beq x✝¹ x✝ = false

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instBEqPackage : BEq Package

Equations

• ImportGraph.WorkspaceModel.instBEqPackage = { beq := ImportGraph.WorkspaceModel.instBEqPackage.beq }

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instInhabitedPackage : Inhabited Package

Equations

• ImportGraph.WorkspaceModel.instInhabitedPackage = { default := ImportGraph.WorkspaceModel.instInhabitedPackage.default }

structure ImportGraph.WorkspaceModel.Libraryextends 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

Equations

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

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instReprLibrary : Repr Library

Equations

• ImportGraph.WorkspaceModel.instReprLibrary = { reprPrec := ImportGraph.WorkspaceModel.instReprLibrary.repr }

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

Equations

• One or more equations did not get rendered due to their size.
• ImportGraph.WorkspaceModel.instBEqLibrary.beq x✝¹ x✝ = false

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instBEqLibrary : BEq Library

Equations

• ImportGraph.WorkspaceModel.instBEqLibrary = { beq := ImportGraph.WorkspaceModel.instBEqLibrary.beq }

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instInhabitedLibrary : Inhabited Library

Equations

• ImportGraph.WorkspaceModel.instInhabitedLibrary = { default := ImportGraph.WorkspaceModel.instInhabitedLibrary.default }

structure ImportGraph.WorkspaceModel.Moduleextends 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

Equations

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

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instReprModule : Repr Module

Equations

• ImportGraph.WorkspaceModel.instReprModule = { reprPrec := ImportGraph.WorkspaceModel.instReprModule.repr }

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instInhabitedModule : Inhabited Module

Equations

• ImportGraph.WorkspaceModel.instInhabitedModule = { default := ImportGraph.WorkspaceModel.instInhabitedModule.default }

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

Equations

• ImportGraph.WorkspaceModel.instReprError = { reprPrec := ImportGraph.WorkspaceModel.instReprError.repr }

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

Equations

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

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instInhabitedError : Inhabited Error

Equations

• ImportGraph.WorkspaceModel.instInhabitedError = { default := ImportGraph.WorkspaceModel.instInhabitedError.default }

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

Equations

• One or more equations did not get rendered due to their size.
• ImportGraph.WorkspaceModel.instToJsonError.toJson (ImportGraph.WorkspaceModel.Error.noLibOfModule a) = Lean.Json.mkObj [("noLibOfModule", Lean.Json.mkObj [("mod", Lean.toJson a)])]

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instToJsonError : Lean.ToJson Error

Equations

• ImportGraph.WorkspaceModel.instToJsonError = { toJson := ImportGraph.WorkspaceModel.instToJsonError.toJson }

@[instance_reducible]

instance ImportGraph.WorkspaceModel.instFromJsonError : Lean.FromJson Error

Equations

• ImportGraph.WorkspaceModel.instFromJsonError = { fromJson? := ImportGraph.WorkspaceModel.instFromJsonError.fromJson }

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

Equations

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

@[instance_reducible]

instance ImportGraph.instToMessageDataError : Lean.ToMessageData WorkspaceModel.Error

Equations

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

structure ImportGraph.WorkspaceModelextends 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.

@[instance_reducible]

instance ImportGraph.instReprWorkspaceModel : Repr WorkspaceModel

Equations

• ImportGraph.instReprWorkspaceModel = { reprPrec := ImportGraph.instReprWorkspaceModel.repr }

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

Equations

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

@[instance_reducible]

instance ImportGraph.instInhabitedWorkspaceModel : Inhabited WorkspaceModel

Equations

• ImportGraph.instInhabitedWorkspaceModel = { default := ImportGraph.instInhabitedWorkspaceModel.default }

@[inline]

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

Whether errors have been produced when creating the WorkspaceModel.

Equations

• w.hasErrors = !w.errors.isEmpty

@[inline]

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

Whether the WorkspaceModel contains the given module.

Equations

• ImportGraph.WorkspaceModel.hasModule mod w = w.idxOfMod.contains mod

Lookups

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

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

Equations

• m.toolchainPkgIdx = m.packages.size - 1

@[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.

Equations

• m.getModIdx? mod = m.idxOfMod[mod]?

@[inline]

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

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

Equations

• m.getPkgIdx? origName = Array.findIdx? (fun (x : ImportGraph.WorkspaceModel.Package) => x.origName == origName) m.packages

@[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.)

Equations

• m.getLibIdx? pkgIdx libName = Array.findIdx? (fun (lib : ImportGraph.WorkspaceModel.Library) => lib.pkgIdx == pkgIdx && lib.name == libName) m.libs

@[inline]

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

Equations

• m.getMod! modIdx = m.mods[modIdx]!

@[inline]

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

Equations

• m.getLib! libIdx = m.libs[libIdx]!

@[inline]

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

Equations

• m.getPkg! pkgIdx = m.packages[pkgIdx]!

@[inline]

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

Equations

• m.libOfMod! mod = m.getLib! mod.libIdx

@[inline]

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

Equations

• m.pkgOfMod! mod = m.getPkg! mod.pkgIdx

@[inline]

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

Equations

• m.pkgOfLib! lib = m.getPkg! lib.pkgIdx

@[inline]

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

Equations

• m.libIdxOfModIdx! modIdx = (m.getMod! modIdx).libIdx

@[inline]

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

Equations

• m.pkgIdxOfModIdx! modIdx = (m.getMod! modIdx).pkgIdx

@[inline]

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

Equations

• m.pkgIdxOfLibIdx! libIdx = (m.getLib! libIdx).pkgIdx

@[inline]

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

Equations

• m.libOfModIdx! modIdx = m.getLib! (m.libIdxOfModIdx! modIdx)

@[inline]

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

Equations

• m.pkgOfModIdx! modIdx = m.getPkg! (m.pkgIdxOfModIdx! modIdx)

@[inline]

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

Equations

• m.pkgOfLibIdx! libIdx = m.getPkg! (m.pkgIdxOfLibIdx! libIdx)

@[inline]

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

Equations

• m.libDepth! modIdx libIdx = (m.getMod! modIdx).depthsPerLib[libIdx]!

@[inline]

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

Equations

• m.pkgDepth! modIdx pkgIdx = (m.getMod! modIdx).depthsPerPkg[pkgIdx]!

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.

Equations

• l.isLocalModule mod = ((l.roots.any fun (x : Lean.Name) => x.isPrefixOf mod) || l.globs.any fun (x : Lake.Glob) => Lake.Glob.matches mod x)

@[inline]

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

Equations

• ImportGraph.WorkspaceModel.rawLibIdxOfMod? libs mod = Array.findIdx? (fun (x : ImportGraph.WorkspaceModel.Library) => x.isLocalModule mod) libs

@[inline]

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

Equations

• m.libIdxOfMod? mod = Array.findIdx? (fun (x : ImportGraph.WorkspaceModel.Library) => x.isLocalModule mod) m.libs

@[inline]

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

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

Equations

• ImportGraph.WorkspaceModel.Module.leanLibFile m mod ext = Lean.modToFilePath (m.pkgOfMod! mod).leanLibDir mod.name ext

@[inline]

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

Equations

• lib.srcPathOfMod mod = Lean.modToFilePath lib.srcDir mod "lean"

@[inline]

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

Equations

• m.srcPathOfMod? mod = Option.map (fun (x : ImportGraph.LibIdx) => Lean.modToFilePath m.libs[x]!.srcDir mod "lean") (m.libIdxOfMod? mod)

@[inline]

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

Equations

• ImportGraph.WorkspaceModel.Module.srcPath m mod = Lean.modToFilePath (m.libOfMod! mod).srcDir mod.name "lean"