feat: basic configured cache use & test

Author: tydeu

src/lake/Lake/CLI/Main.lean

@@ -104,7 +104,6 @@ def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
   Env.compute (← opts.getLakeInstall) (← opts.getLeanInstall) opts.elanInstall?
     opts.noCache |>.adapt fun msg => .invalidEnv msg
 
-/-- Make a `LoadConfig` from a `LakeOptions`. -/
 def LakeOptions.mkLoadConfigCore
   (opts : LakeOptions) (wsDir : FilePath) (lakeEnv : Lake.Env) (lakeConfig : LakeConfig)
 : LoadConfig where
@@ -120,7 +119,6 @@ def LakeOptions.mkLoadConfigCore
   updateDeps := opts.updateDeps
   updateToolchain := opts.updateToolchain
 
-/-- Make a `LoadConfig` from a `LakeOptions`. -/
 def LakeOptions.mkLoadConfig' (opts : LakeOptions) : LogIO LoadConfig := do
   let some wsDir ← resolvePath? opts.rootDir
     | error <| toString <| CliError.missingRootDir opts.rootDir
@@ -399,6 +397,14 @@ namespace lake
 
 namespace cache
 
+def serviceNotFound (service : String) (configuredServices : Array CacheService) : String :=
+  let msg := s!"service `{service}` not found in system configuration"
+  if configuredServices.isEmpty then
+    s!"{msg}; no services configured"
+  else
+    let msg := s!"{msg}; configured services:\n"
+    configuredServices.foldl (· ++ s!"  {·.name?}") msg
+
 @[inline] private def cacheToolchain (pkg : Package) (toolchain : String) : String :=
   if pkg.bootstrap then "" else toolchain
 
@@ -431,15 +437,20 @@ protected def get : CliM PUnit := do
     let platform := opts.platform?.getD System.Platform.target
     let toolchain := opts.toolchain?.getD ws.lakeEnv.toolchain
     let service : CacheService ← id do
-      match ws.lakeEnv.cacheArtifactEndpoint?, ws.lakeEnv.cacheRevisionEndpoint? with
-      | some artifactEndpoint, some revisionEndpoint =>
-        return .downloadService artifactEndpoint revisionEndpoint ws.lakeEnv.cacheService?
-      | none, none =>
-        return .reservoirService ws.lakeEnv.reservoirApiUrl
-      | some artifactEndpoint, none =>
-        error (invalidEndpointConfig artifactEndpoint "")
-      | none, some revisionEndpoint =>
-        error (invalidEndpointConfig "" revisionEndpoint)
+      if let some service := opts.service? then
+        let some service := ws.lakeConfig.cache.services.find? (·.name? == some service)
+          | error (serviceNotFound service ws.lakeConfig.cache.services)
+        return service
+      else
+        match ws.lakeEnv.cacheArtifactEndpoint?, ws.lakeEnv.cacheRevisionEndpoint? with
+        | some artifactEndpoint, some revisionEndpoint =>
+          return .downloadService artifactEndpoint revisionEndpoint ws.lakeEnv.cacheService?
+        | none, none =>
+          return .reservoirService ws.lakeEnv.reservoirApiUrl
+        | some artifactEndpoint, none =>
+          error (invalidEndpointConfig artifactEndpoint "")
+        | none, some revisionEndpoint =>
+          error (invalidEndpointConfig "" revisionEndpoint)
     if let some remoteScope := opts.scope? then
       if !opts.repoScope && service.isReservoir then
         -- `--scope` with Reservoir would imply downloading artifacts for a different package.
@@ -516,11 +527,18 @@ protected def put : CliM PUnit := do
   let platform := cachePlatform pkg (opts.platform?.getD System.Platform.target)
   let toolchain := cacheToolchain pkg (opts.toolchain?.getD ws.lakeEnv.toolchain)
   let service : CacheService ← id do
