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

def Lake.instInhabitedSemVerCore.default : SemVerCore

@[implicit_reducible]

instance Lake.instInhabitedSemVerCore : Inhabited SemVerCore

@[implicit_reducible]

instance Lake.instReprSemVerCore : Repr SemVerCore

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

@[implicit_reducible]

instance Lake.instDecidableEqSemVerCore : DecidableEq SemVerCore

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

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

@[implicit_reducible]

instance Lake.instOrdSemVerCore : Ord SemVerCore

@[implicit_reducible]

instance Lake.SemVerCore.instLT : LT SemVerCore

@[implicit_reducible]

instance Lake.SemVerCore.instLE : LE SemVerCore

@[implicit_reducible]

instance Lake.SemVerCore.instMin : Min SemVerCore

@[implicit_reducible]

instance Lake.SemVerCore.instMax : Max SemVerCore

@[inline]

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

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

@[implicit_reducible]

instance Lake.SemVerCore.instToString : ToString SemVerCore

@[implicit_reducible]

instance Lake.SemVerCore.instToJson : Lean.ToJson SemVerCore

@[implicit_reducible]

instance Lake.SemVerCore.instFromJson : Lean.FromJson SemVerCore

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

def Lake.instInhabitedStdVer.default : StdVer

@[implicit_reducible]

instance Lake.instInhabitedStdVer : Inhabited StdVer

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

@[implicit_reducible]

instance Lake.instReprStdVer : Repr StdVer

@[implicit_reducible]

instance Lake.instDecidableEqStdVer : DecidableEq StdVer

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

@[reducible, inline]

abbrev Lake.LeanVer : Type

A Lean version.

@[implicit_reducible]

instance Lake.StdVer.instCoeSemVerCore : Coe StdVer SemVerCore

@[inline]

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

@[implicit_reducible]

instance Lake.StdVer.instCoeSemVerCore_1 : Coe SemVerCore StdVer

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

@[implicit_reducible]

instance Lake.StdVer.instOrd : Ord StdVer

@[implicit_reducible]

instance Lake.StdVer.instLT : LT StdVer

@[implicit_reducible]

instance Lake.StdVer.instLE : LE StdVer

@[implicit_reducible]

instance Lake.StdVer.instMin : Min StdVer

@[implicit_reducible]

instance Lake.StdVer.instMax : Max StdVer

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

@[inline]

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

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

@[implicit_reducible]

instance Lake.StdVer.instToString : ToString StdVer

@[implicit_reducible]

instance Lake.StdVer.instToJson : Lean.ToJson StdVer

@[implicit_reducible]

instance Lake.StdVer.instFromJson : Lean.FromJson StdVer

ToolchainVer

def Lake.toolchainFileName : System.FilePath

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

def Lake.ToolchainVer.defaultOrigin : String

def Lake.ToolchainVer.prOrigin : String

@[implemented_by Lake.ToolchainVer.toString._override]

noncomputable def Lake.ToolchainVer.toString : ToolchainVer → String

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

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

@[implicit_reducible]

instance Lake.instReprToolchainVer : Repr ToolchainVer

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

@[implicit_reducible]

instance Lake.instDecidableEqToolchainVer : DecidableEq ToolchainVer

@[implicit_reducible]

instance Lake.ToolchainVer.instCoeLeanVer : Coe LeanVer ToolchainVer

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

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

Parse a toolchain from a lean-toolchain file.

@[inline]

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

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

@[implicit_reducible]

instance Lake.ToolchainVer.instToString : ToString ToolchainVer

@[implicit_reducible]

instance Lake.ToolchainVer.instToJson : Lean.ToJson ToolchainVer

@[implicit_reducible]

instance Lake.ToolchainVer.instFromJson : Lean.FromJson ToolchainVer

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

@[implicit_reducible]

instance Lake.ToolchainVer.instLT : LT ToolchainVer

@[implicit_reducible]

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

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

@[implicit_reducible]

instance Lake.ToolchainVer.instLE : LE ToolchainVer

@[implicit_reducible]

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

def Lake.normalizeToolchain (s : String) : String

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

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

@[implicit_reducible, defaultInstance 1000]

instance Lake.instDecodeVersionStdVer : DecodeVersion StdVer

@[implicit_reducible]

instance Lake.instDecodeVersionToolchainVer : DecodeVersion ToolchainVer

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

@[implicit_reducible]

instance Lake.instReprComparatorOp : Repr ComparatorOp

@[implicit_reducible]

instance Lake.instInhabitedComparatorOp : Inhabited ComparatorOp

def Lake.instInhabitedComparatorOp.default : ComparatorOp

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

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

@[implicit_reducible]

instance Lake.ComparatorOp.instToString : ToString ComparatorOp

structure Lake.VerComparator : Type

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

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

@[implicit_reducible]

instance Lake.instReprVerComparator : Repr VerComparator

def Lake.VerComparator.wild : VerComparator

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

@[implicit_reducible]

instance Lake.VerComparator.instInhabited : Inhabited VerComparator

@[inline]

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

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

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

@[implicit_reducible]

instance Lake.VerComparator.instToString : ToString VerComparator

structure Lake.VerRange : Type

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

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

@[implicit_reducible]

instance Lake.instReprVerRange : Repr VerRange

def Lake.instInhabitedVerRange.default : VerRange

@[implicit_reducible]

instance Lake.instInhabitedVerRange : Inhabited VerRange

@[implicit_reducible]

instance Lake.VerRange.instToString : ToString VerRange

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

@[inline]

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

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