Documentation

Lake.Util.Version

Version #

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

structure Lake.SemVerCore :

The major-minor-patch triple of a SemVer.

major : Nat
minor : Nat
patch : Nat

Instances For

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

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 :

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

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 :

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

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 : Lake.StdVer) (b : Lake.StdVer) :

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 :

Equations

Lake.instLTStdVer = ltOfOrd

instance Lake.instLEStdVer :

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

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.

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

Parses a version from a string.

decodeVersion : String → Except String α

Instances

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 }

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.