-    match ws.lakeEnv.cacheKey?, ws.lakeEnv.cacheArtifactEndpoint?, ws.lakeEnv.cacheRevisionEndpoint? with
-    | some key, some artifactEndpoint, some revisionEndpoint =>
-      return .uploadService key artifactEndpoint revisionEndpoint
-    | key?, artifactEndpoint?, revisionEndpoint? =>
-      error (invalidEndpointConfig key? artifactEndpoint? revisionEndpoint?)
+    if let some service := opts.service? then
+      let some service := ws.lakeConfig.cache.services.find? (·.name? == some service)
+        | error (serviceNotFound service ws.lakeConfig.cache.services)
+      let some key := ws.lakeEnv.cacheKey?
+        | error "uploads require an authentication key configured through `LAKE_CACHE_KEY`"
+      return service.withKey key
+    else
+      match ws.lakeEnv.cacheKey?, ws.lakeEnv.cacheArtifactEndpoint?, ws.lakeEnv.cacheRevisionEndpoint? with
+      | some key, some artifactEndpoint, some revisionEndpoint =>
+        return .uploadService key artifactEndpoint revisionEndpoint
+      | key?, artifactEndpoint?, revisionEndpoint? =>
+        error (invalidEndpointConfig key? artifactEndpoint? revisionEndpoint?)
   let service := service.withRepoScope opts.repoScope
   let repo := GitRepo.mk pkg.dir
   if (← repo.hasDiff) then

src/lake/Lake/Config/Cache.lean

@@ -358,12 +358,12 @@ def uploadS3
     let code ← id do
       match (data.get? "response_code" <|> data.get? "http_code") with
       | .ok (some code) => return code
-      | .ok none => error s!"curl's JSON output did not contain a response code"
-      | .error e => error s!"curl's JSON output contained an invalid JSON response code: {e}"
+      | .ok none => error s!"curl's JSON output did not contain a response code; JSON received:\n{out.stderr}"
+      | .error e => error s!"curl's JSON output contained an invalid JSON response code: {e}; JSON received:\n{out.stderr}"
     unless code == 200 do
       error s!"failed to upload artifact, error {code}; received:\n{out.stdout}"
   | .error e =>
-    error s!"curl produced invalid JSON output: {e}"
+    error s!"curl produced invalid JSON output: {e}; received:\n{out.stderr}"
 
 /--
 Configuration of a remote cache service (e.g., Reservoir or an S3 bucket).
@@ -375,7 +375,7 @@ the desired functions by using `CacheService`'s smart constructors
 -/
 public structure CacheService where
   private mk ::
-    private name? : Option String := none
+    name? : Option String := none
     /- S3 Bucket -/
     private key : String := ""
     private artifactEndpoint : String := ""
@@ -411,6 +411,10 @@ namespace CacheService
   (artifactEndpoint : String) (name? : Option String := none)
 : CacheService := {name?, artifactEndpoint}
 
+/-- Reconfigures the cache service to use the provided key (for uploads).-/
+@[inline] public def withKey (service : CacheService) (key : String) : CacheService :=
+  {service with key}
+
 /--
 Reconfigures the cache service to interpret scopes as repositories (or not if `false`).
 

src/lake/Lake/Config/LakeConfig.lean

@@ -16,7 +16,7 @@ namespace Lake
 
 public configuration CacheConfig where
   defaultService : Name := .anonymous
-  services : Array CacheService := #[]
+  services, service : Array CacheService := #[]
   deriving Inhabited
 
 public configuration LakeConfig where

src/lake/Lake/Load/Toml.lean

@@ -334,15 +334,17 @@ public protected def CacheService.decodeToml (t : Table) (ref := Syntax.missing)
   | "reservoir" => ensureDecode do
     let name ← t.tryDecode `name ref
     let repoScope ← t.tryDecode `repoScope ref
