Revert "feat: lake: Reservoir build cache (#5486)"

This reverts commit ffb4c5becf.

RELEASES.md

@@ -8,6 +8,11 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
+v4.13.0
+----------
+
+Release notes to be written.
+
 v4.12.0
 ----------
 

src/CMakeLists.txt

@@ -10,9 +10,9 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 12)
+set(LEAN_VERSION_MINOR 13)
 set(LEAN_VERSION_PATCH 0)
-set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)

src/Lean/Server/FileWorker/SetupFile.lean

@@ -28,7 +28,7 @@ partial def runLakeSetupFile
     : IO LakeSetupFileOutput := do
   let mut args := #["setup-file", filePath.toString] ++ imports.map (toString ·.module)
   if m.dependencyBuildMode matches .never then
-    args := args.push "--no-build" |>.push "--no-cache"
+    args := args.push "--no-build"
   let spawnArgs : Process.SpawnArgs := {
     stdin  := Process.Stdio.null
     stdout := Process.Stdio.piped

src/lake/Lake/Build/Actions.lean

@@ -108,16 +108,15 @@ def compileExe
   }
 
 /-- Download a file using `curl`, clobbering any existing file. -/
-def download
-  (url : String) (file : FilePath) (headers : Array String := #[])
-: LogIO PUnit := do
+def download  (url : String) (file : FilePath) : LogIO PUnit := do
   if (← file.pathExists) then
     IO.FS.removeFile file
   else
     createParentDirs file
-  let args := #["-s", "-S", "-f", "-o", file.toString, "-L", url]
-  let args := headers.foldl (init := args) (· ++ #["-H", ·])
-  proc (quiet := true) {cmd := "curl", args}
+  proc (quiet := true) {
+    cmd := "curl"
+    args := #["-s", "-S", "-f", "-o", file.toString, "-L", url]
+  }
 
 /-- Unpack an archive `file` using `tar` into the directory `dir`. -/
 def untar (file : FilePath) (dir : FilePath) (gzip := true) : LogIO PUnit := do

src/lake/Lake/Build/Basic.lean

@@ -17,13 +17,10 @@ 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.

src/lake/Lake/Build/Facets.lean

@@ -117,53 +117,19 @@ module_data o.noexport : BuildJob FilePath
 /-! ## Package Facets -/
 
 /--
-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.
+A package's *optional* cloud build release.
+Will not cause the whole build to fail if the release cannot be fetched.
 -/
-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
+abbrev Package.optReleaseFacet := `optRelease
 package_data optRelease : BuildJob Bool
 
-@[deprecated (since := "2024-09-27")]
-abbrev Package.optReleaseFacet := optGitHubReleaseFacet
-
 /--
-A package's build archive from a GitHub release.
+A package's cloud build release.
 Will cause the whole build to fail if the release cannot be fetched.
 -/
-abbrev Package.gitHubReleaseFacet := `release
+abbrev Package.releaseFacet := `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

src/lake/Lake/Build/Info.lean

@@ -216,35 +216,13 @@ end Module
 abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
   .packageFacet self facet
 
-@[inherit_doc buildCacheFacet]
-abbrev Package.buildCache (self : Package) : BuildInfo :=
-  self.facet buildCacheFacet
+@[inherit_doc releaseFacet]
+abbrev Package.release (self : Package) : BuildInfo :=
+  self.facet releaseFacet
 
-@[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 optReleaseFacet]
+abbrev Package.optRelease (self : Package) : BuildInfo :=
+  self.facet optReleaseFacet
 
 @[inherit_doc extraDepFacet]
 abbrev Package.extraDep (self : Package) : BuildInfo :=

src/lake/Lake/Build/Package.lean

@@ -7,7 +7,6 @@ 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.
@@ -25,59 +24,14 @@ 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 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
-  let shouldFetch :=
-    (← getTryCache) &&
-    (self.preferReleaseBuild || -- GitHub release
-      !(self.scope.isEmpty -- no Reservoir
-        || (← getElanToolchain).isEmpty
-        || (← self.buildDir.pathExists)))
-  if shouldFetch then
-    self.optBuildCache.fetch
-  else
-    return pure true
-
-@[inline]
-private def Package.optFacetDetails (self : Package) (facet : Name) : JobM String := do
-  if (← getIsVerbose) then
-    return s!" (see '{self.name}:{facet}' for details)"
-  else
-    return " (run with '-v' for details)"
-
-/--
-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
+/-- 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
     unless success do
-      if self.preferReleaseBuild then
-        let details ← self.optFacetDetails optGitHubReleaseFacet
-        logWarning s!"building from source; failed to fetch GitHub release{details}"
-      else
-        let details ← self.optFacetDetails optReservoirBarrelFacet
-        logVerbose s!"building from source; failed to fetch Reservoir build{details}"
+      logWarning s!"building from source; \
+        failed to fetch cloud release (see '{self.name}:optRelease' 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.
@@ -88,9 +42,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 build cache if this package is a dependency
-  if self.name ≠ (← getWorkspace).root.name then
-    job := job.add <| ← self.maybeFetchBuildCacheWithWarning
+  -- 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
   -- Build this package's extra dep targets
   for target in self.extraDepTargets do
     job := job.mix <| ← self.fetchTargetJob target
@@ -100,126 +54,60 @@ def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
 def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
   mkFacetJobConfig Package.recBuildExtraDepTargets
 
-/-- 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
+/-- 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
   let repo := GitRepo.mk self.dir
   let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
   let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
-    | error "release repository URL not known; \
+    | logError s!"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 ""
-      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
+      logError s!"no release tag found for revision{rev}"
+      updateAction .fetch
+      return (false, .nil)
+  let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
   let depTrace := Hash.ofString url
-  let traceFile := archiveFile.addExtension "trace"
-  let upToDate ← buildUnlessUpToDate? (action := .fetch) archiveFile depTrace traceFile do
-    download url archiveFile headers
+  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
   unless upToDate && (← self.buildDir.pathExists) do
     updateAction .fetch
-    untar archiveFile self.buildDir
+    logVerbose s!"unpacking {self.name}:{tag}:{self.buildArchive}"
+    untar self.buildArchiveFile self.buildDir
+  return (true, .nil)
 
-@[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 `optReleaseFacet`. -/
+def Package.optReleaseFacetConfig : PackageFacetConfig optReleaseFacet :=
+  mkFacetJobConfig (·.fetchOptReleaseCore)
 
-@[inline]
-private def Package.mkBuildArchiveFacetConfig
-  {facet : Name} (optFacet : Name) (what : String)
-  [FamilyDef PackageData facet (BuildJob Unit)]
-  [FamilyDef PackageData optFacet (BuildJob Bool)]
-: PackageFacetConfig facet :=
+/-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/
+def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
   mkFacetJobConfig fun pkg =>
-    withRegisterJob s!"{pkg.name}:{facet}" do
-      (← fetch <| pkg.facet optFacet).bindSync fun success t => do
+    withRegisterJob s!"{pkg.name}:release" do
+      (← pkg.optRelease.fetch).bindSync fun success t => do
         unless success do
-          error s!"failed to fetch {what}{← pkg.optFacetDetails optFacet}"
+          error s!"failed to fetch cloud release (see '{pkg.name}:optRelease' for details)"
         return ((), t)
 
-/-- 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 build"
-
-/-- 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
+/-- 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
   else
     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
+/-- 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
   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
@@ -229,9 +117,5 @@ def initPackageFacetConfigs : DNameMap PackageFacetConfig :=
   DNameMap.empty
   |>.insert depsFacet depsFacetConfig
   |>.insert extraDepFacet extraDepFacetConfig
-  |>.insert optBuildCacheFacet optBuildCacheFacetConfig
-  |>.insert buildCacheFacet buildCacheFacetConfig
-  |>.insert optReservoirBarrelFacet optBarrelFacetConfig
-  |>.insert reservoirBarrelFacet barrelFacetConfig
-  |>.insert optGitHubReleaseFacet optGitHubReleaseFacetConfig
-  |>.insert gitHubReleaseFacet gitHubReleaseFacetConfig
+  |>.insert optReleaseFacet optReleaseFacetConfig
+  |>.insert releaseFacet releaseFacetConfig

src/lake/Lake/Build/Run.lean

@@ -36,7 +36,6 @@ structure MonitorContext where
   outLv : LogLevel
   failLv : LogLevel
   minAction : JobAction
-  showOptional : Bool
   useAnsi : Bool
   showProgress : Bool
   /-- How often to poll jobs (in milliseconds). -/
@@ -99,7 +98,7 @@ def renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfinished.si
 
 def reportJob (job : OpaqueJob) : MonitorM PUnit := do
   let {jobNo, ..} ← get
-  let {totalJobs, failLv, outLv, showOptional, out, useAnsi, showProgress, minAction, ..} ← read
+  let {totalJobs, failLv, outLv, out, useAnsi, showProgress, minAction, ..} ← read
   let {task, caption, optional} := job.toJob
   let {log, action, ..} := task.get.state
   let maxLv := log.maxLv
@@ -107,10 +106,7 @@ def reportJob (job : OpaqueJob) : MonitorM PUnit := do
   if failed ∧ ¬optional then
     modify fun s => {s with failures := s.failures.push caption}
   let hasOutput := failed ∨ (log.hasEntries ∧ maxLv ≥ outLv)
-  let showJob :=
-    (¬ optional ∨ showOptional) ∧
-    (hasOutput ∨ (showProgress ∧ ¬ useAnsi ∧ action ≥ minAction))
-  if showJob then
+  if hasOutput ∨ (showProgress ∧ ¬ useAnsi ∧ action ≥ minAction) then
     let verb := action.verb failed
     let icon := if hasOutput then maxLv.icon else '✔'
     let opt := if optional then " (Optional)" else ""
@@ -171,14 +167,14 @@ def monitorJobs
   (out : IO.FS.Stream)
   (failLv outLv : LogLevel)
   (minAction : JobAction)
-  (showOptional useAnsi showProgress : Bool)
+  (useAnsi showProgress : Bool)
   (resetCtrl : String := "")
   (initFailures : Array String := #[])
   (totalJobs := jobs.size)
   (updateFrequency := 100)
 : BaseIO (Array String) := do
   let ctx := {
-    totalJobs, out, failLv, outLv, minAction, showOptional
+    totalJobs, out, failLv, outLv, minAction
     useAnsi, showProgress, updateFrequency
   }
   let s := {
@@ -232,8 +228,7 @@ def Workspace.runFetchM
   let jobs ← ctx.registeredJobs.get
   let resetCtrl := if showAnsiProgress then Ansi.resetLine else ""
   let minAction := if cfg.verbosity = .verbose then .unknown else .fetch
-  let showOptional := cfg.verbosity = .verbose
-  let failures ← monitorJobs jobs out failLv outLv minAction showOptional useAnsi showProgress
+  let failures ← monitorJobs jobs out failLv outLv minAction useAnsi showProgress
     (resetCtrl := resetCtrl) (initFailures := failures)
   -- Failure Report
   if failures.isEmpty then

src/lake/Lake/CLI/Help.lean

@@ -48,8 +48,6 @@ 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

src/lake/Lake/CLI/Main.lean

@@ -40,7 +40,6 @@ 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
@@ -67,7 +66,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?
-    opts.noCache |>.adaptExcept fun msg => .invalidEnv msg
+    |>.adaptExcept fun msg => .invalidEnv msg
 
 /-- Make a `LoadConfig` from a `LakeOptions`. -/
 def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
@@ -174,8 +173,6 @@ 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})

src/lake/Lake/Config/Env.lean

@@ -31,11 +31,6 @@ 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`). -/
@@ -50,20 +45,13 @@ structure Env where
 
 namespace Env
 
-/--
-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
+/-- 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
   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",
@@ -72,10 +60,6 @@ def compute
     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

src/lake/Lake/Config/Monad.lean

@@ -128,14 +128,6 @@ 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 whether the `LAKE_NO_CACHE`/`--no-cache` Lake configuration is **NOT** set. -/
-@[inline] def getTryCache [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

src/lake/Lake/Config/Package.lean

@@ -283,7 +283,7 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   the Git revisions corresponding to released versions.
 
   Defaults to tags that are "version-like".
-  That is, start with a `v` followed by a digit.
+  That is, start with a `v` and are followed by a digit.
   -/
   versionTags : StrPat := defaultVersionTags
 
@@ -299,7 +299,7 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   `devtool`), specific subtopics (e.g., `topology`,  `cryptology`), and
   significant implementation details (e.g., `dsl`, `ffi`, `cli`).
   For instance, Lake's keywords could be `devtool`, `cli`, `dsl`,
-  `package-manager`, and `build-system`.
+  `package-manager`, `build-system`.
   -/
   keywords : Array String := #[]
 
@@ -308,7 +308,7 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
 
   Reservoir will already include a link to the package's GitHub repository
   (if the package is sourced from there). Thus, users are advised to specify
-  something else for this (if anything).
+  something else for this link (if anything).
   -/
   homepage : String := ""
 
@@ -340,11 +340,8 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
 
   /--
   The path to the package's README.
-
-  A README should be a Markdown file containing an overview of the package.
-  Reservoir displays the rendered HTML of this file on a package's page.
-  A nonstandard location can be used to provide a different README for Reservoir
-  and GitHub.
+  A README should be a markdown file containing an overview of the package.
+  Reservoir displays the rendered HTML of this README on a package's page.
 
   Defaults to `README.md`.
   -/
@@ -379,10 +376,8 @@ 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 : String := ""
+  remoteUrl? : Option String := none
   /-- (Opaque references to) the package's direct dependencies. -/
   opaqueDeps : Array OpaquePackage := #[]
   /-- Dependency configurations for the package. -/
@@ -560,10 +555,6 @@ 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
@@ -572,10 +563,6 @@ 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

src/lake/Lake/Load/Config.lean

@@ -28,10 +28,8 @@ 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 : String := ""
+  remoteUrl? : Option String := none
 
 /-- The full path to loaded package's directory. -/
 @[inline] def LoadConfig.pkgDir (cfg : LoadConfig) : FilePath :=

src/lake/Lake/Load/Lean.lean

@@ -29,7 +29,6 @@ def loadLeanConfig (cfg : LoadConfig)
     relDir := cfg.relPkgDir
     config := pkgConfig
     relConfigFile := cfg.relConfigFile
-    scope := cfg.scope
-    remoteUrl := cfg.remoteUrl
+    remoteUrl? := cfg.remoteUrl?
   }
   return (← pkg.loadFromEnv configEnv cfg.leanOpts, configEnv)

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 : String
+  remoteUrl? : Option String
   /-- The manifest entry for the dependency. -/
   manifestEntry : PackageEntry
   deriving Inhabited
