Version

This module contains useful definitions for manipulating versions.

Parser Utils

SemVerCore

structure Lake.SemVerCore : Type

The major-minor-patch triple of a SemVer.

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

@[implicit_reducible]

instance Lake.instInhabitedSemVerCore : Inhabited SemVerCore

Equations

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

@[implicit_reducible]

instance Lake.instReprSemVerCore : Repr SemVerCore

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lake.instDecidableEqSemVerCore : DecidableEq SemVerCore

Equations

• Lake.instDecidableEqSemVerCore = Lake.instDecidableEqSemVerCore.decEq

@[implicit_reducible]

instance Lake.instOrdSemVerCore : Ord SemVerCore

Equations

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

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

@[implicit_reducible]

instance Lake.SemVerCore.instLT : LT SemVerCore

Equations

• Lake.SemVerCore.instLT = ltOfOrd

@[implicit_reducible]

instance Lake.SemVerCore.instLE : LE SemVerCore

Equations

• Lake.SemVerCore.instLE = leOfOrd

@[implicit_reducible]

instance Lake.SemVerCore.instMin : Min SemVerCore

Equations

• Lake.SemVerCore.instMin = minOfLe

@[implicit_reducible]

instance Lake.SemVerCore.instMax : Max SemVerCore

Equations

• Lake.SemVerCore.instMax = maxOfLe

@[inline]

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

Equations

• Lake.SemVerCore.parse s = Lake.runVerParse✝ s Lake.SemVerCore.parseM✝

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

Equations

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

@[implicit_reducible]

instance Lake.SemVerCore.instToString : ToString SemVerCore

Equations

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

@[implicit_reducible]

instance Lake.SemVerCore.instToJson : Lean.ToJson SemVerCore

Equations

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

@[implicit_reducible]

instance Lake.SemVerCore.instFromJson : Lean.FromJson SemVerCore

Equations

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

StdVer

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

@[implicit_reducible]

instance Lake.instInhabitedStdVer : Inhabited StdVer

Equations

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

@[implicit_reducible]

instance Lake.instReprStdVer : Repr StdVer

Equations

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

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

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lake.StdVer.instCoeSemVerCore : Coe StdVer SemVerCore

Equations

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

@[inline]

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

Equations

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

@[implicit_reducible]

instance Lake.StdVer.instCoeSemVerCore_1 : Coe SemVerCore StdVer

Equations

• Lake.StdVer.instCoeSemVerCore_1 = { 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.

@[implicit_reducible]

instance Lake.StdVer.instOrd : Ord StdVer

Equations

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

@[implicit_reducible]

instance Lake.StdVer.instLT : LT StdVer

Equations

• Lake.StdVer.instLT = ltOfOrd

@[implicit_reducible]

instance Lake.StdVer.instLE : LE StdVer

Equations

• Lake.StdVer.instLE = leOfOrd

@[implicit_reducible]

instance Lake.StdVer.instMin : Min StdVer

Equations

• Lake.StdVer.instMin = minOfLe

@[implicit_reducible]

instance Lake.StdVer.instMax : Max StdVer

Equations

• Lake.StdVer.instMax = maxOfLe

def Lake.StdVer.parseM (s : String) : EStateM String s.Pos StdVer

Equations

• Lake.StdVer.parseM s = do let core ← Lake.SemVerCore.parseM✝ s let specialDescr ← Lake.parseSpecialDescr✝ s pure { toSemVerCore := core, specialDescr := specialDescr }

@[inline]

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

Equations

• Lake.StdVer.parse s = Lake.runVerParse✝ s Lake.StdVer.parseM

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

@[implicit_reducible]

instance Lake.StdVer.instToString : ToString StdVer

Equations

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

@[implicit_reducible]

instance Lake.StdVer.instToJson : Lean.ToJson StdVer

Equations

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

@[implicit_reducible]

instance Lake.StdVer.instFromJson : Lean.FromJson StdVer

Equations

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

ToolchainVer

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"

@[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.nightly date (some r)).toString = toString Lake.ToolchainVer.defaultOrigin ++ toString ":nightly-" ++ toString date ++ (toString "-rev" ++ toString r)
• (Lake.ToolchainVer.pr n).toString = toString Lake.ToolchainVer.prOrigin ++ toString ":pr-release-" ++ toString n
• (Lake.ToolchainVer.other v).toString = v

inductive Lake.ToolchainVer : Type

A Lean toolchain version.

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

@[implicit_reducible]

instance Lake.instReprToolchainVer : Repr ToolchainVer

Equations

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

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

Equations

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

@[implicit_reducible]

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 rev) = 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 rev) (Lake.ToolchainVer.release ver) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.nightly a a_1) (Lake.ToolchainVer.nightly b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.nightly date rev) (Lake.ToolchainVer.pr n) = isFalse ⋯
• Lake.instDecidableEqToolchainVer.decEq (Lake.ToolchainVer.nightly date rev) (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 rev) = 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 rev) = 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 ⋯

@[implicit_reducible]

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)

@[implicit_reducible]

instance Lake.ToolchainVer.instToString : ToString ToolchainVer

Equations

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

@[implicit_reducible]

instance Lake.ToolchainVer.instToJson : Lean.ToJson ToolchainVer

Equations

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

@[implicit_reducible]

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 r1).blt (Lake.ToolchainVer.nightly d2 r2) = (decide (d1 < d2) || d1 == d2 && decide (r1.getD 0 < r2.getD 0))
• a.blt b = false

@[implicit_reducible]

instance Lake.ToolchainVer.instLT : LT ToolchainVer

Equations

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

