Documentation

Lake.Util.Version

Version #

This module contains useful definitions for manipulating versions. It also defines a v!"<ver>" syntax for version literals.

structure Lake.SemVerCore :

The major-minor-patch triple of a SemVer.

major : Nat
minor : Nat
patch : Nat

Instances For

instance Lake.instInhabitedSemVerCore :

Inhabited SemVerCore

Equations

Lake.instInhabitedSemVerCore = { default := { major := default, minor := default, patch := default } }

instance Lake.instReprSemVerCore :

Repr SemVerCore

Equations

Lake.instReprSemVerCore = { reprPrec := Lake.reprSemVerCore✝ }

instance Lake.instDecidableEqSemVerCore :

DecidableEq SemVerCore

Equations

Lake.instDecidableEqSemVerCore = Lake.decEqSemVerCore✝

instance Lake.instOrdSemVerCore :

Equations

Lake.instOrdSemVerCore = { compare := Lake.ordSemVerCore✝ }

instance Lake.instLTSemVerCore :

Equations

Lake.instLTSemVerCore = ltOfOrd

instance Lake.instLESemVerCore :

Equations

Lake.instLESemVerCore = leOfOrd

instance Lake.instMinSemVerCore :

Equations

Lake.instMinSemVerCore = minOfLe

instance Lake.instMaxSemVerCore :

Equations

Lake.instMaxSemVerCore = maxOfLe

def Lake.SemVerCore.parse (ver : String) :

Except String SemVerCore

Equations

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

def Lake.SemVerCore.toString (ver : SemVerCore) :

Equations

ver.toString = toString "" ++ toString ver.major ++ toString "." ++ toString ver.minor ++ toString "." ++ toString ver.patch ++ toString ""

instance Lake.instToStringSemVerCore :

ToString SemVerCore

Equations

Lake.instToStringSemVerCore = { toString := Lake.SemVerCore.toString }

instance Lake.instToJsonSemVerCore :

Lean.ToJson SemVerCore

Equations

Lake.instToJsonSemVerCore = { toJson := fun (x : Lake.SemVerCore) => Lean.Json.str x.toString }

instance Lake.instFromJsonSemVerCore :

Lean.FromJson SemVerCore

Equations

Lake.instFromJsonSemVerCore = { fromJson? := fun (x : Lean.Json) => do let __do_lift ← Lean.fromJson? x Lake.SemVerCore.parse __do_lift }

instance Lake.instToExprSemVerCore :

Lean.ToExpr SemVerCore

Equations

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

structure Lake.StdVerextends Lake.SemVerCore :

A Lean-style semantic version. A major-minor-patch triple with an optional arbitrary - suffix.

major : Nat
minor : Nat
patch : Nat
specialDescr : String

Instances For

instance Lake.instInhabitedStdVer :

Inhabited StdVer

Equations

Lake.instInhabitedStdVer = { default := { toSemVerCore := default, specialDescr := default } }

instance Lake.instReprStdVer :

Equations

Lake.instReprStdVer = { reprPrec := Lake.reprStdVer✝ }

instance Lake.instDecidableEqStdVer :

DecidableEq StdVer

Equations

Lake.instDecidableEqStdVer = Lake.decEqStdVer✝

@[reducible, inline]

abbrev Lake.LeanVer :

A Lean version.

Equations

Lake.LeanVer = Lake.StdVer

Instances For

Lake.instCoeLeanVerToolchainVer

instance Lake.instCoeStdVerSemVerCore :

Coe StdVer SemVerCore

Equations

Lake.instCoeStdVerSemVerCore = { coe := Lake.StdVer.toSemVerCore }

@[inline]

def Lake.StdVer.ofSemVerCore (ver : SemVerCore) :

Equations

Lake.StdVer.ofSemVerCore ver = { toSemVerCore := ver }

instance Lake.instCoeSemVerCoreStdVer :

Coe SemVerCore StdVer

