feat: lake: system-wide cache configuration

src/lake/Lake/Config.lean

@@ -23,6 +23,7 @@ public import Lake.Config.InputFile
 public import Lake.Config.InputFileConfig
 public import Lake.Config.InstallPath
 public import Lake.Config.Kinds
+public import Lake.Config.LakeConfig
 public import Lake.Config.Lang
 public import Lake.Config.LeanConfig
 public import Lake.Config.LeanExe

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 := ""
@@ -384,16 +384,17 @@ public structure CacheService where
     /-- Is this a Reservoir cache service configuration? -/
     isReservoir : Bool := false
     private apiEndpoint : String := ""
-    /--  Whether interpret the scope as a repository or not. -/
+    /-- Whether interpret the scope as a repository or not. -/
     private repoScope : Bool := false
 
 namespace CacheService
 
 /-! ### Constructors -/
 
 /-- Constructs a `CacheService` for a Reservoir endpoint. -/
-@[inline] public def reservoirService (apiEndpoint : String) (repoScope := false) : CacheService :=
-  {name? := some "reservoir", isReservoir := true, apiEndpoint, repoScope}
+@[inline] public def reservoirService
+  (apiEndpoint : String) (repoScope := false) (name? : Option String := some "reservoir")
+: CacheService := {name?, isReservoir := true, apiEndpoint, repoScope}
 
 /-- Constructs a `CacheService` to upload artifacts and/or outputs to an S3 endpoint. -/
 @[inline] public def uploadService
@@ -410,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/Env.lean

@@ -58,6 +58,8 @@ public structure Env where
   If `none`, no suitable system directory for the cache exists.
   -/
   lakeSystemCache? : Option Cache := none
+  /-- The path to the sytem Lake configuration (i.e., `LAKE_CONFIG`). -/
+  lakeConfig? : Option FilePath
   /-- The authentication key for cache uploads (i.e., `LAKE_CACHE_KEY`). -/
   cacheKey? : Option String
   /-- The base URL for artifact uploads and downloads from the cache (i.e., `LAKE_CACHE_ARTIFACT_ENDPOINT`). -/
@@ -95,6 +97,14 @@ public def getUserHome? : BaseIO (Option FilePath) := do
   else
     return none
 
+def getSystemCacheHomeAux? (userHome? : Option FilePath) : BaseIO (Option FilePath) := do
+  if let some cacheHome ← IO.getEnv "XDG_CACHE_HOME" then
+    return FilePath.mk cacheHome
+  else if let some userHome := userHome? then
+    return userHome / ".cache"
+  else
+    return none
+
 /-- Returns the system directory that can be used to store caches (if one exists). -/
 public def getSystemCacheHome? : BaseIO (Option FilePath) := do
   if let some cacheHome ← IO.getEnv "XDG_CACHE_HOME" then
@@ -119,15 +129,15 @@ namespace Env
 public def computeToolchain : BaseIO String := do
   return (← IO.getEnv "ELAN_TOOLCHAIN").getD Lean.toolchain
 
-def computeEnvCache? : BaseIO (Option Cache) := OptionT.run do
+@[inline] def computeEnvCache? : BaseIO (Option Cache) := OptionT.run do
   let cacheDir ← IO.getEnv "LAKE_CACHE_DIR"
   guard cacheDir.isEmpty
   return ⟨cacheDir⟩
 
-def computeSystemCache? : BaseIO (Option Cache) := do
-  return (← getSystemCacheHome?).map (⟨· / "lake"⟩)
+@[inline] def cacheOfSystem? (cacheHome? : Option FilePath) : Option Cache :=
+  cacheHome?.map (⟨· / "lake"⟩)
 
-def computeToolchainCache? (elan? : Option ElanInstall) (toolchain : String) : Option Cache := do
+@[inline] def cacheOfToolchain? (elan? : Option ElanInstall) (toolchain : String) : Option Cache := do
   let elan ← elan?
   guard !toolchain.isEmpty
   return elan.lakeToolchainCache toolchain
@@ -139,9 +149,9 @@ If `none`, no system directory for workspace the cache exists.
 public def computeCache? (elan? : Option ElanInstall) (toolchain : String) : BaseIO (Option Cache) := do
   if let some cache ← computeEnvCache? then
     return some cache
-  else if let some cache := computeToolchainCache? elan? toolchain then
+  else if let some cache := cacheOfToolchain? elan? toolchain then
     return some cache
-  else if let some cache ← computeSystemCache? then
+  else if let some cache ← cacheOfSystem? <$> getSystemCacheHome? then
     return some cache
   else
     return none
@@ -156,12 +166,14 @@ public def compute
 : EIO String Env := do
   let reservoirBaseUrl ← getUrlD "RESERVOIR_API_BASE_URL" "https://reservoir.lean-lang.org/api"
   let toolchain ← computeToolchain
