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

This reverts commit b1b73a4.

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

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.

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

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 :=

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

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