Version

This module contains useful definitions for manipulating versions.

structure Lake.SemVerCore : Type

The major-minor-patch triple of a SemVer.

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

instance Lake.instInhabitedSemVerCore : Inhabited SemVerCore

Equations

• Lake.instInhabitedSemVerCore = { default := Lake.instInhabitedSemVerCore.default }

def Lake.instInhabitedSemVerCore.default : SemVerCore

Equations

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

def Lake.instReprSemVerCore.repr : SemVerCore → Nat → Std.Format

Equations

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

instance Lake.instReprSemVerCore : Repr SemVerCore

Equations

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

instance Lake.instDecidableEqSemVerCore : DecidableEq SemVerCore

Equations

• Lake.instDecidableEqSemVerCore = Lake.instDecidableEqSemVerCore.decEq

def Lake.instDecidableEqSemVerCore.decEq (x✝ x✝¹ : SemVerCore) : Decidable (x✝ = x✝¹)

Equations

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

def Lake.instOrdSemVerCore.ord : SemVerCore → SemVerCore → Ordering

Equations

• Lake.instOrdSemVerCore.ord { major := a, minor := a_1, patch := a_2 } { major := b, minor := b_1, patch := b_2 } = (compare a b).then ((compare a_1 b_1).then ((compare a_2 b_2).then Ordering.eq))

instance Lake.instOrdSemVerCore : Ord SemVerCore

Equations

• Lake.instOrdSemVerCore = { compare := Lake.instOrdSemVerCore.ord }

instance Lake.instLTSemVerCore : LT SemVerCore

Equations

• Lake.instLTSemVerCore = ltOfOrd

instance Lake.instLESemVerCore : LE SemVerCore

Equations

• Lake.instLESemVerCore = leOfOrd

instance Lake.instMinSemVerCore : Min SemVerCore

Equations

• Lake.instMinSemVerCore = minOfLe

instance Lake.instMaxSemVerCore : Max SemVerCore

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

Equations

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

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 }

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 StdVer

Equations

• Lake.instInhabitedStdVer = { default := Lake.instInhabitedStdVer.default }

def Lake.instInhabitedStdVer.default : StdVer

Equations

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

def Lake.instReprStdVer.repr : StdVer → Nat → Std.Format

Equations

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

instance Lake.instReprStdVer : Repr StdVer

Equations

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

instance Lake.instDecidableEqStdVer : DecidableEq StdVer

Equations

• Lake.instDecidableEqStdVer = Lake.instDecidableEqStdVer.decEq

def Lake.instDecidableEqStdVer.decEq (x✝ x✝¹ : StdVer) : Decidable (x✝ = x✝¹)

Equations

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

@[reducible, inline]

abbrev Lake.LeanVer : Type

A Lean version.

Equations

• Lake.LeanVer = Lake.StdVer

instance Lake.instCoeStdVerSemVerCore : Coe StdVer SemVerCore

Equations

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

@[inline]

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

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

Equations

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

instance Lake.instOrdStdVer : Ord StdVer

Equations

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

instance Lake.instLTStdVer : LT StdVer

Equations

• Lake.instLTStdVer = ltOfOrd

instance Lake.instLEStdVer : LE StdVer

Equations

• Lake.instLEStdVer = leOfOrd

instance Lake.instMinStdVer : Min StdVer

Equations

• Lake.instMinStdVer = minOfLe

instance Lake.instMaxStdVer : Max StdVer

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

Equations

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

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 }

def Lake.toolchainFileName : System.FilePath

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

Equations

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

def Lake.ToolchainVer.defaultOrigin : String

Equations

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

def Lake.ToolchainVer.prOrigin : String

Equations

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

inductive Lake.ToolchainVer : Type

A Lean toolchain version.

• release (ver : LeanVer) : ToolchainVer
• nightly (date : Date) : ToolchainVer
• pr (n : Nat) : ToolchainVer
• other (v : String) : ToolchainVer

@[implemented_by Lake.ToolchainVer.toString._override]

noncomputable def Lake.ToolchainVer.toString : ToolchainVer → String

Equations