Equations

Lake.instCoeSemVerCoreStdVer = { coe := Lake.StdVer.ofSemVerCore }

def Lake.StdVer.compare (a b : StdVer) :

Equations

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

instance Lake.instOrdStdVer :

Equations

Lake.instOrdStdVer = { compare := Lake.StdVer.compare }

instance Lake.instLTStdVer :

Equations

Lake.instLTStdVer = ltOfOrd

instance Lake.instLEStdVer :

Equations

Lake.instLEStdVer = leOfOrd

instance Lake.instMinStdVer :

Equations

Lake.instMinStdVer = minOfLe

instance Lake.instMaxStdVer :

Equations

Lake.instMaxStdVer = maxOfLe

def Lake.StdVer.parse (ver : String) :

Except String StdVer

Equations

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

def Lake.StdVer.toString (ver : StdVer) :

Equations

ver.toString = if ver.specialDescr.isEmpty = true then ver.toString else toString "" ++ toString ver.toSemVerCore ++ toString "-" ++ toString ver.specialDescr ++ toString ""

instance Lake.instToStringStdVer :

ToString StdVer

Equations

Lake.instToStringStdVer = { toString := Lake.StdVer.toString }

instance Lake.instToJsonStdVer :

Lean.ToJson StdVer

Equations

Lake.instToJsonStdVer = { toJson := fun (x : Lake.StdVer) => Lean.Json.str x.toString }

instance Lake.instFromJsonStdVer :

Lean.FromJson StdVer

Equations

Lake.instFromJsonStdVer = { fromJson? := fun (x : Lean.Json) => do let __do_lift ← Lean.fromJson? x Lake.StdVer.parse __do_lift }

instance Lake.instToExprStdVer :

Lean.ToExpr StdVer

Equations

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

inductive Lake.ToolchainVer :

A Lean toolchain version.

release (ver : LeanVer) : ToolchainVer
nightly (date : Date) : ToolchainVer
pr (no : Nat) : ToolchainVer
other (name : String) : ToolchainVer

Instances For

instance Lake.instReprToolchainVer :

Repr ToolchainVer

Equations

Lake.instReprToolchainVer = { reprPrec := Lake.reprToolchainVer✝ }

instance Lake.instDecidableEqToolchainVer :

DecidableEq ToolchainVer

Equations

Lake.instDecidableEqToolchainVer = Lake.decEqToolchainVer✝

instance Lake.instCoeLeanVerToolchainVer :

Coe LeanVer ToolchainVer

Equations

Lake.instCoeLeanVerToolchainVer = { coe := Lake.ToolchainVer.release }

def Lake.ToolchainVer.defaultOrigin :

Equations

Lake.ToolchainVer.defaultOrigin = "leanprover/lean4"

def Lake.ToolchainVer.prOrigin :

Equations

Lake.ToolchainVer.prOrigin = "leanprover/lean4-pr-releases"

def Lake.ToolchainVer.ofString (ver : String) :

Equations

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

def Lake.ToolchainVer.ofFile? (toolchainFile : System.FilePath) :

IO (Option ToolchainVer)

Parse a toolchain from a lean-toolchain file.

Equations

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

def Lake.toolchainFileName :

System.FilePath

The elan toolchain file name (i.e., lean-toolchain).

Equations

Lake.toolchainFileName = { toString := "lean-toolchain" }

@[inline]

def Lake.ToolchainVer.ofDir? (dir : System.FilePath) :

IO (Option ToolchainVer)

Parse a toolchain from the lean-toolchain file of the directory dir.

Equations

Lake.ToolchainVer.ofDir? dir = Lake.ToolchainVer.ofFile? (dir / Lake.toolchainFileName)

def Lake.ToolchainVer.toString (ver : ToolchainVer) :

Equations