@@ -87,9 +87,6 @@ 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?
@@ -112,13 +109,13 @@ def Dependency.materialize
       let relPkgDir := relParentDir / dir
       return {
         relPkgDir
-        remoteUrl := ""
+        remoteUrl? := none
         manifestEntry := mkEntry <| .path relPkgDir
       }
     | .git url inputRev? subDir? => do
       let sname := dep.name.toString (escape := false)
-      let repoUrl := Git.filterUrl? url |>.getD ""
-      materializeGit sname (relPkgsDir / sname) url repoUrl inputRev? subDir?
+      let repoUrl? := Git.filterUrl? url
+      materializeGit sname (relPkgsDir / sname) url repoUrl? inputRev? subDir?
   else
     if dep.scope.isEmpty then
       error s!"{dep.name}: ill-formed dependency: \
@@ -129,26 +126,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 ← Reservoir.fetchPkg? lakeEnv dep.scope depName
+    let some pkg ← fetchReservoirPkg? 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?.getD "") (verRev? <|> defaultBranch?) subDir?
+      materializeGit pkg.fullName relPkgDir url githubUrl? (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
+      relPkgDir
+      remoteUrl? := remoteUrl?
       manifestEntry := mkEntry <| .git gitUrl rev inputRev? subDir?
     }
 
