Version #

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

source

structure Lake.SemVerCore :

Type

The major-minor-patch triple of a SemVer.

major : Nat
minor : Nat
patch : Nat

Instances For

source

instance Lake.instInhabitedSemVerCore :

Inhabited SemVerCore

Equations

source

instance Lake.instReprSemVerCore :

Repr SemVerCore

Equations

source

instance Lake.instDecidableEqSemVerCore :

DecidableEq SemVerCore

Equations

source

instance Lake.instOrdSemVerCore :

Ord SemVerCore

Equations

source

instance Lake.instLTSemVerCore :

LT SemVerCore

Equations

source

instance Lake.instLESemVerCore :

LE SemVerCore

Equations

source

instance Lake.instMinSemVerCore :

Min SemVerCore

Equations

source

instance Lake.instMaxSemVerCore :

Max SemVerCore

Equations

source

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

Except String SemVerCore

Equations

Instances For

source

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

String

Equations

Instances For

source

instance Lake.instToStringSemVerCore :

ToString SemVerCore

Equations

source

instance Lake.instToJsonSemVerCore :

Lean.ToJson SemVerCore

Equations

source

instance Lake.instFromJsonSemVerCore :

Lean.FromJson SemVerCore

Equations

source

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

Instances For

source

instance Lake.instInhabitedStdVer :

Inhabited StdVer

Equations

source

instance Lake.instReprStdVer :

Repr StdVer

Equations

source

instance Lake.instDecidableEqStdVer :

DecidableEq StdVer

Equations

source

@[reducible, inline]

abbrev Lake.LeanVer :

Type

A Lean version.

Equations

Instances For

source

instance Lake.instCoeStdVerSemVerCore :

Coe StdVer SemVerCore

Equations

source

@[inline]

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

StdVer

Equations

Instances For

source

instance Lake.instCoeSemVerCoreStdVer :

Coe SemVerCore StdVer

Equations

source

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

Ordering

Equations

Instances For

source

instance Lake.instOrdStdVer :

Ord StdVer

Equations

source

instance Lake.instLTStdVer :

LT StdVer

Equations

source

instance Lake.instLEStdVer :

LE StdVer

Equations

source

instance Lake.instMinStdVer :

Min StdVer

Equations

source

instance Lake.instMaxStdVer :

Max StdVer

Equations

source

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

Except String StdVer

Equations

Instances For

source

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

String

Equations

Instances For

source

instance Lake.instToStringStdVer :

ToString StdVer

Equations

source

instance Lake.instToJsonStdVer :

Lean.ToJson StdVer

Equations

source

instance Lake.instFromJsonStdVer :

Lean.FromJson StdVer

Equations

source

inductive Lake.ToolchainVer :

Type

A Lean toolchain version.

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

Instances For

source

instance Lake.instReprToolchainVer :

Repr ToolchainVer

Equations

source

instance Lake.instDecidableEqToolchainVer :

DecidableEq ToolchainVer

Equations

source

instance Lake.instCoeLeanVerToolchainVer :

Coe LeanVer ToolchainVer

Equations

source

def Lake.ToolchainVer.defaultOrigin :

String

Equations

Instances For

source

def Lake.ToolchainVer.prOrigin :

String

Equations

Instances For

source

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

ToolchainVer

Equations

Instances For

source

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

IO (Option ToolchainVer)

Parse a toolchain from a lean-toolchain file.

Equations

Instances For

source

def Lake.toolchainFileName :

System.FilePath

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

Equations

Instances For

source

@[inline]

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

IO (Option ToolchainVer)

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

Equations

Instances For

source

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

String

Equations

Instances For

source

instance Lake.instToStringToolchainVer :

ToString ToolchainVer

Equations

source

instance Lake.instToJsonToolchainVer :

Lean.ToJson ToolchainVer

Equations

source

instance Lake.instFromJsonToolchainVer :

Lean.FromJson ToolchainVer

Equations

source

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

Prop

Equations

Instances For

source

instance Lake.instLTToolchainVer :

LT ToolchainVer

Equations

source

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

Decidable (a < b)

Equations

source

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

Prop

Equations

Instances For

source

instance Lake.instLEToolchainVer :

LE ToolchainVer

Equations

source

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

Decidable (a ≤ b)

Equations

source

class Lake.DecodeVersion (α : Type u) :

Type u

Parses a version from a string.

decodeVersion : String → Except String α

Instances

source

instance Lake.instDecodeVersionSemVerCore :

DecodeVersion SemVerCore

Equations

source

@[defaultInstance 1000]

instance Lake.instDecodeVersionStdVer :

DecodeVersion StdVer

Equations

source

instance Lake.instDecodeVersionToolchainVer :

DecodeVersion ToolchainVer

Equations

Documentation

Lake.Util.Version

Version #