-    let apiEndpoint ← t.tryDecode `artifactEndpoint ref
+    let apiEndpoint ← normalizeUrl <$> t.tryDecode `apiEndpoint ref
     return .reservoirService apiEndpoint repoScope (some name)
   | "s3" => ensureDecode do
     let name ← t.tryDecode `name ref
-    let artifactEndpoint ← t.tryDecode `artifactEndpoint ref
-    let revisionEndpoint ← t.tryDecode `revisionEndpoint ref
+    let artifactEndpoint ← normalizeUrl <$> t.tryDecode `artifactEndpoint ref
+    let revisionEndpoint ← normalizeUrl <$> t.tryDecode `revisionEndpoint ref
     return .downloadService artifactEndpoint revisionEndpoint (some name)
   | _ =>
     throwDecodeErrorAt typeVal.ref "expected one of 'reservoir' or 's3'"
+where
+  normalizeUrl url := if url.back == '/' then url.dropEnd 1 |>.copy else url
 
 public instance : DecodeToml CacheService := ⟨fun v => do CacheService.decodeToml (← v.decodeTable) v.ref⟩
 

tests/lake/tests/cache/online-test.sh

@@ -35,8 +35,8 @@ with_cdn_endpoints() {
 }
 
 with_bogus_endpoints() {
-  LAKE_CACHE_ARTIFACT_ENDPOINT=https://example.com \
-  LAKE_CACHE_REVISION_ENDPOINT=https://example.com \
+  LAKE_CACHE_ARTIFACT_ENDPOINT=http://example.com \
+  LAKE_CACHE_REVISION_ENDPOINT=http://example.com \
   "$@"
 }
 
@@ -58,6 +58,12 @@ echo "# TESTS"
 test_err "must contain exactly one '/'" cache get --repo='invalid'
 test_err 'invalid characters in repository name' cache get --repo='!/invalid'
 
+# Test `--service` validation
+test_err 'service `bogus` not found in system configuration' \
+  cache get --service='bogus'
+test_err 'service `bogus` not found in system configuration'\
+  cache put bogus.jsonl --scope='bogus' --service='bogus'
+
 # Test `cache get` command errors for bad configurations
 test_err 'the `--platform` and `--toolchain` options do nothing' \
   cache get bogus.jsonl --scope='bogus' --platform='bogus' --wfail
@@ -94,10 +100,14 @@ test_exp -f .lake/outputs.jsonl
 test_cmd_eq 3 wc -l < .lake/outputs.jsonl
 test_cmd cp -r .lake/cache .lake/cache-backup
 
-# Test fetch from invalid URL
+# Test upload to an invalid URL
 with_bogus_endpoints test_err "failed to upload artifact" \
   cache put .lake/outputs.jsonl --scope='!/test'
 
+# Test upload to an invalid URL via system configuration
+LAKE_CONFIG=services.toml test_err "failed to upload artifact" \
+  cache put .lake/outputs.jsonl --scope='!/test' --service='bogus'
+
 # Test cache put/get with a custom endpoint
 with_upload_endpoints test_run cache put .lake/outputs.jsonl --scope='!/test'
 test_cmd rm -rf .lake/build "$LAKE_CACHE_DIR"
@@ -117,6 +127,10 @@ test_exp -d $LAKE_CACHE_DIR/revisions/test
 # Test `--force-download`
 with_cdn_endpoints test_out "downloading" cache get --scope='!/test' --force-download
 
+# Test download service configuration through system configuration
+LAKE_CONFIG=services.toml test_out "downloading" \
+  cache get --scope='!/test' --force-download --service=cdn
+
 # Test cache put/get with a set platform/toolchain
 with_upload_endpoints test_run cache put .lake/outputs.jsonl \
   --repo='leanprover/test' --platform=foo --toolchain=bar

tests/lake/tests/cache/services.toml

@@ -0,0 +1,11 @@
+[[cache.service]]
+name = "cdn"
+type = "s3"
+artifactEndpoint = "https://reservoir.lean-cache.cloud/a0"
+revisionEndpoint = "https://reservoir.lean-cache.cloud/r0"
+
+[[cache.service]]
+name = "bogus"
+type = "s3"
+artifactEndpoint = "http://example.com"
+revisionEndpoint = "http://example.com"