@@ -163,7 +160,7 @@ def PackageEntry.materialize
   | .path (dir := relPkgDir) .. =>
     return {
       relPkgDir
-      remoteUrl := ""
+      remoteUrl? := none
       manifestEntry
     }
   | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do
@@ -190,6 +187,6 @@ def PackageEntry.materialize
     let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
     return {
       relPkgDir
-      remoteUrl := Git.filterUrl? url |>.getD ""
+      remoteUrl? := Git.filterUrl? url
       manifestEntry
     }

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
+    | "toml" => ((·,none)) <$> loadTomlConfig cfg.pkgDir cfg.relPkgDir cfg.relConfigFile
     | _ => 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 with relConfigFile := relTomlFile}
+        ((·,none)) <$> loadTomlConfig cfg.pkgDir cfg.relPkgDir relTomlFile
       else
         error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}"
 

src/lake/Lake/Load/Resolve.lean

@@ -34,8 +34,7 @@ def loadDepPackage
     relPkgDir := dep.relPkgDir
     relConfigFile := dep.configFile
     lakeOpts, leanOpts, reconfigure
-    scope := dep.scope
-    remoteUrl := dep.remoteUrl
+    remoteUrl? := dep.remoteUrl?
   }
   if let some env := env? then
     let ws ← IO.ofExcept <| ws.addFacetsFromEnv env leanOpts