(Lake.ToolchainVer.release a).toString = toString "" ++ toString Lake.ToolchainVer.defaultOrigin ++ toString ":v" ++ toString a ++ toString ""
(Lake.ToolchainVer.nightly a).toString = toString "" ++ toString Lake.ToolchainVer.defaultOrigin ++ toString ":nightly-" ++ toString a ++ toString ""
(Lake.ToolchainVer.pr a).toString = toString "" ++ toString Lake.ToolchainVer.prOrigin ++ toString ":pr-release-" ++ toString a ++ toString ""
(Lake.ToolchainVer.other a).toString = a

instance Lake.instToStringToolchainVer :

ToString ToolchainVer

Equations

Lake.instToStringToolchainVer = { toString := Lake.ToolchainVer.toString }

instance Lake.instToJsonToolchainVer :

Lean.ToJson ToolchainVer

Equations

Lake.instToJsonToolchainVer = { toJson := fun (x : Lake.ToolchainVer) => Lean.Json.str x.toString }

instance Lake.instFromJsonToolchainVer :

Lean.FromJson ToolchainVer

Equations

Lake.instFromJsonToolchainVer = { fromJson? := fun (x : Lean.Json) => Lake.ToolchainVer.ofString <$> Lean.fromJson? x }

def Lake.ToolchainVer.lt (a b : ToolchainVer) :

Equations

(Lake.ToolchainVer.release v1).lt (Lake.ToolchainVer.release v2) = (v1 < v2)
(Lake.ToolchainVer.nightly d1).lt (Lake.ToolchainVer.nightly d2) = (d1 < d2)
a.lt b = False

instance Lake.instLTToolchainVer :

LT ToolchainVer

Equations

Lake.instLTToolchainVer = { lt := Lake.ToolchainVer.lt }

instance Lake.ToolchainVer.decLt (a b : ToolchainVer) :

Decidable (a < b)

Equations

(Lake.ToolchainVer.release v1).decLt (Lake.ToolchainVer.release v2) = inferInstanceAs (Decidable (v1 < v2))
(Lake.ToolchainVer.nightly d1).decLt (Lake.ToolchainVer.nightly d2) = inferInstanceAs (Decidable (d1 < d2))
(Lake.ToolchainVer.release ver).decLt (Lake.ToolchainVer.pr no) = isFalse Lake.ToolchainVer.decLt.proof_1
(Lake.ToolchainVer.release ver).decLt (Lake.ToolchainVer.nightly date) = isFalse Lake.ToolchainVer.decLt.proof_1
(Lake.ToolchainVer.release ver).decLt (Lake.ToolchainVer.other name) = isFalse Lake.ToolchainVer.decLt.proof_1
(Lake.ToolchainVer.nightly date).decLt (Lake.ToolchainVer.release ver) = isFalse Lake.ToolchainVer.decLt.proof_1
(Lake.ToolchainVer.nightly date).decLt (Lake.ToolchainVer.pr no) = isFalse Lake.ToolchainVer.decLt.proof_1
(Lake.ToolchainVer.nightly date).decLt (Lake.ToolchainVer.other name) = isFalse Lake.ToolchainVer.decLt.proof_1
(Lake.ToolchainVer.pr no).decLt b = isFalse Lake.ToolchainVer.decLt.proof_1
(Lake.ToolchainVer.other name).decLt b = isFalse Lake.ToolchainVer.decLt.proof_1

def Lake.ToolchainVer.le (a b : ToolchainVer) :

Equations

(Lake.ToolchainVer.release v1).le (Lake.ToolchainVer.release v2) = (v1 ≤ v2)
(Lake.ToolchainVer.nightly d1).le (Lake.ToolchainVer.nightly d2) = (d1 ≤ d2)
(Lake.ToolchainVer.pr n1).le (Lake.ToolchainVer.pr n2) = (n1 = n2)
(Lake.ToolchainVer.other v1).le (Lake.ToolchainVer.other v2) = (v1 = v2)
a.le b = False

instance Lake.instLEToolchainVer :

LE ToolchainVer

