# Package Registries #

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

source
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

Instances For

source
instance Lake.instInhabitedRegistrySrc :
Inhabited RegistrySrc
Equations

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

source
def Lake.instInhabitedRegistrySrc.default :
RegistrySrc
Equations

- Lake.instInhabitedRegistrySrc.default = Lake.RegistrySrc.git default default default default default

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
instance Lake.RegistrySrc.instToJson :
Lean.ToJson RegistrySrc
Equations

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

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

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

Instances For

source
instance Lake.RegistrySrc.instFromJson :
Lean.FromJson RegistrySrc
Equations

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

source
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

Instances For

source
def Lake.instInhabitedRegistryPkg.default :
RegistryPkg
Equations

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

Instances For

source
instance Lake.instInhabitedRegistryPkg :
Inhabited RegistryPkg
Equations

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

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

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

Instances For

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

- src.toJson = src.data

Instances For

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

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

Instances For

source
instance Lake.RegistryPkg.instFromJson :
Lean.FromJson RegistryPkg
Equations

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

source
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 α

Instances For

source
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.

Instances For

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

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

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

Instances For

source
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.

Instances For

source
structure Lake.RegistryVer :
Type

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

- version : StdVer
- revision : String

Instances For

source
def Lake.RegistryVer.fromJson? (val : Lean.Json) :
Except String RegistryVer
Equations

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

Instances For

source
instance Lake.instFromJsonRegistryVer :
Lean.FromJson RegistryVer
Equations

- Lake.instFromJsonRegistryVer = { fromJson? := Lake.RegistryVer.fromJson? }

source
def Lake.Reservoir.pkgVersionsApiUrl (lakeEnv : Env) (owner pkg : String) :
String
Equations

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

Instances For

source
def Lake.Reservoir.fetchPkgVersions (lakeEnv : Env) (owner pkg : String) :
LogIO (Array RegistryVer)
Equations

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

Instances For