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.instInhabitedBuildKey.default }

def Lake.instInhabitedBuildKey.default : BuildKey

Equations

• Lake.instInhabitedBuildKey.default = Lake.BuildKey.module default

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

Equations

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

instance Lake.instReprBuildKey : Repr BuildKey

Equations

• Lake.instReprBuildKey = { reprPrec := Lake.instReprBuildKey.repr }

instance Lake.instDecidableEqBuildKey : DecidableEq BuildKey

Equations

• Lake.instDecidableEqBuildKey = Lake.instDecidableEqBuildKey.decEq

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

Equations

• One or more equations did not get rendered due to their size.
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.module a) (Lake.BuildKey.module b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.module module) (Lake.BuildKey.package package) = isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.module module) (Lake.BuildKey.packageTarget package target) = isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.module module) (target.facet facet) = isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.package package) (Lake.BuildKey.module module) = isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.package a) (Lake.BuildKey.package b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.package package) (Lake.BuildKey.packageTarget package_1 target) = isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.package package) (target.facet facet) = isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.packageTarget package target) (Lake.BuildKey.module module) = isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.packageTarget package target) (Lake.BuildKey.package package_1) = isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.packageTarget a a_1) (Lake.BuildKey.packageTarget b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (Lake.BuildKey.packageTarget package target) (target_1.facet facet) = isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (target.facet facet) (Lake.BuildKey.module module) = isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (target.facet facet) (Lake.BuildKey.package package) = isFalse ⋯
• Lake.instDecidableEqBuildKey.decEq (target.facet facet) (Lake.BuildKey.packageTarget package target_1) = isFalse ⋯

def Lake.instHashableBuildKey.hash : BuildKey → UInt64

Equations

• Lake.instHashableBuildKey.hash (Lake.BuildKey.module a) = mixHash 0 (hash a)
• Lake.instHashableBuildKey.hash (Lake.BuildKey.package a) = mixHash 1 (hash a)
• Lake.instHashableBuildKey.hash (Lake.BuildKey.packageTarget a a_1) = mixHash (mixHash 2 (hash a)) (hash a_1)
• Lake.instHashableBuildKey.hash (a.facet a_1) = mixHash (mixHash 3 (Lake.instHashableBuildKey.hash a)) (hash a_1)

instance Lake.instHashableBuildKey : Hashable BuildKey

Equations

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

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

instance Lake.PartialBuildKey.instCoeBuildKey : Coe BuildKey PartialBuildKey

Equations

• Lake.PartialBuildKey.instCoeBuildKey = { coe := Lake.PartialBuildKey.mk }

instance Lake.PartialBuildKey.instRepr : Repr PartialBuildKey

Equations

• Lake.PartialBuildKey.instRepr = Lake.PartialBuildKey.instRepr._private_1

instance Lake.PartialBuildKey.instInhabited : Inhabited PartialBuildKey

Equations

• Lake.PartialBuildKey.instInhabited = { default := Lake.PartialBuildKey.mk (Lake.BuildKey.package Lean.Name.anonymous) }

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.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
• Lake.PartialBuildKey.toString (Lake.BuildKey.package p) = if p.isAnonymous = true then "" else toString "@" ++ toString p
• Lake.PartialBuildKey.toString (t.facet f) = if f.isAnonymous = true then Lake.PartialBuildKey.toString t else toString (Lake.PartialBuildKey.toString t) ++ toString ":" ++ toString f

instance Lake.PartialBuildKey.instToString : ToString PartialBuildKey

Equations

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

@[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
• (Lake.BuildKey.package a).toString = toString "@" ++ toString a
• (Lake.BuildKey.packageTarget a a_1).toString = toString a ++ toString "/" ++ toString a_1
• (a.facet a_1).toString = toString a.toString ++ toString ":" ++ toString (Lake.Name.eraseHead a_1)

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

Like the default toString, but without disambiguation markers.

Equations

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

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.instLawfulEqCmpQuickCmp : Std.LawfulEqCmp quickCmp