Equations

Lake.instLEToolchainVer = { le := Lake.ToolchainVer.le }

instance Lake.ToolchainVer.decLe (a b : ToolchainVer) :

Decidable (a ≤ b)

Equations

(Lake.ToolchainVer.release v1).decLe (Lake.ToolchainVer.release v2) = inferInstanceAs (Decidable (v1 ≤ v2))
(Lake.ToolchainVer.nightly d1).decLe (Lake.ToolchainVer.nightly d2) = inferInstanceAs (Decidable (d1 ≤ d2))
(Lake.ToolchainVer.pr n1).decLe (Lake.ToolchainVer.pr n2) = inferInstanceAs (Decidable (n1 = n2))
(Lake.ToolchainVer.other v1).decLe (Lake.ToolchainVer.other v2) = inferInstanceAs (Decidable (v1 = v2))
(Lake.ToolchainVer.release ver).decLe (Lake.ToolchainVer.pr no) = isFalse Lake.ToolchainVer.decLe.proof_1
(Lake.ToolchainVer.release ver).decLe (Lake.ToolchainVer.nightly date) = isFalse Lake.ToolchainVer.decLe.proof_1
(Lake.ToolchainVer.release ver).decLe (Lake.ToolchainVer.other name) = isFalse Lake.ToolchainVer.decLe.proof_1
(Lake.ToolchainVer.nightly date).decLe (Lake.ToolchainVer.release ver) = isFalse Lake.ToolchainVer.decLe.proof_1
(Lake.ToolchainVer.nightly date).decLe (Lake.ToolchainVer.pr no) = isFalse Lake.ToolchainVer.decLe.proof_1
(Lake.ToolchainVer.nightly date).decLe (Lake.ToolchainVer.other name) = isFalse Lake.ToolchainVer.decLe.proof_1
(Lake.ToolchainVer.pr no).decLe (Lake.ToolchainVer.release ver) = isFalse Lake.ToolchainVer.decLe.proof_1
(Lake.ToolchainVer.pr no).decLe (Lake.ToolchainVer.nightly date) = isFalse Lake.ToolchainVer.decLe.proof_1
(Lake.ToolchainVer.pr no).decLe (Lake.ToolchainVer.other name) = isFalse Lake.ToolchainVer.decLe.proof_1
(Lake.ToolchainVer.other name).decLe (Lake.ToolchainVer.release ver) = isFalse Lake.ToolchainVer.decLe.proof_1
(Lake.ToolchainVer.other name).decLe (Lake.ToolchainVer.nightly date) = isFalse Lake.ToolchainVer.decLe.proof_1
(Lake.ToolchainVer.other name).decLe (Lake.ToolchainVer.pr no) = isFalse Lake.ToolchainVer.decLe.proof_1

Version Literals #

Defines the v!"<ver>" syntax for version literals. The elaborator attempts to synthesize an instance of ToVersion for the expected type and then applies it to the string literal.

class Lake.DecodeVersion (α : Type u) :

Parses a version from a string.

decodeVersion : String → Except String α

Instances

instance Lake.instDecodeVersionSemVerCore :

DecodeVersion SemVerCore

Equations

Lake.instDecodeVersionSemVerCore = { decodeVersion := Lake.SemVerCore.parse }

@[defaultInstance 1000]

instance Lake.instDecodeVersionStdVer :

DecodeVersion StdVer

Equations

Lake.instDecodeVersionStdVer = { decodeVersion := Lake.StdVer.parse }

instance Lake.instDecodeVersionToolchainVer :

DecodeVersion ToolchainVer

Equations

Lake.instDecodeVersionToolchainVer = { decodeVersion := fun (x : String) => pure (Lake.ToolchainVer.ofString x) }

def Lake.verLit :

Lean.ParserDescr

A Lake version literal.

Equations

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

def Lake.elabVerLit :

Lean.Elab.Term.TermElab

Equations

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