inductive Lake.BuildKey : Type

The type of keys in the Lake build store.

• module (module : Lean.Name) : BuildKey
• package (package : Lean.Name) : BuildKey
• packageModule (package module : Lean.Name) : BuildKey
• packageTarget (package target : Lean.Name) : BuildKey
• facet (target : BuildKey) (facet : Lean.Name) : BuildKey

@[implicit_reducible]

instance Lake.instInhabitedBuildKey : Inhabited BuildKey

def Lake.instInhabitedBuildKey.default : BuildKey

@[implicit_reducible]

instance Lake.instReprBuildKey : Repr BuildKey

def Lake.instReprBuildKey.repr : BuildKey → Nat → Std.Format

@[implicit_reducible]

instance Lake.instDecidableEqBuildKey : DecidableEq BuildKey

def Lake.instDecidableEqBuildKey.decEq (x✝ x✝¹ : BuildKey) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Lake.instHashableBuildKey : Hashable BuildKey

def Lake.instHashableBuildKey.hash : BuildKey → UInt64

def Lake.PartialBuildKey : Type

A build key with some missing info.

• Package names may be elided (replaced by Name.anonymous).
• Facet names are unqualified (they do not include the input target kind) and may also be ellided.

@[inline]

def Lake.PartialBuildKey.mk (key : BuildKey) : PartialBuildKey

Cast a BuildKey to a PartialBuildKey.

@[implicit_reducible]

instance Lake.PartialBuildKey.instCoeBuildKey : Coe BuildKey PartialBuildKey

@[implicit_reducible]

instance Lake.PartialBuildKey.instRepr : Repr PartialBuildKey

@[implicit_reducible]

instance Lake.PartialBuildKey.instInhabited : Inhabited PartialBuildKey

def Lake.PartialBuildKey.parse (s : String) : Except String PartialBuildKey

Parses a PartialBuildKey from a String. Uses the same syntax as the lake build / lake query CLI.

def Lake.PartialBuildKey.toString (self : PartialBuildKey) : String

@[implicit_reducible]

instance Lake.PartialBuildKey.instToString : ToString PartialBuildKey

@[reducible, match_pattern, inline, deprecated Lake.BuildKey.packageModuleFacet (since := "2025-11-13")]

abbrev Lake.BuildKey.moduleFacet (module facet : Lean.Name) : BuildKey

@[reducible, match_pattern, inline]

abbrev Lake.BuildKey.packageFacet (package facet : Lean.Name) : BuildKey

@[reducible, match_pattern, inline]

abbrev Lake.BuildKey.packageModuleFacet (package module facet : Lean.Name) : BuildKey

@[reducible, match_pattern, inline]

abbrev Lake.BuildKey.targetFacet (package target facet : Lean.Name) : BuildKey

@[reducible, match_pattern, inline]

abbrev Lake.BuildKey.customTarget (package target : Lean.Name) : BuildKey

def Lake.BuildKey.toString (self : BuildKey) : String

def Lake.BuildKey.toSimpleString (self : BuildKey) : String

Like the default toString, but without disambiguation markers.

@[implicit_reducible]

instance Lake.BuildKey.instToString : ToString BuildKey

def Lake.BuildKey.quickCmp (k k' : BuildKey) : Ordering

theorem Lake.BuildKey.eq_of_quickCmp {k k' : BuildKey} : k.quickCmp k' = Ordering.eq → k = k'

instance Lake.BuildKey.instLawfulEqCmpQuickCmp : Std.LawfulEqCmp quickCmp