max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: lake: use --service w/ cache get <mappings> (#12640)

Browse source 
This PR fixes an oversight in #12490 where `--service` was not used for
`cache get` with a mappings file.
This commit is contained in:
Mac Malone 2026-02-22 23:45:08 -05:00 • committed by GitHub
parent aab4d64f25
commit e7e3588c97
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/lake/Lake/CLI/Main.lean
View file

@ -411,11 +411,16 @@ protected def get : CliM PUnit := do
failure
let some remoteScope := opts.scope?
| error "to use `cache get` with a mappings file, `--scope` or `--repo` must be set"
let service : CacheService :=
if let some artifactEndpoint := ws.lakeEnv.cacheArtifactEndpoint? then
.downloadArtsService artifactEndpoint ws.lakeEnv.cacheService?
let service : CacheService ← id do
if let some service := opts.service? then
let some service := ws.findCacheService? service
| error (serviceNotFound service ws.lakeConfig.config.cache.services)
return service
else if let some artifactEndpoint := ws.lakeEnv.cacheArtifactEndpoint? then
logWarning endpointDeprecation
return .downloadArtsService artifactEndpoint ws.lakeEnv.cacheService?
else
.reservoirService ws.lakeEnv.reservoirApiUrl
return ws.defaultCacheService
let map ← CacheMap.load file
service.downloadOutputArtifacts map cache ws.root.cacheScope remoteScope opts.forceDownload
else