Documentation

Lake.Build.Key

inductive Lake.BuildKey :

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

instance Lake.instInhabitedBuildKey :

Inhabited BuildKey

Equations

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

instance Lake.instReprBuildKey :

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 :

Equations

Lake.PartialBuildKey.moduleTargetIndicator = `«_+»

def Lake.PartialBuildKey :

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

@[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) :

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

Equations

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

@[reducible, match_pattern, inline]

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

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

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

Equations

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

Instances For

Lake.instFamilyDefBuildKeyBuildDataCustomTargetNameCustomData

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

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

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

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

Lake.BuildKey.instLawfulCmpEqQuickCmp

theorem Lake.BuildKey.eq_of_quickCmp {k k' : BuildKey} :

k.quickCmp k' = Ordering.eq → k = k'

instance Lake.BuildKey.instLawfulCmpEqQuickCmp :

LawfulCmpEq BuildKey quickCmp