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

@[implicit_reducible]

instance Lake.instInhabitedRegistrySrc : Inhabited RegistrySrc

def Lake.instInhabitedRegistrySrc.default : RegistrySrc

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

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

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

@[implicit_reducible]

instance Lake.RegistrySrc.instToJson : Lean.ToJson RegistrySrc

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

@[implicit_reducible]

instance Lake.RegistrySrc.instFromJson : Lean.FromJson RegistrySrc

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

@[implicit_reducible]

instance Lake.instInhabitedRegistryPkg : Inhabited RegistryPkg

def Lake.instInhabitedRegistryPkg.default : RegistryPkg

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

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

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

@[implicit_reducible]

instance Lake.RegistryPkg.instFromJson : Lean.FromJson RegistryPkg

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

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

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

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

@[implicit_reducible]

instance Lake.instFromJsonRegistryVer : Lean.FromJson RegistryVer

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

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