@[implicit_reducible]

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 r1).ble (Lake.ToolchainVer.nightly d2 r2) = (decide (d1 < d2) || d1 == d2 && decide (r1.getD 0 ≤ r2.getD 0))
• (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

@[implicit_reducible]

instance Lake.ToolchainVer.instLE : LE ToolchainVer

Equations

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

@[implicit_reducible]

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

DecodeVersion

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

Parses a version from a string.

• decodeVersion : String → Except String α

@[implicit_reducible]

instance Lake.instDecodeVersionSemVerCore : DecodeVersion SemVerCore

Equations

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

@[implicit_reducible, defaultInstance 1000]

instance Lake.instDecodeVersionStdVer : DecodeVersion StdVer

Equations

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

@[implicit_reducible]

instance Lake.instDecodeVersionToolchainVer : DecodeVersion ToolchainVer

Equations

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

VerRange

inductive Lake.ComparatorOp : Type

• lt : ComparatorOp
• le : ComparatorOp
• gt : ComparatorOp
• ge : ComparatorOp
• eq : ComparatorOp
• ne : ComparatorOp

def Lake.instReprComparatorOp.repr : ComparatorOp → Nat → Std.Format

Equations

• Lake.instReprComparatorOp.repr Lake.ComparatorOp.lt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.ComparatorOp.lt")).group prec✝
• Lake.instReprComparatorOp.repr Lake.ComparatorOp.le prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.ComparatorOp.le")).group prec✝
• Lake.instReprComparatorOp.repr Lake.ComparatorOp.gt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.ComparatorOp.gt")).group prec✝
• Lake.instReprComparatorOp.repr Lake.ComparatorOp.ge prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.ComparatorOp.ge")).group prec✝
• Lake.instReprComparatorOp.repr Lake.ComparatorOp.eq prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.ComparatorOp.eq")).group prec✝
• Lake.instReprComparatorOp.repr Lake.ComparatorOp.ne prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.ComparatorOp.ne")).group prec✝

@[implicit_reducible]

instance Lake.instReprComparatorOp : Repr ComparatorOp

Equations

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

@[implicit_reducible]

instance Lake.instInhabitedComparatorOp : Inhabited ComparatorOp

Equations

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

def Lake.ComparatorOp.ofString? (s : String) : Option ComparatorOp

Equations

• Lake.ComparatorOp.ofString? s = match Lake.ComparatorOp.parseM✝ s s.startPos with | EStateM.Result.ok op p => if p = s.endPos then some op else none | EStateM.Result.error a a_1 => none

def Lake.ComparatorOp.toString (self : ComparatorOp) : String

Equations

• Lake.ComparatorOp.lt.toString = "<"
• Lake.ComparatorOp.le.toString = "≤"
• Lake.ComparatorOp.gt.toString = ">"
• Lake.ComparatorOp.ge.toString = "≥"
• Lake.ComparatorOp.eq.toString = "="
• Lake.ComparatorOp.ne.toString = "≠"

@[implicit_reducible]

instance Lake.ComparatorOp.instToString : ToString ComparatorOp

Equations

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

structure Lake.VerComparator : Type

• innerMk :: (
• ver : Lake.StdVer
• op : Lake.ComparatorOp
• includeSuffixes : Bool
• )

def Lake.instReprVerComparator.repr : VerComparator → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Lake.instReprVerComparator : Repr VerComparator

Equations

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

def Lake.VerComparator.wild : VerComparator

A version comparator that matches any non-suffixed version (i.e., *, ≥0.0.0).

Equations

• Lake.VerComparator.wild = { ver := Lake.StdVer.ofSemVerCore { }, op := Lake.ComparatorOp.ge }

@[implicit_reducible]

instance Lake.VerComparator.instInhabited : Inhabited VerComparator

Equations

• Lake.VerComparator.instInhabited = { default := Lake.VerComparator.wild }

@[inline]

def Lake.VerComparator.parse (s : String) : Except String VerComparator

Equations

• Lake.VerComparator.parse s = Lake.runVerParse✝ s Lake.VerComparator.parseM✝

def Lake.VerComparator.test (self : VerComparator) (ver : StdVer) : Bool

Equations

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

def Lake.VerComparator.toString (self : VerComparator) : String

Equations

• self.toString = toString (Lake.VerComparator.op✝ self) ++ toString (Lake.VerComparator.ver✝ self) ++ toString (if Lake.VerComparator.includeSuffixes✝ self = true then "-" else "")

@[implicit_reducible]

instance Lake.VerComparator.instToString : ToString VerComparator

Equations

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

structure Lake.VerRange : Type

• innerMk :: (
• toString : String
• clauses : Array (Array VerComparator)
• )

@[implicit_reducible]

instance Lake.instReprVerRange : Repr VerRange

Equations

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

def Lake.instReprVerRange.repr : VerRange → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Lake.instInhabitedVerRange : Inhabited VerRange

Equations

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

@[implicit_reducible]

instance Lake.VerRange.instToString : ToString VerRange

Equations

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

def Lake.VerRange.ofClauses (clauses : Array (Array VerComparator)) : VerRange

Equations

• Lake.VerRange.ofClauses clauses = { toString := Lake.VerRange.ofClauses.fmtOrs✝ clauses, clauses := clauses }

@[inline]

def Lake.VerRange.parse (s : String) : Except String VerRange

Equations

• Lake.VerRange.parse s = Lake.runVerParse✝ s Lake.VerRange.parseM✝

def Lake.VerRange.test (self : VerRange) (ver : StdVer) : Bool

Equations

• self.test ver = self.clauses.any fun (x : Array Lake.VerComparator) => x.all fun (x : Lake.VerComparator) => x.test ver