From e7e3588c973226e85d79ed0f3154cfca79b61c6f Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Sun, 22 Feb 2026 23:45:08 -0500 Subject: [PATCH] fix: lake: use `--service` w/ `cache get ` (#12640) This PR fixes an oversight in #12490 where `--service` was not used for `cache get` with a mappings file. --- src/lake/Lake/CLI/Main.lean | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 43cc01f9d2..0bbf830244 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -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