Basic Lake workspace data

This file defines the BaseWorkspace shared by both the WorkspaceSummary, which is transported as Json across a process boundary (extracted from loading the lake workspace), and the WorkspaceModel, which is computed from the WorkspaceSummary (but doesn't need some of its fields). See ImportGraph.WorkspaceModel.WorkspaceSummary and ImportGraph.WorkspaceModel.Model.

structure ImportGraph.Lake.BaseLibrary : Type

Basic data for a lean_lib.

• name : Lean.Name

  The library's name.

• srcDir : System.FilePath

  The directory relative to which the library's module names locate source files (absolute).

• roots : Array Lean.Name

  The library's root module names.

• globs : Array Lake.Glob

  The globs specifying the library's buildable modules.

def ImportGraph.Lake.instToJsonBaseLibrary.toJson : BaseLibrary → Lean.Json

@[instance_reducible]

instance ImportGraph.Lake.instToJsonBaseLibrary : Lean.ToJson BaseLibrary

def ImportGraph.Lake.instFromJsonBaseLibrary.fromJson : Lean.Json → Except String BaseLibrary

@[instance_reducible]

instance ImportGraph.Lake.instFromJsonBaseLibrary : Lean.FromJson BaseLibrary

@[instance_reducible]

instance ImportGraph.Lake.instReprBaseLibrary : Repr BaseLibrary

def ImportGraph.Lake.instReprBaseLibrary.repr : BaseLibrary → Nat → Std.Format

@[instance_reducible]

instance ImportGraph.Lake.instBEqBaseLibrary : BEq BaseLibrary

def ImportGraph.Lake.instBEqBaseLibrary.beq : BaseLibrary → BaseLibrary → Bool

@[instance_reducible]

instance ImportGraph.Lake.instInhabitedBaseLibrary : Inhabited BaseLibrary

structure ImportGraph.Lake.BasePackage : Type

Basic data for a lake package. All paths are absolute.

• baseName : Lean.Name

  The package's assigned name (Package.baseName).

• origName : Lean.Name

  The package's original name (Package.origName).

• wsIdx : Nat

  Lake's index for the package (Package.wsIdx) Together with baseName, this disambiguates packages.

• dir : System.FilePath

  The package's root directory (absolute).

• leanLibDir : System.FilePath

  The directory holding the package's compiled module artifacts (.oleans etc.), e.g. <dir>/.lake/build/lib/lean.

def ImportGraph.Lake.instToJsonBasePackage.toJson : BasePackage → Lean.Json

@[instance_reducible]

instance ImportGraph.Lake.instToJsonBasePackage : Lean.ToJson BasePackage

def ImportGraph.Lake.instFromJsonBasePackage.fromJson : Lean.Json → Except String BasePackage

@[instance_reducible]

instance ImportGraph.Lake.instFromJsonBasePackage : Lean.FromJson BasePackage

@[instance_reducible]

instance ImportGraph.Lake.instReprBasePackage : Repr BasePackage

def ImportGraph.Lake.instReprBasePackage.repr : BasePackage → Nat → Std.Format

def ImportGraph.Lake.instBEqBasePackage.beq : BasePackage → BasePackage → Bool

@[instance_reducible]

instance ImportGraph.Lake.instBEqBasePackage : BEq BasePackage

@[instance_reducible]

instance ImportGraph.Lake.instInhabitedBasePackage : Inhabited BasePackage

def ImportGraph.Lake.toolchainPrefix : Lean.Name

The prefix we use for modelling the Lean toolchain, which is simply toolchain.

@[inline]

def ImportGraph.Lake.toolchainName (githash : String) : Lean.Name

A Lean githash as a Name for uniquely identifying the Lean toolchain.

@[inline]

def ImportGraph.Lake.isToolchainName (n : Lean.Name) : Bool

Whether a name is of the form toolchain.<ver>.

@[inline]

def ImportGraph.Lake.versionOfToolchainName? (n : Lean.Name) : Option Lake.ToolchainVer

The ToolchainVer extracted from a name of the form toolchain.<ver>.

@[instance_reducible]

instance ImportGraph.Lake.instInhabitedToolchainVer_importGraph : Inhabited Lake.ToolchainVer

structure ImportGraph.Lake.BaseWorkspace : Type

The basic data of a Lake workspace shared by both the transported WorkspaceSummary and the rich, computed WorkspaceModel.

• dir : System.FilePath

  The workspace root directory (absolute).

• sysroot : System.FilePath

  The Lean toolchain's sysroot (absolute).

• leanLibDir : System.FilePath

  The Lean toolchain's directory for its oleans (absolute), usually {sysroot}/lib/lean/.

• lakeSrcDir : System.FilePath

  The Lean toolchain's lake source directory (absolute), usually {sysroot}/src/lean/lake/. Note that we should search here first for files, lest we confuse src/lean/lake/ with src/lean/Lake on case-insensitive filesystems.

• leanSrcDir : System.FilePath

  The Lean toolchain's lean source directory (absolute), usually {sysroot}/src/lean/. Note that we should search lakeSrcDir first for files, lest we confuse src/lean/lake/ with src/lean/Lake on case-insensitive filesystems.

• version : Option Lake.ToolchainVer

  The Lean toolchain's version, as read from the lean-toolchain file, if possible.

• leanGitHash : String

  The git hash of the lean version.

• manifestFile : System.FilePath

  The path to the lake manifest. Should be uniform, but is allowed to change in lake internals, so just in case.

def ImportGraph.Lake.instToJsonBaseWorkspace.toJson : BaseWorkspace → Lean.Json

@[instance_reducible]

instance ImportGraph.Lake.instToJsonBaseWorkspace : Lean.ToJson BaseWorkspace

def ImportGraph.Lake.instFromJsonBaseWorkspace.fromJson : Lean.Json → Except String BaseWorkspace

@[instance_reducible]

instance ImportGraph.Lake.instFromJsonBaseWorkspace : Lean.FromJson BaseWorkspace

@[instance_reducible]

instance ImportGraph.Lake.instReprBaseWorkspace : Repr BaseWorkspace

def ImportGraph.Lake.instReprBaseWorkspace.repr : BaseWorkspace → Nat → Std.Format

def ImportGraph.Lake.instBEqBaseWorkspace.beq : BaseWorkspace → BaseWorkspace → Bool

@[instance_reducible]

instance ImportGraph.Lake.instBEqBaseWorkspace : BEq BaseWorkspace

@[instance_reducible]

instance ImportGraph.Lake.instInhabitedBaseWorkspace : Inhabited BaseWorkspace