src/lake/Lake/Load/Toml.lean

@@ -305,9 +305,10 @@ 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 (cfg: LoadConfig) : LogIO Package := do
-  let input ← IO.FS.readFile cfg.configFile
-  let ictx := mkInputContext input cfg.relConfigFile.toString
+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
   match (← loadToml ictx |>.toBaseIO) with
   | .ok table =>
     let (pkg, errs) := Id.run <| StateT.run (s := (#[] : Array DecodeError)) do
@@ -318,11 +319,7 @@ def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do
       let defaultTargets := defaultTargets.map stringToLegalOrSimpleName
       let depConfigs ← table.tryDecodeD `require #[]
       return {
-        dir := cfg.pkgDir
-        relDir := cfg.relPkgDir
-        relConfigFile := cfg.relConfigFile
-        scope := cfg.scope
-        remoteUrl := cfg.remoteUrl
+        dir, relDir, relConfigFile
         config, depConfigs, leanLibConfigs, leanExeConfigs
         defaultTargets
       }

src/lake/Lake/Reservoir.lean

@@ -121,41 +121,19 @@ def hexEncodeByte (b : UInt8) : Char :=
 def uriEscapeByte (b : UInt8) (s := "") : String :=
   s.push '%' |>.push (hexEncodeByte <| b >>> 4) |>.push (hexEncodeByte <| b &&& 0xF)
 
-/-- 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
+@[specialize] def utf8EncodeCharM [Monad m] (c : Char) (f : σ → UInt8 → m σ) (init : σ) : m σ := do
   let v := c.val
-  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]
+  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
 
 /-- Encode a character as a sequence of URI escape codes representing its UTF8 encoding. -/
 def uriEscapeChar (c : Char) (s := "") : String :=
-  foldlUtf8 c (init := s) fun s b => uriEscapeByte b s
+  Id.run <| utf8EncodeCharM 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 :=
@@ -193,19 +171,14 @@ protected def ReservoirResp.fromJson? [FromJson α] (val : Json) : Except String
 
 instance [FromJson α] : FromJson (ReservoirResp α) := ⟨ReservoirResp.fromJson?⟩
 
-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
+def fetchReservoirPkg? (lakeEnv : Lake.Env) (owner pkg : String) : LogIO (Option RegistryPkg) := do
+  let url := s!"{lakeEnv.reservoirApiUrl}/packages/{uriEncode owner}/{uriEncode pkg}"
   let out ←
     try
-      getUrl url Reservoir.lakeHeaders
+      getUrl url #[
+        "X-Reservoir-Api-Version:1.0.0",
+        "X-Lake-Registry-Api-Version:0.1.0"
+      ]
     catch _ =>
       logError s!"{owner}/{pkg}: Reservoir lookup failed"
       return none

src/lake/README.md

@@ -13,7 +13,6 @@ A Lake configuration file defines the package's basic configuration. It also typ
 * [Creating and Building a Package](#creating-and-building-a-package)
 * [Glossary of Terms](#glossary-of-terms)
 * [Package Configuration Options](#package-configuration-options)
-  + [Metadata](#metadata)
   + [Layout](#layout)
   + [Build & Run](#build--run)
   + [Test & Lint](#test--lint)
@@ -164,22 +163,6 @@ Lake uses a lot of terms common in software development -- like workspace, packa
 
 Lake provides a large assortment of configuration options for packages.
 
-### Metadata
-
-These options describe the package. They are used by Lake's package registry, [Reservoir](https://reservoir.lean-lang.org/), to index and display packages. If a field is left out, Reservoir may use information from the package's GitHub repository to fill in details.
-
-* `name`: The name of the package. Set by `package <name>` in Lean configuration files.
-* `version`: The version of the package. A 3-point version identifier with an optional `-` suffix.
-* `versionTags`: Git tags of this package's repository that should be treated as versions.  Reservoir makes use of this information to determine the Git revisions corresponding to released versions. Defaults to tags that are "version-like". That is, start with a `v` followed by a digit.
-* `description`: A short description for the package.
-* `keywords`: An `Array` of custom keywords that identify key aspects of the package. Reservoir can make use of these to group packages and make it easier for potential users to discover them.  For example, Lake's keywords could be `devtool`, `cli`, `dsl`,  `package-manager`, and `build-system`.
-* `homepage`: A URL to information about the package. Reservoir will already include a link to the package's GitHub repository. Thus, users are advised to specify something else for this.
-* `license`: An [SPFX license identifier](https://spdx.org/licenses/) for the package's license. For example, `Apache-2.0` or `MIT`.
-* `licenseFiles`: An `Array` of  files that contain license information. For example, `#["LICENSE", "NOTICE"]` for Apache 2.0. Defaults to `#["LICENSE"]`,
-* `readmeFile`: The relative path to the package's README. It should be a Markdown file containing an overview of the package. A nonstandard location can be used to provide a different README for Reservoir and GitHub. Defaults to `README.md`.
-* `reservoir`:  Whether Reservoir should index the package. Defaults to `true`. Set this to `false` to have Reservoir exclude the package from its index.
-
-
 ### Layout
 
 These options control the top-level directory layout of the package and its build directory. Further paths specified by libraries, executables, and targets within the package are relative to these directories.

src/lake/tests/noRelease/test.sh

@@ -30,9 +30,12 @@ $LAKE update
 git -C .lake/packages/dep tag -d release
 
 # Test that a direct invocation fo `lake build *:release` fails
+REV_STR="'${INIT_REV}'"
 ($LAKE build dep:release && exit 1 || true) | diff -u --strip-trailing-cr <(cat << EOF
+✖ [1/2] (Optional) Fetching dep:optRelease
+error: no release tag found for revision ${REV_STR}
 ✖ [2/2] Running dep:release
-error: failed to fetch GitHub release (run with '-v' for details)
+error: failed to fetch cloud release (see 'dep:optRelease' for details)
 Some required builds logged failures:
 - dep:release
 EOF
@@ -40,8 +43,10 @@ EOF
 
 # Test that an indirect fetch on the release does not cause the build to fail
 $LAKE build Test | diff -u --strip-trailing-cr <(cat << EOF
+✖ [1/5] (Optional) Fetching dep:optRelease
+error: no release tag found for revision ${REV_STR}
 ⚠ [2/5] Ran dep:extraDep
-warning: building from source; failed to fetch GitHub release (run with '-v' for details)
+warning: building from source; failed to fetch cloud release (see 'dep:optRelease' for details)
 ✔ [4/5] Built Test
 Build completed successfully.
 EOF
@@ -49,7 +54,7 @@ EOF
 
 # Test download failure
 $LAKE update # re-fetch release tag
-($LAKE -v build dep:release && exit 1 || true) | grep --color "curl"
+($LAKE build dep:release && exit 1 || true) | grep --color "downloading"
 
 # Test automatic cloud release unpacking
 mkdir -p .lake/packages/dep/.lake/build
@@ -57,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 "tar"
+$LAKE build dep:release -v | grep --color "unpacking"
 test -d .lake/packages/dep/.lake/build
 
 # Test that the job prints nothing if the archive is already fetched and unpacked

src/lake/tests/online/barrel.lean

@@ -1,7 +0,0 @@
-import Lake
-open Lake DSL
-
-package test
-
-require "leanprover" / "Cli"
-  @ git "2cf1030dc2ae6b3632c84a09350b675ef3e347d0"

src/lake/tests/online/git.toml

@@ -1,6 +0,0 @@
-name = "test"
-
-[[require]]
-name = "Cli"
-git = "https://github.com/leanprover/lean4-cli"
-rev = "main"

src/lake/tests/online/test.sh

@@ -3,58 +3,17 @@ set -exo pipefail
 
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
-export ELAN_TOOLCHAIN=test
-
 ./clean.sh
 # Tests requiring a package not in the index
-($LAKE -f bogus-dep.toml update 2>&1 && exit 1 || true) |
+($LAKE update -f bogus-dep.toml 2>&1 && exit || true) |
   grep --color "error: bogus/bogus: could not materialize package: dependency has no explicit source and was not found on Reservoir"
 
 ./clean.sh
-$LAKE -f git.toml update
-# Test that barrels are not fetched for non-Reservoir dependencies
-$LAKE -v -f git.toml build @Cli:extraDep |
-  grep --color "Cli:optBarrel" && exit 1 || true
-
-./clean.sh
-$LAKE -f barrel.lean update
-# Test that barrels are not fetched after the build directory is created.
-mkdir -p .lake/packages/Cli/.lake/build
-($LAKE -v -f barrel.lean build @Cli:extraDep) |
-  grep --color "Cli:optBarrel" && exit 1 || true
-rmdir .lake/packages/Cli/.lake/build
-# Test that barrels are not fetched without a toolchain
-(ELAN_TOOLCHAIN= $LAKE -v -f barrel.lean build @Cli:extraDep) |
-  grep --color "Cli:optBarrel" && exit 1 || true
-($LAKE -v -f barrel.lean build @Cli:barrel && exit 1 || true) |
-  grep --color "toolchain=test"
-# Test that fetch failures are only shown in verbose mode
-$LAKE -v -f barrel.lean build @Cli:extraDep |
-  grep --color "Cli:optBarrel"
-$LAKE -f barrel.lean build @Cli:extraDep |
-  grep --color "Cli:optBarrel" && exit 1 || true
-# Test cache toggle
-(LAKE_NO_CACHE=1 $LAKE -v -f barrel.lean build @Cli:extraDep) |
-  grep --color "Cli:optBarrel" && exit 1 || true
-($LAKE -v -f barrel.lean build @Cli:extraDep --no-cache) |
-  grep --color "Cli:optBarrel" && exit 1 || true
-(LAKE_NO_CACHE=1 $LAKE -v -f barrel.lean build @Cli:extraDep --try-cache) |
-  grep --color "Cli:optBarrel"
-# Test barrel download
-(ELAN_TOOLCHAIN= $LAKE -v -f barrel.lean build @Cli:barrel && exit 1 || true) |
-  grep --color "Lean toolchain not known"
-ELAN_TOOLCHAIN=leanprover/lean4:v4.11.0 \
-  $LAKE -v -f barrel.lean build @Cli:barrel
-ELAN_TOOLCHAIN=leanprover/lean4:v4.11.0 \
-LEAN_GITHASH=ec3042d94bd11a42430f9e14d39e26b1f880f99b \
-  $LAKE -f barrel.lean build Cli --no-build
-
-./clean.sh
-$LAKE -f require.lean update -v
+$LAKE update -f lakefile.lean -v
 test -d .lake/packages/doc-gen4
-$LAKE -f require.lean resolve-deps  # validate manifest
+$LAKE resolve-deps -f lakefile.lean # validate manifest
 
 ./clean.sh
-$LAKE -f require.toml update  v
+$LAKE update -f lakefile.toml -v
 test -d .lake/packages/doc-gen4
-$LAKE -f require.toml resolve-deps  # validate manifest
+$LAKE resolve-deps -f lakefile.toml # validate manifest