inductive Lake.CacheServiceKind : Type

• undef : CacheServiceKind
• reservoir : CacheServiceKind
• s3 : CacheServiceKind

@[implicit_reducible]

instance Lake.instInhabitedCacheServiceKind : Inhabited CacheServiceKind

Equations

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

def Lake.instInhabitedCacheServiceKind.default : CacheServiceKind

Equations

• Lake.instInhabitedCacheServiceKind.default = Lake.CacheServiceKind.undef

@[inline]

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

Equations

• Lake.CacheServiceKind.ofString? "reservoir" = some Lake.CacheServiceKind.reservoir
• Lake.CacheServiceKind.ofString? "s3" = some Lake.CacheServiceKind.s3
• Lake.CacheServiceKind.ofString? s = none

structure Lake.CacheServiceConfig : Type

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

@[implicit_reducible]

instance Lake.CacheServiceConfig.instConfigInfo : ConfigInfo `Lake.CacheServiceConfig

Equations

• Lake.CacheServiceConfig.instConfigInfo = { fields := Lake.CacheServiceConfig._fields, arity := 0 }

@[implicit_reducible]

instance Lake.CacheServiceConfig.artifactEndpoint.instConfigField : ConfigField CacheServiceConfig `artifactEndpoint String

Equations

• Lake.CacheServiceConfig.artifactEndpoint.instConfigField = { toConfigProj := Lake.CacheServiceConfig.artifactEndpoint._proj }

@[implicit_reducible]

instance Lake.CacheServiceConfig.instEmptyCollection : EmptyCollection CacheServiceConfig

Equations

• Lake.CacheServiceConfig.instEmptyCollection = { emptyCollection := { } }

@[implicit_reducible]

instance Lake.CacheServiceConfig.type.instConfigField : ConfigField CacheServiceConfig `type CacheServiceKind

Equations

• Lake.CacheServiceConfig.type.instConfigField = { toConfigProj := Lake.CacheServiceConfig.kind._proj }

@[implicit_reducible]

instance Lake.CacheServiceConfig.revisionEndpoint.instConfigField : ConfigField CacheServiceConfig `revisionEndpoint String

Equations

• Lake.CacheServiceConfig.revisionEndpoint.instConfigField = { toConfigProj := Lake.CacheServiceConfig.revisionEndpoint._proj }

@[implicit_reducible]

instance Lake.CacheServiceConfig.name.instConfigField : ConfigField CacheServiceConfig `name String

Equations

• Lake.CacheServiceConfig.name.instConfigField = { toConfigProj := Lake.CacheServiceConfig.name._proj }

@[implicit_reducible]

instance Lake.CacheServiceConfig.kind.instConfigField : ConfigField CacheServiceConfig `kind CacheServiceKind

Equations

• Lake.CacheServiceConfig.kind.instConfigField = { toConfigProj := Lake.CacheServiceConfig.kind._proj }

@[implicit_reducible]

instance Lake.CacheServiceConfig.apiEndpoint.instConfigField : ConfigField CacheServiceConfig `apiEndpoint String

Equations

• Lake.CacheServiceConfig.apiEndpoint.instConfigField = { toConfigProj := Lake.CacheServiceConfig.apiEndpoint._proj }

@[implicit_reducible]

instance Lake.CacheServiceConfig.instConfigFields : ConfigFields CacheServiceConfig

Equations

• Lake.CacheServiceConfig.instConfigFields = { fields := Lake.CacheServiceConfig._fields }

def Lake.instInhabitedCacheServiceConfig.default : CacheServiceConfig

Equations

• Lake.instInhabitedCacheServiceConfig.default = { name := default, kind := default, apiEndpoint := default, artifactEndpoint := default, revisionEndpoint := default }

@[implicit_reducible]

instance Lake.instInhabitedCacheServiceConfig : Inhabited CacheServiceConfig

Equations

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

structure Lake.CacheConfig : Type

• defaultService : String
• defaultUploadService : String
• services : Array CacheServiceConfig

@[implicit_reducible]

instance Lake.CacheConfig.instEmptyCollection : EmptyCollection CacheConfig

Equations

• Lake.CacheConfig.instEmptyCollection = { emptyCollection := { } }

@[implicit_reducible]

instance Lake.CacheConfig.defaultUploadService.instConfigField : ConfigField CacheConfig `defaultUploadService String

Equations

• Lake.CacheConfig.defaultUploadService.instConfigField = { toConfigProj := Lake.CacheConfig.defaultUploadService._proj }

@[implicit_reducible]

instance Lake.CacheConfig.service.instConfigField : ConfigField CacheConfig `service (Array CacheServiceConfig)

Equations

• Lake.CacheConfig.service.instConfigField = { toConfigProj := Lake.CacheConfig.services._proj }

@[implicit_reducible]

instance Lake.CacheConfig.defaultService.instConfigField : ConfigField CacheConfig `defaultService String

Equations

• Lake.CacheConfig.defaultService.instConfigField = { toConfigProj := Lake.CacheConfig.defaultService._proj }

@[implicit_reducible]

instance Lake.CacheConfig.instConfigFields : ConfigFields CacheConfig

Equations

• Lake.CacheConfig.instConfigFields = { fields := Lake.CacheConfig._fields }

@[implicit_reducible]

instance Lake.CacheConfig.instConfigInfo : ConfigInfo `Lake.CacheConfig

Equations

• Lake.CacheConfig.instConfigInfo = { fields := Lake.CacheConfig._fields, arity := 0 }

def Lake.instInhabitedCacheConfig.default : CacheConfig

Equations

• Lake.instInhabitedCacheConfig.default = { defaultService := default, defaultUploadService := default, services := default }

@[implicit_reducible]

instance Lake.instInhabitedCacheConfig : Inhabited CacheConfig

Equations

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

structure Lake.LakeConfig : Type

• cache : CacheConfig

@[implicit_reducible]

instance Lake.LakeConfig.instConfigFields : ConfigFields LakeConfig

Equations

• Lake.LakeConfig.instConfigFields = { fields := Lake.LakeConfig._fields }

@[implicit_reducible]

instance Lake.LakeConfig.instEmptyCollection : EmptyCollection LakeConfig

Equations

• Lake.LakeConfig.instEmptyCollection = { emptyCollection := { } }

@[implicit_reducible]

instance Lake.LakeConfig.instConfigInfo : ConfigInfo `Lake.LakeConfig

Equations

• Lake.LakeConfig.instConfigInfo = { fields := Lake.LakeConfig._fields, arity := 0 }

@[implicit_reducible]

instance Lake.LakeConfig.cache.instConfigField : ConfigField LakeConfig `cache CacheConfig

Equations

• Lake.LakeConfig.cache.instConfigField = { toConfigProj := Lake.LakeConfig.cache._proj }

@[implicit_reducible]

instance Lake.instInhabitedLakeConfig : Inhabited LakeConfig

Equations

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

def Lake.instInhabitedLakeConfig.default : LakeConfig

Equations

• Lake.instInhabitedLakeConfig.default = { cache := default }

structure Lake.LoadedLakeConfig : Type

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

instance Lake.instNonemptyLoadedLakeConfig : Nonempty LoadedLakeConfig