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

Equations

• Lake.instInhabitedBuildKey = { default := Lake.BuildKey.module default }

instance Lake.instReprBuildKey : Repr BuildKey

Equations

• Lake.instReprBuildKey = { reprPrec := Lake.reprBuildKey✝ }

instance Lake.instDecidableEqBuildKey : DecidableEq BuildKey

Equations

• Lake.instDecidableEqBuildKey = Lake.decEqBuildKey✝

instance Lake.instHashableBuildKey : Hashable BuildKey

Equations

• Lake.instHashableBuildKey = { hash := Lake.hashBuildKey✝ }

def Lake.PartialBuildKey.moduleTargetIndicator : Lean.Name

Equations

• Lake.PartialBuildKey.moduleTargetIndicator = `«_+»

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.

Equations

• Lake.PartialBuildKey = Lake.BuildKey

@[inline]

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

Cast a BuildKey to a PartialBuildKey.

Equations

• Lake.PartialBuildKey.mk key = key

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.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lake.PartialBuildKey.toString (Lake.BuildKey.module m) = toString "+" ++ toString m ++ toString ""
• Lake.PartialBuildKey.toString (Lake.BuildKey.package p) = if p.isAnonymous = true then "" else toString "@" ++ toString p ++ toString ""

instance Lake.instToStringPartialBuildKey : ToString PartialBuildKey

Equations

• Lake.instToStringPartialBuildKey = { toString := Lake.PartialBuildKey.toString }

instance Lake.instReprPartialBuildKey : Repr PartialBuildKey

Equations

• Lake.instReprPartialBuildKey = inferInstanceAs (Repr Lake.BuildKey)

@[reducible, match_pattern, inline]

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

Equations

• Lake.BuildKey.moduleFacet module facet = (Lake.BuildKey.module module).facet facet

@[reducible, match_pattern, inline]

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

Equations

• Lake.BuildKey.packageFacet package facet = (Lake.BuildKey.package package).facet facet

@[reducible, match_pattern, inline]

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

Equations

• Lake.BuildKey.targetFacet package target facet = (Lake.BuildKey.packageTarget package target).facet facet

@[reducible, match_pattern, inline]

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

Equations

• Lake.BuildKey.customTarget package target = Lake.BuildKey.packageTarget package target

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

Equations

• (Lake.BuildKey.module a).toString = toString "+" ++ toString a ++ toString ""
• (Lake.BuildKey.package a).toString = toString "@" ++ toString a ++ toString ""
• (Lake.BuildKey.packageTarget a a_1).toString = toString "" ++ toString a ++ toString "/" ++ toString a_1 ++ toString ""
• (a.facet a_1).toString = toString "" ++ toString a.toString ++ toString ":" ++ toString (Lake.Name.eraseHead a_1) ++ toString ""

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

Like the default toString, but without disambiguation markers.

Equations

• (Lake.BuildKey.module a).toSimpleString = toString "" ++ toString a ++ toString ""
• (Lake.BuildKey.package a).toSimpleString = toString "" ++ toString a ++ toString ""
• (Lake.BuildKey.packageTarget a a_1).toSimpleString = toString "" ++ toString a ++ toString "/" ++ toString a_1 ++ toString ""
• (a.facet a_1).toSimpleString = toString "" ++ toString a.toSimpleString ++ toString ":" ++ toString (Lake.Name.eraseHead a_1) ++ toString ""

instance Lake.BuildKey.instToString : ToString BuildKey

Equations

• Lake.BuildKey.instToString = { toString := fun (x : Lake.BuildKey) => x.toString }

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

Equations

• (Lake.BuildKey.module a).quickCmp (Lake.BuildKey.module m') = a.quickCmp m'
• (Lake.BuildKey.module a).quickCmp k' = Ordering.lt
• (Lake.BuildKey.package a).quickCmp (Lake.BuildKey.module module) = Ordering.gt
• (Lake.BuildKey.package a).quickCmp (Lake.BuildKey.package p') = a.quickCmp p'
• (Lake.BuildKey.package a).quickCmp k' = Ordering.lt
• (Lake.BuildKey.packageTarget a a_1).quickCmp (target.facet facet) = Ordering.lt
• (Lake.BuildKey.packageTarget a a_1).quickCmp (Lake.BuildKey.packageTarget p' t') = match a.quickCmp p' with | Ordering.eq => a_1.quickCmp t' | ord => ord
• (Lake.BuildKey.packageTarget a a_1).quickCmp k' = Ordering.gt
• (a.facet a_1).quickCmp (t'.facet f') = match a.quickCmp t' with | Ordering.eq => a_1.quickCmp f' | ord => ord
• (a.facet a_1).quickCmp k' = Ordering.gt

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

instance Lake.BuildKey.instLawfulCmpEqQuickCmp : LawfulCmpEq BuildKey quickCmp