-  addCacheDirs toolchain {
+  let userHome? ← getUserHome?
+  addCacheDirs userHome? toolchain {
     lake, lean, elan?,
     pkgUrlMap := ← computePkgUrlMap
     reservoirApiUrl := ← getUrlD "RESERVOIR_API_URL" s!"{reservoirBaseUrl}/v1"
     noCache := (noCache <|> (← IO.getEnv "LAKE_NO_CACHE").bind envToBool?).getD false
     enableArtifactCache? := (← IO.getEnv "LAKE_ARTIFACT_CACHE").bind envToBool?
+    lakeConfig? := (← IO.getEnv "LAKE_CONFIG") <|> userHome?.map (· / ".lake" / "config.toml" |>.toString)
     cacheKey? := (← IO.getEnv "LAKE_CACHE_KEY").map (·.trimAscii.copy)
     cacheArtifactEndpoint? := (← IO.getEnv "LAKE_CACHE_ARTIFACT_ENDPOINT").map normalizeUrl
     cacheRevisionEndpoint? := (← IO.getEnv "LAKE_CACHE_REVISION_ENDPOINT").map normalizeUrl
@@ -174,15 +186,16 @@ public def compute
     initPath := ← getSearchPath "PATH"
   }
 where
-  addCacheDirs toolchain env := do
+  addCacheDirs userHome? toolchain env := do
     if let some dir ← IO.getEnv "LAKE_CACHE_DIR" then
       if dir.isEmpty then
         return {env with noSystemCache := true}
       else
         return {env with lakeCache? := some ⟨dir⟩, lakeSystemCache? := some ⟨dir⟩}
-    else if let some cache := computeToolchainCache? elan? toolchain then
-      return {env with lakeCache? := some cache, lakeSystemCache? := ← computeSystemCache?}
-    else if let some cache ← computeSystemCache? then
+    else if let some cache := cacheOfToolchain? elan? toolchain then
+      let lakeSystemCache? ← cacheOfSystem? <$> getSystemCacheHomeAux? userHome?
+      return {env with lakeCache? := some cache, lakeSystemCache?}
+    else if let some cache ← cacheOfSystem? <$> getSystemCacheHomeAux? userHome? then
       return {env with lakeCache? := some cache, lakeSystemCache? := some cache}
     else
       return env
@@ -271,6 +284,7 @@ public def baseVars (env : Env) : Array (String × Option String)  :=
     ("ELAN_TOOLCHAIN", if env.toolchain.isEmpty then none else env.toolchain),
     ("LAKE", env.lake.lake.toString),
     ("LAKE_HOME", env.lake.home.toString),
+    ("LAKE_CONFIG", if let some path := env.lakeConfig? then path.toString else ""),
     ("LAKE_PKG_URL_MAP", toJson env.pkgUrlMap |>.compress),
     ("LAKE_NO_CACHE", toString env.noCache),
     ("LAKE_CACHE_KEY", env.cacheKey?),

src/lake/Lake/Config/LakeConfig.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+module
+
+prelude
+public import Lake.Config.Cache
+public import Lake.Config.MetaClasses
+meta import Lake.Config.Meta
+
+open System Lean
+
+namespace Lake
+
+public configuration CacheConfig where
+  defaultService : Name := .anonymous
+  services, service : Array CacheService := #[]
+  deriving Inhabited
+
+public configuration LakeConfig where
+  cache : CacheConfig := ∅
+  deriving Inhabited

src/lake/Lake/Config/Workspace.lean

@@ -11,8 +11,8 @@ public import Lake.Config.LeanExe
 public import Lake.Config.ExternLib
 public import Lake.Config.FacetConfig
 public import Lake.Config.TargetConfig
-meta import all Lake.Util.OpaqueType
-import Lake.Util.OpaqueType
+public import Lake.Config.LakeConfig
+meta import Lake.Util.OpaqueType
 import Lean.DocString.Syntax
 
 set_option doc.verso true
@@ -28,6 +28,8 @@ public structure Workspace : Type where
   root : Package
   /-- The detected {lean}`Lake.Env` of the workspace. -/
   lakeEnv : Lake.Env
+  /-- The Lake configuration from the system configuration file. -/
+  lakeConfig : LakeConfig := ∅
   /-- The Lake cache. -/
   lakeCache : Cache :=
     if root.bootstrap then lakeEnv.lakeSystemCache?.getD ⟨root.lakeDir / "cache"⟩

src/lake/Lake/Load/Config.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lake.Config.Env
+public import Lake.Config.LakeConfig
 public import Lake.Load.Manifest
 
 set_option doc.verso true
@@ -19,6 +20,8 @@ namespace Lake
 public structure LoadConfig where
   /-- The Lake environment of the load process. -/
   lakeEnv : Lake.Env
+  /-- The system Lake configuration. -/
+  lakeConfig : LakeConfig := ∅
   /--
   The CLI arguments Lake was run with.
   Used to perform a restart of Lake on a toolchain update.

src/lake/Lake/Load/Toml.lean

@@ -12,6 +12,7 @@ public import Lake.Toml.Decode
 import Lake.Toml.Load
 import Lean.Parser.Extension
 import Init.Omega
+meta import Lake.Config.LakeConfig
 meta import Lake.Config.InputFileConfig
 meta import Lake.Config.LeanExeConfig
 meta import Lake.Config.LeanLibConfig
@@ -325,6 +326,28 @@ public protected def Dependency.decodeToml (t : Table) (ref := Syntax.missing) :
 
 public instance : DecodeToml Dependency := ⟨fun v => do Dependency.decodeToml (← v.decodeTable) v.ref⟩
 
+/-! ## Dependency Configuration Decoders -/
+
+public protected def CacheService.decodeToml (t : Table) (ref := Syntax.missing) : EDecodeM CacheService := do
+  let typeVal ← t.decodeValue `type
+  match (← typeVal.decodeString) with
+  | "reservoir" => ensureDecode do
+    let name ← t.tryDecode `name ref
+    let repoScope ← t.tryDecode `repoScope 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 ← 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⟩
+
 /-! ## Package & Target Configuration Decoders -/
 
 public structure TomlFieldInfo (σ : Type) where
@@ -386,6 +409,9 @@ end
 
 local macro "gen_toml_decoders%" : command => do
   let cmds := #[]
+  -- Lake
+  let cmds ← genDecodeToml cmds ``CacheConfig
+  let cmds ← genDecodeToml cmds ``LakeConfig
   -- Targets
   let cmds ← genDecodeToml cmds ``LeanConfig
   let cmds ← genDecodeToml cmds ``LeanLibConfig
@@ -468,3 +494,22 @@ public def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do
         logError <| mkErrorStringWithPos ictx.fileName pos msg
   | .error log =>
     errorWithLog <| log.forM fun msg => do logError (← msg.toString)
+
+/-! ## System Configuration Loader -/
+
+/-- Load the system Lake configuration from a TOML file. -/
+public def loadLakeConfig (path : FilePath) : LogIO LakeConfig := do
+  let input ← IO.FS.readFile path
+  let ictx := mkInputContext input path.toString
+  match (← loadToml ictx |>.toBaseIO) with
+  | .ok table =>
+    let .ok pkg errs := EStateM.run (s := #[]) do
+      LakeConfig.decodeToml table
+    if errs.isEmpty then
+      return pkg
+    else
+      errorWithLog <| errs.forM fun {ref, msg} =>
+        let pos := ictx.fileMap.toPosition <| ref.getPos?.getD 0
+        logError <| mkErrorStringWithPos ictx.fileName pos msg
+  | .error log =>
+    errorWithLog <| log.forM fun msg => do logError (← msg.toString)

src/lake/Lake/Load/Workspace.lean

@@ -34,6 +34,7 @@ public def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
   let ws : Workspace := {
     root
     lakeEnv := config.lakeEnv
+    lakeConfig := config.lakeConfig
     lakeArgs? := config.lakeArgs?
     facetConfigs := initFacetConfigs
   }

src/lake/Lake/Toml/Decode.lean

@@ -25,8 +25,10 @@ public structure Toml.DecodeError where
   ref : Syntax
   msg : String
 
+/-- Monad for decoders that do not abort. -/
 public abbrev Toml.DecodeM := EStateM Empty (Array DecodeError)
 
+/-- Monad for decoders that may abort. -/
 public abbrev Toml.EDecodeM := EStateM Unit (Array DecodeError)
 
 public class DecodeToml (α : Type) where

src/lake/Lake/Util/OpaqueType.lean

@@ -3,12 +3,11 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-module
+module -- shake: keep-all
 
 prelude
 public meta import Lake.Util.Binder
-public import Init.Notation
-import Lake.Util.Binder
+public import Init.Prelude
 
 /-!
 This module provides utilities for defining simple opaque types

tests/CMakeLists.txt

@@ -200,7 +200,7 @@ endforeach(T)
 # online: downloads remote repositories
 file(
   GLOB_RECURSE LEANLAKETESTS
-  #"${LEAN_SOURCE_DIR}/../tests/lake/tests/test.sh"
+  "${LEAN_SOURCE_DIR}/../tests/lake/tests/test.sh"
   "${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh"
   "${LEAN_SOURCE_DIR}/../tests/lake/tests/shake/test.sh"
 )

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