diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean
index 44be2002ea2b..28ae124fc6b0 100644
--- a/src/lake/Lake/Build/Actions.lean
+++ b/src/lake/Lake/Build/Actions.lean
@@ -108,15 +108,16 @@ def compileExe
   }
 
 /-- Download a file using `curl`, clobbering any existing file. -/
-def download  (url : String) (file : FilePath) : LogIO PUnit := do
+def download
+  (url : String) (file : FilePath) (headers : Array String := #[])
+: LogIO PUnit := do
   if (← file.pathExists) then
     IO.FS.removeFile file
   else
     createParentDirs file
-  proc (quiet := true) {
-    cmd := "curl"
-    args := #["-s", "-S", "-f", "-o", file.toString, "-L", url]
-  }
+  let args := #["-s", "-S", "-f", "-o", file.toString, "-L", url]
+  let args := headers.foldl (init := args) (· ++ #["-H", ·])
+  proc (quiet := true) {cmd := "curl", args}
 
 /-- Unpack an archive `file` using `tar` into the directory `dir`. -/
 def untar (file : FilePath) (dir : FilePath) (gzip := true) : LogIO PUnit := do
diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean
index 39ca7951656c..cabed7f25051 100644
--- a/src/lake/Lake/Build/Basic.lean
+++ b/src/lake/Lake/Build/Basic.lean
@@ -17,10 +17,13 @@ def noBuildCode : ExitCode := 3
 
 /-- Configuration options for a Lake build. -/
 structure BuildConfig where
+  /-- Use modification times for trace checking. -/
   oldMode : Bool := false
+  /-- Whether to trust `.hash` files. -/
   trustHash : Bool := true
   /-- Early exit if a target has to be rebuilt. -/
   noBuild : Bool := false
+  /-- Verbosity level (`-q`, `-v`, or neither). -/
   verbosity : Verbosity := .normal
   /--
   Fail the top-level build if entries of at least this level have been logged.
diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean
index 67c32462bb86..663db80c6723 100644
--- a/src/lake/Lake/Build/Facets.lean
+++ b/src/lake/Lake/Build/Facets.lean
@@ -117,19 +117,53 @@ module_data o.noexport : BuildJob FilePath
 /-! ## Package Facets -/
 
 /--
-A package's *optional* cloud build release.
-Will not cause the whole build to fail if the release cannot be fetched.
+A package's *optional* cached build archive (e.g., from Reservoir or GitHub).
+Will NOT cause the whole build to fail if the archive cannot be fetched.
 -/
-abbrev Package.optReleaseFacet := `optRelease
+abbrev Package.optBuildCacheFacet := `optCache
+package_data optCache : BuildJob Bool
+
+/--
+A package's cached build archive (e.g., from Reservoir or GitHub).
+Will cause the whole build to fail if the archive cannot be fetched.
+-/
+abbrev Package.buildCacheFacet := `cache
+package_data cache : BuildJob Unit
+
+/--
+A package's *optional* build archive from Reservoir.
+Will NOT cause the whole build to fail if the barrel cannot be fetched.
+-/
+abbrev Package.optReservoirBarrelFacet := `optBarrel
+package_data optBarrel : BuildJob Bool
+
+/--
+A package's Reservoir build archive from Reservoir.
+Will cause the whole build to fail if the barrel cannot be fetched.
+-/
+abbrev Package.reservoirBarrelFacet := `barrel
+package_data barrel : BuildJob Unit
+
+/--
+A package's *optional* build archive from a GitHub release.
+Will NOT cause the whole build to fail if the release cannot be fetched.
+-/
+abbrev Package.optGitHubReleaseFacet := `optRelease
 package_data optRelease : BuildJob Bool
 
+@[deprecated (since := "2024-09-27")]
+abbrev Package.optReleaseFacet := optGitHubReleaseFacet
+
 /--
-A package's cloud build release.
+A package's build archive from a GitHub release.
 Will cause the whole build to fail if the release cannot be fetched.
 -/
-abbrev Package.releaseFacet := `release
+abbrev Package.gitHubReleaseFacet := `release
 package_data release : BuildJob Unit
 
+@[deprecated (since := "2024-09-27")]
+abbrev Package.releaseFacet := gitHubReleaseFacet
+
 /-- A package's `extraDepTargets` mixed with its transitive dependencies'. -/
 abbrev Package.extraDepFacet := `extraDep
 package_data extraDep : BuildJob Unit
diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean
index 9427e367b1e2..fcc2f517cf30 100644
--- a/src/lake/Lake/Build/Info.lean
+++ b/src/lake/Lake/Build/Info.lean
@@ -216,13 +216,35 @@ end Module
 abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
   .packageFacet self facet
 
-@[inherit_doc releaseFacet]
-abbrev Package.release (self : Package) : BuildInfo :=
-  self.facet releaseFacet
+@[inherit_doc buildCacheFacet]
+abbrev Package.buildCache (self : Package) : BuildInfo :=
+  self.facet buildCacheFacet
 
-@[inherit_doc optReleaseFacet]
-abbrev Package.optRelease (self : Package) : BuildInfo :=
-  self.facet optReleaseFacet
+@[inherit_doc optBuildCacheFacet]
+abbrev Package.optBuildCache (self : Package) : BuildInfo :=
+  self.facet optBuildCacheFacet
+
+@[inherit_doc reservoirBarrelFacet]
+abbrev Package.reservoirBarrel (self : Package) : BuildInfo :=
+  self.facet reservoirBarrelFacet
+
+@[inherit_doc optReservoirBarrelFacet]
+abbrev Package.optReservoirBarrel (self : Package) : BuildInfo :=
+  self.facet optReservoirBarrelFacet
+
+@[inherit_doc gitHubReleaseFacet]
+abbrev Package.gitHubRelease (self : Package) : BuildInfo :=
+  self.facet gitHubReleaseFacet
+
+@[inherit_doc optGitHubReleaseFacet]
+abbrev Package.optGitHubRelease (self : Package) : BuildInfo :=
+  self.facet optGitHubReleaseFacet
+
+@[deprecated (since := "2024-09-27")]
+abbrev Package.release := @gitHubRelease
+
+@[deprecated (since := "2024-09-27")]
+abbrev Package.optRelease := @optGitHubRelease
 
 @[inherit_doc extraDepFacet]
 abbrev Package.extraDep (self : Package) : BuildInfo :=
diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean
index 03bdb3089591..da268d950e60 100644
--- a/src/lake/Lake/Build/Package.lean
+++ b/src/lake/Lake/Build/Package.lean
@@ -7,6 +7,7 @@ import Lake.Util.Git
 import Lake.Util.Sugar
 import Lake.Build.Common
 import Lake.Build.Targets
+import Lake.Reservoir
 
 /-! # Package Facet Builds
 Build function definitions for a package's builtin facets.
@@ -24,14 +25,44 @@ def Package.recComputeDeps (self : Package) : FetchM (Array Package) := do
 def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
   mkFacetConfig Package.recComputeDeps
 
-/-- Tries to download and unpack the package's prebuilt release archive (from GitHub). -/
-def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Unit) := do
-  (← self.optRelease.fetch).bindSync fun success t => do
+/--
+Tries to download and unpack the package's cached build archive
+(e.g., from Reservoir or GitHub).
+-/
+private def Package.fetchOptBuildCacheCore (self : Package) : FetchM (BuildJob Bool) := do
+  if self.preferReleaseBuild then
+    self.optGitHubRelease.fetch
+  else
+    self.optReservoirBarrel.fetch
+
+/-- The `PackageFacetConfig` for the builtin `optBuildCacheFacet`. -/
+def Package.optBuildCacheFacetConfig : PackageFacetConfig optBuildCacheFacet :=
+  mkFacetJobConfig (·.fetchOptBuildCacheCore)
+
+/-- Tries to download the package's build cache (if configured). -/
+def Package.maybeFetchBuildCache (self : Package) : FetchM (BuildJob Bool) := do
+  if (← getNoCache) then
+    return pure true
+  else
+    self.optBuildCache.fetch
+
+/--
+Tries to download and unpack the package's cached build archive
+(e.g., from Reservoir or GitHub). Prints a warning on failure.
+-/
+def Package.maybeFetchBuildCacheWithWarning (self : Package) := do
+  let job ← self.maybeFetchBuildCache
+  job.bindSync fun success t => do
     unless success do
+      let facet := if self.preferReleaseBuild then
+        optGitHubReleaseFacet else optReservoirBarrelFacet
       logWarning s!"building from source; \
-        failed to fetch cloud release (see '{self.name}:optRelease' for details)"
+        failed to fetch cloud release (see '{self.name}:{facet}' for details)"
     return ((), t)
 
+@[deprecated maybeFetchBuildCacheWithWarning (since := "2024-09-27")]
+def Package.fetchOptRelease := @maybeFetchBuildCacheWithWarning
+
 /--
 Build the `extraDepTargets` for the package and its transitive dependencies.
 Also fetch pre-built releases for the package's' dependencies.
@@ -42,9 +73,9 @@ def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
   -- Build dependencies' extra dep targets
   for dep in self.deps do
     job := job.mix <| ← dep.extraDep.fetch
-  -- Fetch pre-built release if desired and this package is a dependency
-  if self.name ≠ (← getWorkspace).root.name ∧ self.preferReleaseBuild then
-    job := job.add <| ← self.fetchOptRelease
+  -- Fetch build cache if this package is a dependency
+  if self.name ≠ (← getWorkspace).root.name then
+    job := job.add <| ← self.maybeFetchBuildCacheWithWarning
   -- Build this package's extra dep targets
   for target in self.extraDepTargets do
     job := job.mix <| ← self.fetchTargetJob target
@@ -54,60 +85,126 @@ def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
 def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
   mkFacetJobConfig Package.recBuildExtraDepTargets
 
-/-- Tries to download and unpack the package's prebuilt release archive (from GitHub). -/
-def Package.fetchOptReleaseCore (self : Package) : FetchM (BuildJob Bool) :=
-  withRegisterJob s!"{self.name}:optRelease" (optional := true) <| Job.async do
+/-- Compute the package's Reservoir barrel URL. -/
+def Package.getBarrelUrl (self : Package) : JobM String := do
+  if self.scope.isEmpty then
+    error "package has no Reservoir scope"
+  let repo := GitRepo.mk self.dir
+  let some rev ← repo.getHeadRevision?
+    | error "failed to resolve HEAD revision"
+  let pkgName := self.name.toString (escape := false)
+  let env ← getLakeEnv
+  let mut url := Reservoir.pkgApiUrl env self.scope pkgName
+  if env.toolchain.isEmpty then
+    error "Lean toolchain not known; Reservoir only hosts builds for known toolchains"
+  url := s!"{url}/barrel?rev={rev}&toolchain={uriEncode env.toolchain}"
+  return url
+
+/-- Compute the package's GitHub release URL. -/
+def Package.getReleaseUrl (self : Package) : JobM String := do
   let repo := GitRepo.mk self.dir
   let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
   let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
-    | logError s!"release repository URL not known; \
+    | error "release repository URL not known; \
         the package may need to set 'releaseRepo'"
-      updateAction .fetch
-      return (false, .nil)
   let some tag ← repo.findTag?
     | let rev ← if let some rev ← repo.getHeadRevision? then pure s!" '{rev}'" else pure ""
-      logError s!"no release tag found for revision{rev}"
-      updateAction .fetch
-      return (false, .nil)
-  let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
+      error s!"no release tag found for revision{rev}"
+  return s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
+
+/-- Tries to download and unpack a build archive for the package from a URL. -/
+def Package.fetchBuildArchive
+  (self : Package) (url : String) (archiveFile : FilePath)
+  (headers : Array String := #[])
+: JobM PUnit := do
   let depTrace := Hash.ofString url
-  let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
-  let upToDate ← buildUnlessUpToDate? (action := .fetch) self.buildArchiveFile depTrace traceFile do
-    logVerbose s!"downloading {url}"
-    download url self.buildArchiveFile
+  let traceFile := archiveFile.addExtension "trace"
+  let upToDate ← buildUnlessUpToDate? (action := .fetch) archiveFile depTrace traceFile do
+    download url archiveFile headers
   unless upToDate && (← self.buildDir.pathExists) do
     updateAction .fetch
-    logVerbose s!"unpacking {self.name}:{tag}:{self.buildArchive}"
-    untar self.buildArchiveFile self.buildDir
-  return (true, .nil)
+    untar archiveFile self.buildDir
 
-/-- The `PackageFacetConfig` for the builtin `optReleaseFacet`. -/
-def Package.optReleaseFacetConfig : PackageFacetConfig optReleaseFacet :=
-  mkFacetJobConfig (·.fetchOptReleaseCore)
+@[inline]
+private def Package.mkOptBuildArchiveFacetConfig
+  {facet : Name} (archiveFile : Package → FilePath)
+  (getUrl : Package → JobM String) (headers : Array String := #[])
+  [FamilyDef PackageData facet (BuildJob Bool)]
+: PackageFacetConfig facet := mkFacetJobConfig fun pkg =>
+  withRegisterJob s!"{pkg.name}:{facet}" (optional := true) <| Job.async do
+  try
+    let url ← getUrl pkg
+    pkg.fetchBuildArchive url (archiveFile pkg) headers
+    return (true, .nil)
+  catch _ =>
+    updateAction .fetch
+    return (false, .nil)
 
-/-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/
-def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
+@[inline]
+private def Package.mkBuildArchiveFacetConfig
+  {facet : Name} (optFacet : Name) (what : String)
+  [FamilyDef PackageData facet (BuildJob Unit)]
+  [FamilyDef PackageData optFacet (BuildJob Bool)]
+: PackageFacetConfig facet :=
   mkFacetJobConfig fun pkg =>
-    withRegisterJob s!"{pkg.name}:release" do
-      (← pkg.optRelease.fetch).bindSync fun success t => do
+    withRegisterJob s!"{pkg.name}:{facet}" do
+      (← fetch <| pkg.facet optFacet).bindSync fun success t => do
         unless success do
-          error s!"failed to fetch cloud release (see '{pkg.name}:optRelease' for details)"
+          error s!"failed to fetch {what} (see '{pkg.name}:{optFacet}' for details)"
         return ((), t)
 
-/-- Perform a build job after first checking for an (optional) cloud release for the package. -/
-def Package.afterReleaseAsync (self : Package) (build : SpawnM (Job α)) : FetchM (Job α) := do
-  if self.preferReleaseBuild ∧ self.name ≠ (← getRootPackage).name then
-    (← self.optRelease.fetch).bindAsync fun _ _ => build
+/-- The `PackageFacetConfig` for the builtin `buildCacheFacet`. -/
+def Package.buildCacheFacetConfig : PackageFacetConfig buildCacheFacet :=
+  mkBuildArchiveFacetConfig optBuildCacheFacet "build cache"
+
+/-- The `PackageFacetConfig` for the builtin `optReservoirBarrelFacet`. -/
+def Package.optBarrelFacetConfig : PackageFacetConfig optReservoirBarrelFacet :=
+  mkOptBuildArchiveFacetConfig barrelFile getBarrelUrl Reservoir.lakeHeaders
+
+/-- The `PackageFacetConfig` for the builtin `reservoirBarrelFacet`. -/
+def Package.barrelFacetConfig : PackageFacetConfig reservoirBarrelFacet :=
+  mkBuildArchiveFacetConfig optReservoirBarrelFacet "Reservoir barrel"
+
+/-- The `PackageFacetConfig` for the builtin `optGitHubReleaseFacet`. -/
+def Package.optGitHubReleaseFacetConfig : PackageFacetConfig optGitHubReleaseFacet :=
+  mkOptBuildArchiveFacetConfig buildArchiveFile getReleaseUrl
+
+@[deprecated (since := "2024-09-27")]
+abbrev Package.optReleaseFacetConfig := optGitHubReleaseFacetConfig
+
+/-- The `PackageFacetConfig` for the builtin `gitHubReleaseFacet`. -/
+def Package.gitHubReleaseFacetConfig : PackageFacetConfig gitHubReleaseFacet :=
+  mkBuildArchiveFacetConfig optGitHubReleaseFacet "GitHub release"
+
+@[deprecated (since := "2024-09-27")]
+abbrev Package.releaseFacetConfig := gitHubReleaseFacetConfig
+
+/--
+Perform a build job after first checking for an (optional) cached build
+for the package (e.g., from Reservoir or GitHub).
+-/
+def Package.afterBuildCacheAsync (self : Package) (build : SpawnM (Job α)) : FetchM (Job α) := do
+  if self.name ≠ (← getRootPackage).name then
+    (← self.maybeFetchBuildCache).bindAsync fun _ _ => build
   else
     build
 
-/-- Perform a build after first checking for an (optional) cloud release for the package. -/
-def Package.afterReleaseSync (self : Package) (build : JobM α) : FetchM (Job α) := do
-  if self.preferReleaseBuild ∧ self.name ≠ (← getRootPackage).name then
-    (← self.optRelease.fetch).bindSync fun _ _ => build
+@[deprecated afterBuildCacheAsync (since := "2024-09-27")]
+def Package.afterReleaseAsync := @afterBuildCacheAsync
+
+/--
+ Perform a build after first checking for an (optional) cached build
+ for the package (e.g., from Reservoir or GitHub).
+-/
+def Package.afterBuildCacheSync (self : Package) (build : JobM α) : FetchM (Job α) := do
+  if self.name ≠ (← getRootPackage).name then
+    (← self.maybeFetchBuildCache).bindSync fun _ _ => build
   else
     Job.async build
 
+@[deprecated afterBuildCacheSync (since := "2024-09-27")]
+def Package.afterReleaseSync := @afterBuildCacheSync
+
 open Package in
 /--
 A package facet name to build function map that contains builders for
@@ -117,5 +214,9 @@ def initPackageFacetConfigs : DNameMap PackageFacetConfig :=
   DNameMap.empty
   |>.insert depsFacet depsFacetConfig
   |>.insert extraDepFacet extraDepFacetConfig
-  |>.insert optReleaseFacet optReleaseFacetConfig
-  |>.insert releaseFacet releaseFacetConfig
+  |>.insert optBuildCacheFacet optBuildCacheFacetConfig
+  |>.insert buildCacheFacet buildCacheFacetConfig
+  |>.insert optReservoirBarrelFacet optBarrelFacetConfig
+  |>.insert reservoirBarrelFacet barrelFacetConfig
+  |>.insert optGitHubReleaseFacet optGitHubReleaseFacetConfig
+  |>.insert gitHubReleaseFacet gitHubReleaseFacetConfig
diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean
index cc6a1294ebcf..23c01a5b1bbc 100644
--- a/src/lake/Lake/CLI/Help.lean
+++ b/src/lake/Lake/CLI/Help.lean
@@ -48,6 +48,8 @@ BASIC OPTIONS:
   --update, -U          update manifest before building
   --reconfigure, -R     elaborate configuration files instead of using OLeans
   --no-build            exit immediately if a build target is not up-to-date
+  --no-cache            build packages locally; do not download build caches
+  --try-cache           attempt to download build caches for supported packages
 
 OUTPUT OPTIONS:
   --quiet, -q           hide informational logs and the progress indicator
diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index 5b7d16c9aa63..5b24a9d59c35 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -40,6 +40,7 @@ structure LakeOptions where
   oldMode : Bool := false
   trustHash : Bool := true
   noBuild : Bool := false
+  noCache : Option Bool := none
   failLv : LogLevel := .error
   outLv? : Option LogLevel := .none
   ansiMode : AnsiMode := .auto
@@ -66,7 +67,7 @@ def LakeOptions.getInstall (opts : LakeOptions) : Except CliError (LeanInstall 
 /-- Compute the Lake environment based on `opts`. Error if an install is missing. -/
 def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
   Env.compute (← opts.getLakeInstall) (← opts.getLeanInstall) opts.elanInstall?
-    |>.adaptExcept fun msg => .invalidEnv msg
+    opts.noCache |>.adaptExcept fun msg => .invalidEnv msg
 
 /-- Make a `LoadConfig` from a `LakeOptions`. -/
 def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
@@ -173,6 +174,8 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--reconfigure" => modifyThe LakeOptions ({· with reconfigure := true})
 | "--old"         => modifyThe LakeOptions ({· with oldMode := true})
 | "--no-build"    => modifyThe LakeOptions ({· with noBuild := true})
+| "--no-cache"    => modifyThe LakeOptions ({· with noCache := true})
+| "--try-cache"   => modifyThe LakeOptions ({· with noCache := false})
 | "--rehash"      => modifyThe LakeOptions ({· with trustHash := false})
 | "--wfail"       => modifyThe LakeOptions ({· with failLv := .warning})
 | "--iofail"      => modifyThe LakeOptions ({· with failLv := .info})
diff --git a/src/lake/Lake/Config/Env.lean b/src/lake/Lake/Config/Env.lean
index dd2321635403..d15081823618 100644
--- a/src/lake/Lake/Config/Env.lean
+++ b/src/lake/Lake/Config/Env.lean
@@ -31,6 +31,11 @@ structure Env where
   githashOverride : String
   /-- A name-to-URL mapping of URL overrides for the named packages. -/
   pkgUrlMap : NameMap String
+  /--
+  Whether to disable downloading build caches for packages. Set via `LAKE_NO_CACHE`.
+  Can be overridden on a per-command basis with`--try-cache`.
+  -/
+  noCache : Bool
   /-- The initial Elan toolchain of the environment (i.e., `ELAN_TOOLCHAIN`). -/
   initToolchain : String
   /-- The initial Lean library search path of the environment (i.e., `LEAN_PATH`). -/
@@ -45,13 +50,20 @@ structure Env where
 
 namespace Env
 
-/-- Compute an `Lake.Env` object from the given installs and set environment variables. -/
-def compute (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstall) : EIO String Env := do
+/--
+Compute a `Lake.Env` object from the given installs
+and the set environment variables.
+-/
+def compute
+  (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstall)
+  (noCache : Option Bool := none)
+: EIO String Env := do
   let reservoirBaseUrl ← getUrlD "RESERVOIR_API_BASE_URL" "https://reservoir.lean-lang.org/api"
   return {
     lake, lean, elan?,
     pkgUrlMap := ← computePkgUrlMap
     reservoirApiUrl := ← getUrlD "RESERVOIR_API_URL" s!"{reservoirBaseUrl}/v1"
+    noCache := (noCache <|> (← IO.getEnv "LAKE_NO_CACHE").bind toBool?).getD false
     githashOverride := (← IO.getEnv "LEAN_GITHASH").getD ""
     initToolchain := (← IO.getEnv "ELAN_TOOLCHAIN").getD ""
     initLeanPath := ← getSearchPath "LEAN_PATH",
@@ -60,6 +72,10 @@ def compute (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstal
     initPath := ← getSearchPath "PATH"
   }
 where
+  toBool? (o : String) : Option Bool :=
+    if ["y", "yes", "t", "true", "on", "1"].contains o.toLower then true
+    else if ["n", "no", "f", "false", "off", "0"].contains o.toLower then false
+    else none
   computePkgUrlMap := do
     let some urlMapStr ← IO.getEnv "LAKE_PKG_URL_MAP" | return {}
     match Json.parse urlMapStr |>.bind fromJson? with
diff --git a/src/lake/Lake/Config/Monad.lean b/src/lake/Lake/Config/Monad.lean
index 0ac8db9607c5..ab5154db55b7 100644
--- a/src/lake/Lake/Config/Monad.lean
+++ b/src/lake/Lake/Config/Monad.lean
@@ -128,6 +128,10 @@ variable [MonadLakeEnv m]
 
 variable [Functor m]
 
+/-- Get the `LAKE_NO_CACHE`/`--no-cache` LAke configuration. -/
+@[inline] def getNoCache [Functor m] [MonadBuild m] : m Bool :=
+  (·.noCache) <$> getLakeEnv
+
 /-- Get the `LAKE_PACKAGE_URL_MAP` for the Lake environment. Empty if none. -/
 @[inline] def getPkgUrlMap : m (NameMap String) :=
   (·.pkgUrlMap) <$> getLakeEnv
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index 30cd46b94bb2..2e9f6ea8f025 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -376,8 +376,10 @@ structure Package where
   relConfigFile : FilePath
   /-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/
   relManifestFile : FilePath := config.manifestFile.getD defaultManifestFile
+  /-- The package's scope (e.g., in Reservoir). -/
+  scope : String := ""
   /-- The URL to this package's Git remote. -/
-  remoteUrl? : Option String := none
+  remoteUrl : String := ""
   /-- (Opaque references to) the package's direct dependencies. -/
   opaqueDeps : Array OpaquePackage := #[]
   /-- Dependency configurations for the package. -/
@@ -555,6 +557,10 @@ namespace Package
 @[inline] def releaseRepo? (self : Package) : Option String :=
   self.config.releaseRepo <|> self.config.releaseRepo?
 
+/-- The packages `remoteUrl` as an `Option` (`none` if empty). -/
+@[inline] def remoteUrl? (self : Package) : Option String :=
+  if self.remoteUrl.isEmpty then some self.remoteUrl else none
+
 /-- The package's `buildArchive`/`buildArchive?` configuration. -/
 @[inline] def buildArchive (self : Package) : String :=
   self.config.buildArchive
@@ -563,6 +569,10 @@ namespace Package
 @[inline] def buildArchiveFile (self : Package) : FilePath :=
   self.lakeDir / self.buildArchive
 
+/-- The path where Lake stores the package's barrel (downloaded from Reservoir). -/
+@[inline] def barrelFile (self : Package) : FilePath :=
+  self.lakeDir / "build.barrel"
+
 /-- The package's `preferReleaseBuild` configuration. -/
 @[inline] def preferReleaseBuild (self : Package) : Bool :=
   self.config.preferReleaseBuild
diff --git a/src/lake/Lake/Load/Config.lean b/src/lake/Lake/Load/Config.lean
index 2de9c24661c5..237578cd8c36 100644
--- a/src/lake/Lake/Load/Config.lean
+++ b/src/lake/Lake/Load/Config.lean
@@ -28,8 +28,10 @@ structure LoadConfig where
   leanOpts : Options := {}
   /-- If `true`, Lake will elaborate configuration files instead of using OLeans. -/
   reconfigure : Bool := false
+  /-- The package's scope (e.g., in Reservoir). -/
+  scope : String := ""
   /-- The URL to this package's Git remote (if any). -/
-  remoteUrl? : Option String := none
+  remoteUrl : String := ""
 
 /-- The full path to loaded package's directory. -/
 @[inline] def LoadConfig.pkgDir (cfg : LoadConfig) : FilePath :=
diff --git a/src/lake/Lake/Load/Lean.lean b/src/lake/Lake/Load/Lean.lean
index 95fc73677470..08aab790c347 100644
--- a/src/lake/Lake/Load/Lean.lean
+++ b/src/lake/Lake/Load/Lean.lean
@@ -29,6 +29,7 @@ def loadLeanConfig (cfg : LoadConfig)
     relDir := cfg.relPkgDir
     config := pkgConfig
     relConfigFile := cfg.relConfigFile
-    remoteUrl? := cfg.remoteUrl?
+    scope := cfg.scope
+    remoteUrl := cfg.remoteUrl
   }
   return (← pkg.loadFromEnv configEnv cfg.leanOpts, configEnv)
diff --git a/src/lake/Lake/Load/Materialize.lean b/src/lake/Lake/Load/Materialize.lean
index 9867672b8f37..cf618aaf5342 100644
--- a/src/lake/Lake/Load/Materialize.lean
+++ b/src/lake/Lake/Load/Materialize.lean
@@ -79,7 +79,7 @@ structure MaterializedDep where
   URL for the materialized package.
   Used as the endpoint from which to fetch cloud releases for the package.
   -/
-  remoteUrl? : Option String
+  remoteUrl : String
   /-- The manifest entry for the dependency. -/
   manifestEntry : PackageEntry
   deriving Inhabited
@@ -87,6 +87,9 @@ structure MaterializedDep where
 @[inline] def MaterializedDep.name (self : MaterializedDep) :=
   self.manifestEntry.name
 
+@[inline] def MaterializedDep.scope (self : MaterializedDep) :=
+  self.manifestEntry.scope
+
 /-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
 @[inline] def MaterializedDep.manifestFile? (self : MaterializedDep) :=
   self.manifestEntry.manifestFile?
@@ -109,13 +112,13 @@ def Dependency.materialize
       let relPkgDir := relParentDir / dir
       return {
         relPkgDir
-        remoteUrl? := none
+        remoteUrl := ""
         manifestEntry := mkEntry <| .path relPkgDir
       }
     | .git url inputRev? subDir? => do
       let sname := dep.name.toString (escape := false)
-      let repoUrl? := Git.filterUrl? url
-      materializeGit sname (relPkgsDir / sname) url repoUrl? inputRev? subDir?
+      let repoUrl := Git.filterUrl? url |>.getD ""
+      materializeGit sname (relPkgsDir / sname) url repoUrl inputRev? subDir?
   else
     if dep.scope.isEmpty then
       error s!"{dep.name}: ill-formed dependency: \
@@ -126,26 +129,26 @@ def Dependency.materialize
       else
         error s!"{dep.name} unsupported dependency version format '{ver}' (should be \"git#>rev>\")"
     let depName := dep.name.toString (escape := false)
-    let some pkg ← fetchReservoirPkg? lakeEnv dep.scope depName
+    let some pkg ← Reservoir.fetchPkg? lakeEnv dep.scope depName
       | error s!"{dep.scope}/{depName}: could not materialize package: \
         dependency has no explicit source and was not found on Reservoir"
     let relPkgDir := relPkgsDir / pkg.name
     match pkg.gitSrc? with
     | some (.git _ url githubUrl? defaultBranch? subDir?) =>
-      materializeGit pkg.fullName relPkgDir url githubUrl? (verRev? <|> defaultBranch?) subDir?
+      materializeGit pkg.fullName relPkgDir url
+        (githubUrl?.getD "") (verRev? <|> defaultBranch?) subDir?
     | _ => error s!"{pkg.fullName}: Git source not found on Reservoir"
 where
   mkEntry src : PackageEntry :=
     {name := dep.name, scope := dep.scope, inherited, src}
-  materializeGit name relPkgDir gitUrl remoteUrl? inputRev? subDir? : LogIO MaterializedDep := do
+  materializeGit name relPkgDir gitUrl remoteUrl inputRev? subDir? : LogIO MaterializedDep := do
     let repo := GitRepo.mk (wsDir / relPkgDir)
     let gitUrl := lakeEnv.pkgUrlMap.find? dep.name |>.getD gitUrl
     materializeGitRepo name repo gitUrl inputRev?
     let rev ← repo.getHeadRevision
     let relPkgDir := if let some subDir := subDir? then relPkgDir / subDir else relPkgDir
     return {
-      relPkgDir
-      remoteUrl? := remoteUrl?
+      relPkgDir, remoteUrl
       manifestEntry := mkEntry <| .git gitUrl rev inputRev? subDir?
     }
 
@@ -160,7 +163,7 @@ def PackageEntry.materialize
   | .path (dir := relPkgDir) .. =>
     return {
       relPkgDir
-      remoteUrl? := none
+      remoteUrl := ""
       manifestEntry
     }
   | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do
@@ -187,6 +190,6 @@ def PackageEntry.materialize
     let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
     return {
       relPkgDir
-      remoteUrl? := Git.filterUrl? url
+      remoteUrl := Git.filterUrl? url |>.getD ""
       manifestEntry
     }
diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean
index b287e0fd5fad..26607f2d43e6 100644
--- a/src/lake/Lake/Load/Package.lean
+++ b/src/lake/Lake/Load/Package.lean
@@ -40,7 +40,7 @@ def loadPackageCore
       error s!"{name}: configuration file not found: {cfg.configFile}"
     match ext with
     | "lean" => (·.map id some) <$> loadLeanConfig cfg
-    | "toml" => ((·,none)) <$> loadTomlConfig cfg.pkgDir cfg.relPkgDir cfg.relConfigFile
+    | "toml" => ((·,none)) <$> loadTomlConfig cfg
     | _ => error s!"{name}: configuration has unsupported file extension: {cfg.configFile}"
   else
     let relLeanFile := cfg.relConfigFile.addExtension "lean"
@@ -55,7 +55,7 @@ def loadPackageCore
       (·.map id some) <$> loadLeanConfig {cfg with relConfigFile := relLeanFile}
     else
       if tomlExists then
-        ((·,none)) <$> loadTomlConfig cfg.pkgDir cfg.relPkgDir relTomlFile
+        ((·,none)) <$> loadTomlConfig {cfg with relConfigFile := relTomlFile}
       else
         error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}"
 
diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean
index d32470519b17..a5681a42da71 100644
--- a/src/lake/Lake/Load/Resolve.lean
+++ b/src/lake/Lake/Load/Resolve.lean
@@ -34,7 +34,8 @@ def loadDepPackage
     relPkgDir := dep.relPkgDir
     relConfigFile := dep.configFile
     lakeOpts, leanOpts, reconfigure
-    remoteUrl? := dep.remoteUrl?
+    scope := dep.scope
+    remoteUrl := dep.remoteUrl
   }
   if let some env := env? then
     let ws ← IO.ofExcept <| ws.addFacetsFromEnv env leanOpts
diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean
index ad20492aca46..79a399cd65f7 100644
--- a/src/lake/Lake/Load/Toml.lean
+++ b/src/lake/Lake/Load/Toml.lean
@@ -305,10 +305,9 @@ instance : DecodeToml Dependency := ⟨fun v => do Dependency.decodeToml (← v.
 Load a `Package` from a TOML Lake configuration file.
 The resulting package does not yet include any dependencies.
 -/
-def loadTomlConfig (dir relDir relConfigFile : FilePath) : LogIO Package := do
-  let configFile := dir / relConfigFile
-  let input ← IO.FS.readFile configFile
-  let ictx := mkInputContext input relConfigFile.toString
+def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do
+  let input ← IO.FS.readFile cfg.configFile
+  let ictx := mkInputContext input cfg.relConfigFile.toString
   match (← loadToml ictx |>.toBaseIO) with
   | .ok table =>
     let (pkg, errs) := Id.run <| StateT.run (s := (#[] : Array DecodeError)) do
@@ -319,7 +318,11 @@ def loadTomlConfig (dir relDir relConfigFile : FilePath) : LogIO Package := do
       let defaultTargets := defaultTargets.map stringToLegalOrSimpleName
       let depConfigs ← table.tryDecodeD `require #[]
       return {
-        dir, relDir, relConfigFile
+        dir := cfg.pkgDir
+        relDir := cfg.relPkgDir
+        relConfigFile := cfg.relConfigFile
+        scope := cfg.scope
+        remoteUrl := cfg.remoteUrl
         config, depConfigs, leanLibConfigs, leanExeConfigs
         defaultTargets
       }
diff --git a/src/lake/Lake/Reservoir.lean b/src/lake/Lake/Reservoir.lean
index 5f9c026a551a..f2d72fb47093 100644
--- a/src/lake/Lake/Reservoir.lean
+++ b/src/lake/Lake/Reservoir.lean
@@ -121,19 +121,41 @@ def hexEncodeByte (b : UInt8) : Char :=
 def uriEscapeByte (b : UInt8) (s := "") : String :=
   s.push '%' |>.push (hexEncodeByte <| b >>> 4) |>.push (hexEncodeByte <| b &&& 0xF)
 
-@[specialize] def utf8EncodeCharM [Monad m] (c : Char) (f : σ → UInt8 → m σ) (init : σ) : m σ := do
+/-- Folds a monadic function over the UTF-8 bytes of `Char` from most significant to least significant. -/
+@[specialize] def foldlUtf8M [Monad m] (c : Char) (f : σ → UInt8 → m σ) (init : σ) : m σ := do
+  let s := init
   let v := c.val
-  let s ← f init <| v.toUInt8 &&& 0x3f ||| 0x80
-  if v ≤ 0x7f then return s
-  let s ← f s <| (v >>>  6).toUInt8 &&& 0x1f ||| 0xc0
-  if v ≤ 0x7ff then return s
-  let s ← f s <| (v >>> 12).toUInt8 &&& 0x0f ||| 0xe0
-  if v ≤ 0xffff then return s
-  f s <| (v >>> 18).toUInt8 &&& 0x07 ||| 0xf0
+  if v ≤ 0x7f then
+    f s v.toUInt8
+  else if v ≤ 0x7ff then
+    let s ← f s <| (v >>>  6).toUInt8 &&& 0x1f ||| 0xc0
+    let s ← f s <| v.toUInt8 &&& 0x3f ||| 0x80
+    return s
+  else if v ≤ 0xffff then
+    let s ← f s <| (v >>> 12).toUInt8 &&& 0x0f ||| 0xe0
+    let s ← f s <| (v >>>  6).toUInt8 &&& 0x3f ||| 0x80
+    let s ← f s <| v.toUInt8 &&& 0x3f ||| 0x80
+    return s
+  else
+    let s ← f s <| (v >>> 18).toUInt8 &&& 0x07 ||| 0xf0
+    let s ← f s <| (v >>> 12).toUInt8 &&& 0x3f ||| 0x80
+    let s ← f s <| (v >>>  6).toUInt8 &&& 0x3f ||| 0x80
+    let s ← f s <| v.toUInt8 &&& 0x3f ||| 0x80
+    return s
+
+abbrev foldlUtf8 (c : Char) (f : σ → UInt8 → σ) (init : σ) : σ :=
+  Id.run <| foldlUtf8M c f init
+
+example : foldlUtf8 c (fun l b => b::l) List.nil = (String.utf8EncodeChar c).reverse := by
+  simp only [foldlUtf8M, String.utf8EncodeChar, Id.run]
+  if h1 : c.val ≤ 0x7f then simp [h1]
+  else if h2 : c.val ≤ 0x7ff then simp [h1, h2]
+  else if h3 : c.val ≤ 0xffff then simp [h1, h2, h3]
+  else simp [h1, h2, h3]
 
 /-- Encode a character as a sequence of URI escape codes representing its UTF8 encoding. -/
 def uriEscapeChar (c : Char) (s := "") : String :=
-  Id.run <| utf8EncodeCharM c (init := s) fun s b => uriEscapeByte b s
+  foldlUtf8 c (init := s) fun s b => uriEscapeByte b s
 
 /-- A URI unreserved mark as specified in [RFC2396](https://datatracker.ietf.org/doc/html/rfc2396#section-2.3). -/
 def isUriUnreservedMark (c : Char)  : Bool :=
@@ -171,14 +193,19 @@ protected def ReservoirResp.fromJson? [FromJson α] (val : Json) : Except String
 
 instance [FromJson α] : FromJson (ReservoirResp α) := ⟨ReservoirResp.fromJson?⟩
 
-def fetchReservoirPkg? (lakeEnv : Lake.Env) (owner pkg : String) : LogIO (Option RegistryPkg) := do
-  let url := s!"{lakeEnv.reservoirApiUrl}/packages/{uriEncode owner}/{uriEncode pkg}"
+def Reservoir.pkgApiUrl (lakeEnv : Lake.Env) (owner pkg : String) :=
+   s!"{lakeEnv.reservoirApiUrl}/packages/{uriEncode owner}/{uriEncode pkg}"
+
+def Reservoir.lakeHeaders := #[
+  "X-Reservoir-Api-Version:1.0.0",
+  "X-Lake-Registry-Api-Version:0.1.0"
+]
+
+def Reservoir.fetchPkg? (lakeEnv : Lake.Env) (owner pkg : String) : LogIO (Option RegistryPkg) := do
+  let url := Reservoir.pkgApiUrl lakeEnv owner pkg
   let out ←
     try
-      getUrl url #[
-        "X-Reservoir-Api-Version:1.0.0",
-        "X-Lake-Registry-Api-Version:0.1.0"
-      ]
+      getUrl url Reservoir.lakeHeaders
     catch _ =>
       logError s!"{owner}/{pkg}: Reservoir lookup failed"
       return none
diff --git a/src/lake/tests/noRelease/test.sh b/src/lake/tests/noRelease/test.sh
index ccb5aa1bf866..26b361740b9d 100755
--- a/src/lake/tests/noRelease/test.sh
+++ b/src/lake/tests/noRelease/test.sh
@@ -35,7 +35,7 @@ REV_STR="'${INIT_REV}'"
 ✖ [1/2] (Optional) Fetching dep:optRelease
 error: no release tag found for revision ${REV_STR}
 ✖ [2/2] Running dep:release
-error: failed to fetch cloud release (see 'dep:optRelease' for details)
+error: failed to fetch GitHub release (see 'dep:optRelease' for details)
 Some required builds logged failures:
 - dep:release
 EOF
@@ -54,7 +54,7 @@ EOF
 
 # Test download failure
 $LAKE update # re-fetch release tag
-($LAKE build dep:release && exit 1 || true) | grep --color "downloading"
+($LAKE  build dep:release && exit 1 || true) | grep --color "curl"
 
 # Test automatic cloud release unpacking
 mkdir -p .lake/packages/dep/.lake/build
@@ -62,7 +62,7 @@ $LAKE -d .lake/packages/dep pack 2>&1 | grep --color "packing"
 test -f .lake/packages/dep/.lake/release.tgz
 echo 4225503363911572621 > .lake/packages/dep/.lake/release.tgz.trace
 rmdir .lake/packages/dep/.lake/build
-$LAKE build dep:release -v | grep --color "unpacking"
+$LAKE build dep:release -v | grep --color "tar"
 test -d .lake/packages/dep/.lake/build
 
 # Test that the job prints nothing if the archive is already fetched and unpacked
diff --git a/src/lake/tests/online/barrel.lean b/src/lake/tests/online/barrel.lean
new file mode 100644
index 000000000000..4afa5e9688b0
--- /dev/null
+++ b/src/lake/tests/online/barrel.lean
@@ -0,0 +1,7 @@
+import Lake
+open Lake DSL
+
+package test
+
+require "leanprover" / "Cli"
+  @ git "2cf1030dc2ae6b3632c84a09350b675ef3e347d0"
diff --git a/src/lake/tests/online/lakefile.lean b/src/lake/tests/online/require.lean
similarity index 100%
rename from src/lake/tests/online/lakefile.lean
rename to src/lake/tests/online/require.lean
diff --git a/src/lake/tests/online/lakefile.toml b/src/lake/tests/online/require.toml
similarity index 100%
rename from src/lake/tests/online/lakefile.toml
rename to src/lake/tests/online/require.toml
diff --git a/src/lake/tests/online/test.sh b/src/lake/tests/online/test.sh
index 96961eb49a35..b1b94f3a5b73 100755
--- a/src/lake/tests/online/test.sh
+++ b/src/lake/tests/online/test.sh
@@ -3,17 +3,36 @@ set -exo pipefail
 
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
+./clean.sh
+$LAKE -f barrel.lean update
+# Test cache toggle
+$LAKE -f barrel.lean build @Cli:extraDep | grep --color "Cli:optBarrel"
+(LAKE_NO_CACHE=1 $LAKE -f barrel.lean build @Cli:extraDep) |
+  grep --color "Cli:optBarrel" && exit 1 || true
+($LAKE -f barrel.lean build @Cli:extraDep --no-cache) |
+  grep --color "Cli:optBarrel" && exit 1 || true
+(LAKE_NO_CACHE=1 $LAKE -f barrel.lean build @Cli:extraDep --try-cache) |
+  grep --color "Cli:optBarrel"
+# Test barrel download
+(ELAN_TOOLCHAIN= $LAKE -f barrel.lean build @Cli:barrel -v && exit 1 || true) |
+  grep --color "Lean toolchain not known"
+ELAN_TOOLCHAIN=leanprover/lean4:v4.11.0 \
+  $LAKE -f barrel.lean build @Cli:barrel -v
+ELAN_TOOLCHAIN=leanprover/lean4:v4.11.0 \
+LEAN_GITHASH=ec3042d94bd11a42430f9e14d39e26b1f880f99b \
+  $LAKE -f barrel.lean build Cli --no-build
+
 ./clean.sh
 # Tests requiring a package not in the index
-($LAKE update -f bogus-dep.toml 2>&1 && exit || true) |
+($LAKE -f bogus-dep.toml update 2>&1 && exit 1 || true) |
   grep --color "error: bogus/bogus: could not materialize package: dependency has no explicit source and was not found on Reservoir"
 
 ./clean.sh
-$LAKE update -f lakefile.lean -v
+$LAKE -f require.lean update -v
 test -d .lake/packages/doc-gen4
-$LAKE resolve-deps -f lakefile.lean # validate manifest
+$LAKE -f require.lean resolve-deps  # validate manifest
 
 ./clean.sh
-$LAKE update -f lakefile.toml -v
+$LAKE -f require.toml update  v
 test -d .lake/packages/doc-gen4
-$LAKE resolve-deps -f lakefile.toml # validate manifest
+$LAKE -f require.toml resolve-deps  # validate manifest