Version

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

structure Lake.SemVerCore : Type

The major-minor-patch triple of a SemVer.

• major : Nat
• minor : Nat
• patch : Nat

instance Lake.instInhabitedSemVerCore : Inhabited Lake.SemVerCore

Equations

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

instance Lake.instReprSemVerCore : Repr Lake.SemVerCore

Equations

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

instance Lake.instDecidableEqSemVerCore : DecidableEq Lake.SemVerCore

Equations

• Lake.instDecidableEqSemVerCore = Lake.decEqSemVerCore✝

instance Lake.instOrdSemVerCore : Ord Lake.SemVerCore

Equations

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

instance Lake.instLTSemVerCore : LT Lake.SemVerCore

Equations

• Lake.instLTSemVerCore = ltOfOrd

instance Lake.instLESemVerCore : LE Lake.SemVerCore

Equations

• Lake.instLESemVerCore = leOfOrd

instance Lake.instMinSemVerCore : Min Lake.SemVerCore

Equations

• Lake.instMinSemVerCore = minOfLe

instance Lake.instMaxSemVerCore : Max Lake.SemVerCore

Equations

• Lake.instMaxSemVerCore = maxOfLe

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

Equations

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

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

Equations

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

instance Lake.instToStringSemVerCore : ToString Lake.SemVerCore

Equations

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

instance Lake.instToJsonSemVerCore : Lean.ToJson Lake.SemVerCore

Equations

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

instance Lake.instFromJsonSemVerCore : Lean.FromJson Lake.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 Lake.SemVerCore

Equations

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

structure Lake.StdVerextends Lake.SemVerCore : Type

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

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

instance Lake.instInhabitedStdVer : Inhabited Lake.StdVer

Equations

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

instance Lake.instReprStdVer : Repr Lake.StdVer

Equations

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

instance Lake.instDecidableEqStdVer : DecidableEq Lake.StdVer

Equations

• Lake.instDecidableEqStdVer = Lake.decEqStdVer✝

@[reducible, inline]

abbrev Lake.LeanVer : Type

A Lean version.

Equations

• Lake.LeanVer = Lake.StdVer

instance Lake.instCoeStdVerSemVerCore : Coe Lake.StdVer Lake.SemVerCore

Equations

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

@[inline]

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

Equations

• Lake.StdVer.ofSemVerCore ver = { toSemVerCore := ver, specialDescr := "" }

instance Lake.instCoeSemVerCoreStdVer : Coe Lake.SemVerCore Lake.StdVer

Equations

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

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

Equations

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

instance Lake.instOrdStdVer : Ord Lake.StdVer

Equations

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

instance Lake.instLTStdVer : LT Lake.StdVer

Equations

• Lake.instLTStdVer = ltOfOrd

instance Lake.instLEStdVer : LE Lake.StdVer

Equations

• Lake.instLEStdVer = leOfOrd

instance Lake.instMinStdVer : Min Lake.StdVer

Equations

• Lake.instMinStdVer = minOfLe

instance Lake.instMaxStdVer : Max Lake.StdVer

Equations

• Lake.instMaxStdVer = maxOfLe

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

Equations

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

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

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 Lake.StdVer

Equations

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

instance Lake.instToJsonStdVer : Lean.ToJson Lake.StdVer

Equations

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

instance Lake.instFromJsonStdVer : Lean.FromJson Lake.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 Lake.StdVer

Equations

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

inductive Lake.ToolchainVer : Type

A Lean toolchain version.

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

instance Lake.instReprToolchainVer : Repr Lake.ToolchainVer

Equations

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

instance Lake.instDecidableEqToolchainVer : DecidableEq Lake.ToolchainVer

Equations

• Lake.instDecidableEqToolchainVer = Lake.decEqToolchainVer✝

instance Lake.instCoeLeanVerToolchainVer : Coe Lake.LeanVer Lake.ToolchainVer

Equations

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

def Lake.ToolchainVer.defaultOrigin : String

Equations

• Lake.ToolchainVer.defaultOrigin = "leanprover/lean4"

def Lake.ToolchainVer.prOrigin : String

Equations

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

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

Equations

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

def Lake.ToolchainVer.ofFile? (toolchainFile : System.FilePath) : IO (Option Lake.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 Lake.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 : Lake.ToolchainVer) : String

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 Lake.ToolchainVer

Equations

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

instance Lake.instToJsonToolchainVer : Lean.ToJson Lake.ToolchainVer

Equations

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

instance Lake.instFromJsonToolchainVer : Lean.FromJson Lake.ToolchainVer

Equations

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

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

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 Lake.ToolchainVer

Equations

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

instance Lake.ToolchainVer.decLt (a b : Lake.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 : Lake.ToolchainVer) : Prop

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 Lake.ToolchainVer

Equations

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

instance Lake.ToolchainVer.decLe (a b : Lake.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) : Type u

Parses a version from a string.

• decodeVersion : String → Except String α

instance Lake.instDecodeVersionSemVerCore : Lake.DecodeVersion Lake.SemVerCore

Equations

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

@[defaultInstance 1000]

instance Lake.instDecodeVersionStdVer : Lake.DecodeVersion Lake.StdVer

Equations

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

instance Lake.instDecodeVersionToolchainVer : Lake.DecodeVersion Lake.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.