Lake.Config.LakeConfig

source

inductive Lake.CacheServiceKind :

Type

Instances For

source

@[implicit_reducible]

instance Lake.instInhabitedCacheServiceKind :

Inhabited CacheServiceKind

source

def Lake.instInhabitedCacheServiceKind.default :

CacheServiceKind

Instances For

source

@[inline]

def Lake.CacheServiceKind.ofString? (s : String) :

Option CacheServiceKind

Instances For

source

structure Lake.CacheServiceConfig :

Type

name : String
kind : CacheServiceKind
apiEndpoint : String
artifactEndpoint : String
revisionEndpoint : String

Instances For

source

@[implicit_reducible]

instance Lake.CacheServiceConfig.instConfigInfo :

ConfigInfo `Lake.CacheServiceConfig

source

@[implicit_reducible]

instance Lake.CacheServiceConfig.artifactEndpoint.instConfigField :

ConfigField CacheServiceConfig `artifactEndpoint String

source

@[implicit_reducible]

instance Lake.CacheServiceConfig.instEmptyCollection :

EmptyCollection CacheServiceConfig

source

@[implicit_reducible]

instance Lake.CacheServiceConfig.type.instConfigField :

ConfigField CacheServiceConfig `type CacheServiceKind

source

@[implicit_reducible]

instance Lake.CacheServiceConfig.revisionEndpoint.instConfigField :

ConfigField CacheServiceConfig `revisionEndpoint String

source

@[implicit_reducible]

instance Lake.CacheServiceConfig.name.instConfigField :

ConfigField CacheServiceConfig `name String

source

@[implicit_reducible]

instance Lake.CacheServiceConfig.kind.instConfigField :

ConfigField CacheServiceConfig `kind CacheServiceKind

source

@[implicit_reducible]

instance Lake.CacheServiceConfig.apiEndpoint.instConfigField :

ConfigField CacheServiceConfig `apiEndpoint String

source

@[implicit_reducible]

instance Lake.CacheServiceConfig.instConfigFields :

ConfigFields CacheServiceConfig

source

def Lake.instInhabitedCacheServiceConfig.default :

CacheServiceConfig

Instances For

source

@[implicit_reducible]

instance Lake.instInhabitedCacheServiceConfig :

Inhabited CacheServiceConfig

source

structure Lake.CacheConfig :

Type

defaultService : String
defaultUploadService : String
services : Array CacheServiceConfig

Instances For

source

@[implicit_reducible]

instance Lake.CacheConfig.instEmptyCollection :

EmptyCollection CacheConfig

source

@[implicit_reducible]

instance Lake.CacheConfig.defaultUploadService.instConfigField :

ConfigField CacheConfig `defaultUploadService String

source

@[implicit_reducible]

instance Lake.CacheConfig.service.instConfigField :

ConfigField CacheConfig `service (Array CacheServiceConfig)

source

@[implicit_reducible]

instance Lake.CacheConfig.defaultService.instConfigField :

ConfigField CacheConfig `defaultService String

source

@[implicit_reducible]

instance Lake.CacheConfig.instConfigFields :

ConfigFields CacheConfig

source

@[implicit_reducible]

instance Lake.CacheConfig.instConfigInfo :

ConfigInfo `Lake.CacheConfig

source

def Lake.instInhabitedCacheConfig.default :

CacheConfig

Instances For

source

@[implicit_reducible]

instance Lake.instInhabitedCacheConfig :

Inhabited CacheConfig

source

structure Lake.LakeConfig :

Type

cache : CacheConfig

Instances For

source

@[implicit_reducible]

instance Lake.LakeConfig.instConfigFields :

ConfigFields LakeConfig

source

@[implicit_reducible]

instance Lake.LakeConfig.instEmptyCollection :

EmptyCollection LakeConfig

source

@[implicit_reducible]

instance Lake.LakeConfig.instConfigInfo :

ConfigInfo `Lake.LakeConfig

source

@[implicit_reducible]

instance Lake.LakeConfig.cache.instConfigField :

ConfigField LakeConfig `cache CacheConfig

source

@[implicit_reducible]

instance Lake.instInhabitedLakeConfig :

Inhabited LakeConfig

source

def Lake.instInhabitedLakeConfig.default :

LakeConfig

Instances For

source

structure Lake.LoadedLakeConfig :

Type

config : LakeConfig
defaultCacheService : CacheService
defaultUploadCacheService? : Option CacheService
cacheServices : Lean.NameMap CacheService

Instances For

source

instance Lake.instNonemptyLoadedLakeConfig :

Nonempty LoadedLakeConfig