inductive Lake.BuildKey : Type

The type of keys in the Lake build store.

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

instance Lake.instInhabitedBuildKey : Inhabited BuildKey

instance Lake.instReprBuildKey : Repr BuildKey

instance Lake.instDecidableEqBuildKey : DecidableEq BuildKey

instance Lake.instHashableBuildKey : Hashable BuildKey

def Lake.PartialBuildKey.moduleTargetIndicator : Lean.Name

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.
• Module package targets are supported via a fake packageTarget with a target name ending in moduleTargetIndicator.

@[inline]

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

Cast a BuildKey to a 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.parse.parseTarget (s : String) : Except String PartialBuildKey

def Lake.PartialBuildKey.parse.parsePackageTarget (pkg : Lean.Name) (target : String) : Except String PartialBuildKey

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

instance Lake.instToStringPartialBuildKey : ToString PartialBuildKey

instance Lake.instReprPartialBuildKey : Repr PartialBuildKey

@[reducible, match_pattern, inline]

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

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.instLawfulCmpEqQuickCmp : LawfulCmpEq BuildKey quickCmp