source
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

Instances For

source
instance Lake.instInhabitedBuildKey :
Inhabited BuildKey
Equations

- Lake.instInhabitedBuildKey = { default := Lake.instInhabitedBuildKey.default }

source
def Lake.instInhabitedBuildKey.default :
BuildKey
Equations

- Lake.instInhabitedBuildKey.default = Lake.BuildKey.module default

Instances For

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

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

Instances For

source
instance Lake.instReprBuildKey :
Repr BuildKey
Equations

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

source
instance Lake.instDecidableEqBuildKey :
DecidableEq BuildKey
Equations

- Lake.instDecidableEqBuildKey = Lake.instDecidableEqBuildKey.decEq

source
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 ⋯

Instances For

source
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)

Instances For

source
instance Lake.instHashableBuildKey :
Hashable BuildKey
Equations

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

source
def Lake.PartialBuildKey.moduleTargetIndicator :
Lean.Name
Equations

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

Instances For

source
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

Instances For

source
@[inline]
def Lake.PartialBuildKey.mk (key : BuildKey) :
PartialBuildKey

Cast a `BuildKey` to a `PartialBuildKey`.

Equations

- Lake.PartialBuildKey.mk key = key

Instances For

source
instance Lake.PartialBuildKey.instCoeBuildKey :
Coe BuildKey PartialBuildKey
Equations

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

source
instance Lake.PartialBuildKey.instRepr :
Repr PartialBuildKey
Equations

- Lake.PartialBuildKey.instRepr = Lake.PartialBuildKey.instRepr._private_1

source
instance Lake.PartialBuildKey.instInhabited :
Inhabited PartialBuildKey
Equations

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

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

Instances For

source
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

Instances For

source
instance Lake.PartialBuildKey.instToString :
ToString PartialBuildKey
Equations

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

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[reducible, match_pattern, inline]
abbrev Lake.BuildKey.customTarget (package target : Lean.Name) :
BuildKey
Equations

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

Instances For

source
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)

Instances For

source
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)

Instances For

source
instance Lake.BuildKey.instToString :
ToString BuildKey
Equations

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

source
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

Instances For

source
theorem Lake.BuildKey.eq_of_quickCmp {k k' : BuildKey} :
k.quickCmp k' = Ordering.eq → k = k'
source
instance Lake.BuildKey.instLawfulEqCmpQuickCmp :
Std.LawfulEqCmp quickCmp