Package Registries

This module contains definitions for fetching Lake package information from a online registry (e.g., Reservoir).

inductive Lake.RegistrySrc : Type

Package source information from a Lake registry (e.g., Reservoir). Only contains the subset of fields useful to Lake.

• git (data : JsonObject) (url : String) (githubUrl? defaultBranch? : Option String) (subDir? : Option System.FilePath) : RegistrySrc
• other (data : JsonObject) : RegistrySrc

def Lake.instInhabitedRegistrySrc.default : RegistrySrc

Equations

• Lake.instInhabitedRegistrySrc.default = Lake.RegistrySrc.git default default default default default

instance Lake.instInhabitedRegistrySrc : Inhabited RegistrySrc

Equations

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

def Lake.RegistrySrc.isGit (src : RegistrySrc) : Bool

Equations

• (Lake.RegistrySrc.git data url githubUrl? defaultBranch? subDir?).isGit = true
• (Lake.RegistrySrc.other data).isGit = false

def Lake.RegistrySrc.data (src : RegistrySrc) : JsonObject

Equations

• (Lake.RegistrySrc.git data url githubUrl? defaultBranch? subDir?).data = data
• (Lake.RegistrySrc.other data).data = data

def Lake.RegistrySrc.toJson (src : RegistrySrc) : Lean.Json

Equations

• src.toJson = Lean.Json.obj src.data

instance Lake.RegistrySrc.instToJson : Lean.ToJson RegistrySrc

Equations

• Lake.RegistrySrc.instToJson = { toJson := Lake.RegistrySrc.toJson }

def Lake.RegistrySrc.fromJson? (val : Lean.Json) : Except String RegistrySrc

Equations

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

instance Lake.RegistrySrc.instFromJson : Lean.FromJson RegistrySrc

Equations

• Lake.RegistrySrc.instFromJson = { fromJson? := Lake.RegistrySrc.fromJson? }

structure Lake.RegistryPkg : Type

Package metadata from a Lake registry (e.g., Reservoir). Only contains the subset of fields useful to Lake.

• name : String
• fullName : String
• sources : Array RegistrySrc
• data : Lean.Json

def Lake.instInhabitedRegistryPkg.default : RegistryPkg

Equations

• Lake.instInhabitedRegistryPkg.default = { name := default, fullName := default, sources := default, data := default }

instance Lake.instInhabitedRegistryPkg : Inhabited RegistryPkg

Equations

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

def Lake.RegistryPkg.gitSrc? (pkg : RegistryPkg) : Option RegistrySrc

Equations

• pkg.gitSrc? = Array.find? (fun (x : Lake.RegistrySrc) => x.isGit) pkg.sources

def Lake.RegistryPkg.toJson (src : RegistryPkg) : Lean.Json

Equations

• src.toJson = src.data

def Lake.RegistryPkg.fromJson? (val : Lean.Json) : Except String RegistryPkg

Equations

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

instance Lake.RegistryPkg.instFromJson : Lean.FromJson RegistryPkg

Equations

• Lake.RegistryPkg.instFromJson = { fromJson? := Lake.RegistryPkg.fromJson? }

def Lake.hexEncodeByte (b : UInt8) : Char

Equations

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

def Lake.uriEscapeByte (b : UInt8) (s : String := "") : String

Encode a byte as a URI escape code (e.g., %20).

Equations

• Lake.uriEscapeByte b s = ((s.push '%').push (Lake.hexEncodeByte (b >>> 4))).push (Lake.hexEncodeByte (b &&& 15))

@[specialize #[]]

def Lake.foldlUtf8M {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (c : Char) (f : σ → UInt8 → m σ) (init : σ) : m σ

Folds a monadic function over the UTF-8 bytes of Char from most significant to least significant.

Equations

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

@[reducible, inline]

abbrev Lake.foldlUtf8 {σ : Type u_1} (c : Char) (f : σ → UInt8 → σ) (init : σ) : σ

Equations

• Lake.foldlUtf8 c f init = (Lake.foldlUtf8M c (fun (x1 : σ) (x2 : UInt8) => pure (f x1 x2)) init).run

def Lake.uriEscapeChar (c : Char) (s : String := "") : String

Encode a character as a sequence of URI escape codes representing its UTF8 encoding.

Equations

• Lake.uriEscapeChar c s = Lake.foldlUtf8 c (fun (s : String) (b : UInt8) => Lake.uriEscapeByte b s) s

def Lake.isUriUnreservedMark (c : Char) : Bool

A URI unreserved mark as specified in RFC2396.

Equations

• Lake.isUriUnreservedMark '-' = true
• Lake.isUriUnreservedMark '_' = true
• Lake.isUriUnreservedMark '.' = true
• Lake.isUriUnreservedMark '!' = true
• Lake.isUriUnreservedMark '~' = true
• Lake.isUriUnreservedMark '*' = true
• Lake.isUriUnreservedMark '\'' = true
• Lake.isUriUnreservedMark '(' = true
• Lake.isUriUnreservedMark ')' = true
• Lake.isUriUnreservedMark c = false

def Lake.uriEncodeChar (c : Char) (s : String := "") : String

Encodes anything but a URI unreserved character as a URI escape sequences.

Equations

• Lake.uriEncodeChar c s = if (c.isAlphanum || Lake.isUriUnreservedMark c) = true then s.push c else Lake.uriEscapeChar c s

def Lake.uriEncode (s : String) : String

Encodes a string as an ASCII URI component, escaping special characters (and unicode).

Equations

• Lake.uriEncode s = String.foldl (fun (s : String) (c : Char) => Lake.uriEncodeChar c s) "" s

def Lake.getUrl (url : String) (headers : Array String := #[]) : LogIO String

Perform a HTTP GET request of a URL (using curl) and return the body.

Equations

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

inductive Lake.ReservoirResp (α : Type u) : Type u

A Reservoir API response object.

• data {α : Type u} (a : α) : ReservoirResp α
• error {α : Type u} (status : Nat) (message : String) : ReservoirResp α

def Lake.ReservoirResp.fromJson? {α : Type} [Lean.FromJson α] (val : Lean.Json) : Except String (ReservoirResp α)

Equations

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

instance Lake.instFromJsonReservoirResp {α : Type} [Lean.FromJson α] : Lean.FromJson (ReservoirResp α)

Equations

• Lake.instFromJsonReservoirResp = { fromJson? := Lake.ReservoirResp.fromJson? }

def Lake.Reservoir.pkgApiUrl (lakeEnv : Env) (owner pkg : String) : String

Equations

• Lake.Reservoir.pkgApiUrl lakeEnv owner pkg = toString lakeEnv.reservoirApiUrl ++ toString "/packages/" ++ toString (Lake.uriEncode owner) ++ toString "/" ++ toString (Lake.uriEncode pkg)

def Lake.Reservoir.lakeHeaders : Array String

Equations

• Lake.Reservoir.lakeHeaders = #["X-Reservoir-Api-Version:1.0.0", "X-Lake-Registry-Api-Version:0.1.0"]

def Lake.Reservoir.fetchPkg? (lakeEnv : Env) (owner pkg : String) : LogIO (Option RegistryPkg)

Equations

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