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

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instToJsonBaseLibrary : Lean.ToJson BaseLibrary

Equations

• ImportGraph.Lake.instToJsonBaseLibrary = { toJson := ImportGraph.Lake.instToJsonBaseLibrary.toJson }

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

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instFromJsonBaseLibrary : Lean.FromJson BaseLibrary

Equations

• ImportGraph.Lake.instFromJsonBaseLibrary = { fromJson? := ImportGraph.Lake.instFromJsonBaseLibrary.fromJson }

@[instance_reducible]

instance ImportGraph.Lake.instReprBaseLibrary : Repr BaseLibrary

Equations

• ImportGraph.Lake.instReprBaseLibrary = { reprPrec := ImportGraph.Lake.instReprBaseLibrary.repr }

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

Equations

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

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

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instBEqBaseLibrary : BEq BaseLibrary

Equations

• ImportGraph.Lake.instBEqBaseLibrary = { beq := ImportGraph.Lake.instBEqBaseLibrary.beq }

@[instance_reducible]

instance ImportGraph.Lake.instInhabitedBaseLibrary : Inhabited BaseLibrary

Equations

• ImportGraph.Lake.instInhabitedBaseLibrary = { default := ImportGraph.Lake.instInhabitedBaseLibrary.default }

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.

@[instance_reducible]

instance ImportGraph.Lake.instToJsonBasePackage : Lean.ToJson BasePackage

Equations

• ImportGraph.Lake.instToJsonBasePackage = { toJson := ImportGraph.Lake.instToJsonBasePackage.toJson }

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

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instFromJsonBasePackage : Lean.FromJson BasePackage

Equations

• ImportGraph.Lake.instFromJsonBasePackage = { fromJson? := ImportGraph.Lake.instFromJsonBasePackage.fromJson }

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

Equations

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

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

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instReprBasePackage : Repr BasePackage

Equations

• ImportGraph.Lake.instReprBasePackage = { reprPrec := ImportGraph.Lake.instReprBasePackage.repr }

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

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instBEqBasePackage : BEq BasePackage

Equations

• ImportGraph.Lake.instBEqBasePackage = { beq := ImportGraph.Lake.instBEqBasePackage.beq }

@[instance_reducible]

instance ImportGraph.Lake.instInhabitedBasePackage : Inhabited BasePackage

Equations

• ImportGraph.Lake.instInhabitedBasePackage = { default := ImportGraph.Lake.instInhabitedBasePackage.default }

def ImportGraph.Lake.toolchainPrefix : Lean.Name

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

Equations

• ImportGraph.Lake.toolchainPrefix = `toolchain

@[inline]

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

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

Equations

• ImportGraph.Lake.toolchainName githash = ImportGraph.Lake.toolchainPrefix.str githash

@[inline]

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

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

Equations

• ImportGraph.Lake.isToolchainName (base.str str) = (base == ImportGraph.Lake.toolchainPrefix)
• ImportGraph.Lake.isToolchainName n = false

@[inline]

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

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

Equations

• ImportGraph.Lake.versionOfToolchainName? (base.str str) = do guard ((base == ImportGraph.Lake.toolchainPrefix) = true) some (Lake.ToolchainVer.ofString str)
• ImportGraph.Lake.versionOfToolchainName? n = none

@[instance_reducible]

instance ImportGraph.Lake.instInhabitedToolchainVer_importGraph : Inhabited Lake.ToolchainVer

Equations

• ImportGraph.Lake.instInhabitedToolchainVer_importGraph = { default := ImportGraph.Lake.instInhabitedToolchainVer_importGraph.default }

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.

@[instance_reducible]

instance ImportGraph.Lake.instToJsonBaseWorkspace : Lean.ToJson BaseWorkspace

Equations

• ImportGraph.Lake.instToJsonBaseWorkspace = { toJson := ImportGraph.Lake.instToJsonBaseWorkspace.toJson }

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

Equations

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

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

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instFromJsonBaseWorkspace : Lean.FromJson BaseWorkspace

Equations

• ImportGraph.Lake.instFromJsonBaseWorkspace = { fromJson? := ImportGraph.Lake.instFromJsonBaseWorkspace.fromJson }

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

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instReprBaseWorkspace : Repr BaseWorkspace

Equations

• ImportGraph.Lake.instReprBaseWorkspace = { reprPrec := ImportGraph.Lake.instReprBaseWorkspace.repr }

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

Equations

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

@[instance_reducible]

instance ImportGraph.Lake.instBEqBaseWorkspace : BEq BaseWorkspace

Equations

• ImportGraph.Lake.instBEqBaseWorkspace = { beq := ImportGraph.Lake.instBEqBaseWorkspace.beq }

@[instance_reducible]

instance ImportGraph.Lake.instInhabitedBaseWorkspace : Inhabited BaseWorkspace

Equations

• ImportGraph.Lake.instInhabitedBaseWorkspace = { default := ImportGraph.Lake.instInhabitedBaseWorkspace.default }