• (Lake.ToolchainVer.release ver).toString = toString Lake.ToolchainVer.defaultOrigin ++ toString ":v" ++ toString ver
• (Lake.ToolchainVer.nightly date).toString = toString Lake.ToolchainVer.defaultOrigin ++ toString ":nightly-" ++ toString date
• (Lake.ToolchainVer.pr n).toString = toString Lake.ToolchainVer.prOrigin ++ toString ":pr-release-" ++ toString n
• (Lake.ToolchainVer.other v).toString = v

def Lake.instReprToolchainVer.repr : ToolchainVer → Nat → Std.Format

Equations

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

instance Lake.instReprToolchainVer : Repr ToolchainVer

Equations

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

instance Lake.instDecidableEqToolchainVer : DecidableEq ToolchainVer

Equations

• Lake.instDecidableEqToolchainVer = Lake.instDecidableEqToolchainVer.decEq

def Lake.instDecidableEqToolchainVer.decEq (x✝ x✝¹ : ToolchainVer) : Decidable (x✝ = x✝¹)

Equations

• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.release a) (Lake.ToolchainVer.release b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.release ver) (Lake.ToolchainVer.nightly date) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.release ver) (Lake.ToolchainVer.pr n) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.release ver) (Lake.ToolchainVer.other v) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.nightly date) (Lake.ToolchainVer.release ver) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.nightly a) (Lake.ToolchainVer.nightly b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.nightly date) (Lake.ToolchainVer.pr n) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.nightly date) (Lake.ToolchainVer.other v) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.pr n) (Lake.ToolchainVer.release ver) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.pr n) (Lake.ToolchainVer.nightly date) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.pr a) (Lake.ToolchainVer.pr b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.pr n) (Lake.ToolchainVer.other v) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.other v) (Lake.ToolchainVer.release ver) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.other v) (Lake.ToolchainVer.nightly date) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.other v) (Lake.ToolchainVer.pr n) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.other a) (Lake.ToolchainVer.other b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Lake.ToolchainVer.instCoeLeanVer : Coe LeanVer ToolchainVer

Equations

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

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

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.

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

instance Lake.ToolchainVer.instToString : ToString ToolchainVer

Equations

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

instance Lake.ToolchainVer.instToJson : Lean.ToJson ToolchainVer

Equations

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

instance Lake.ToolchainVer.instFromJson : Lean.FromJson ToolchainVer

Equations

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

def Lake.ToolchainVer.blt (a b : ToolchainVer) : Bool

Equations

• (Lake.ToolchainVer.release v1).blt (Lake.ToolchainVer.release v2) = decide (v1 < v2)
• (Lake.ToolchainVer.nightly d1).blt (Lake.ToolchainVer.nightly d2) = decide (d1 < d2)
• a.blt b = false

instance Lake.ToolchainVer.instLT : LT ToolchainVer

Equations

• Lake.ToolchainVer.instLT = { lt := fun (x1 x2 : Lake.ToolchainVer) => x1.blt x2 = true }

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

Equations

• a.decLt b = decidable_of_bool (a.blt b) ⋯

def Lake.ToolchainVer.ble (a b : ToolchainVer) : Bool

Equations

• (Lake.ToolchainVer.release v1).ble (Lake.ToolchainVer.release v2) = decide (v1 ≤ v2)
• (Lake.ToolchainVer.nightly d1).ble (Lake.ToolchainVer.nightly d2) = decide (d1 ≤ d2)
• (Lake.ToolchainVer.pr n1).ble (Lake.ToolchainVer.pr n2) = decide (n1 = n2)
• (Lake.ToolchainVer.other v1).ble (Lake.ToolchainVer.other v2) = decide (v1 = v2)
• a.ble b = false

instance Lake.ToolchainVer.instLE : LE ToolchainVer

Equations

• Lake.ToolchainVer.instLE = { le := fun (x1 x2 : Lake.ToolchainVer) => x1.ble x2 = true }

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

Equations

• a.decLe b = decidable_of_bool (a.ble b) ⋯

def Lake.normalizeToolchain (s : String) : String

Converts a toolchain version to its normal form (e.g., with an origin).

Equations

• Lake.normalizeToolchain s = (Lake.ToolchainVer.ofString s).toString

class Lake.DecodeVersion (α : Type u) : Type u

Parses a version from a string.

• decodeVersion : String → Except String α

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