feat: lake cache (& remote cache support) (#10188)

This PR adds support for remote artifact caches (e.g., Reservoir) to
Lake. As part of this support, a new suite of `lake cache` CLI commands
has been introduced to help manage Lake's cache. Also, the existing
local cache support has been overhauled for better interplay with the
new remote support.

**Cache CLI**

Artifacts are uploaded to a remote cache via `lake cache put`. This
command takes a JSON Lines input-to-outputs file which describes the
output artifacts for a build (indexed by its input hash). This file can
be produced by a run of `lake build` with the new `-o` option. Lake will
write the input-to-outputs mappings of thee root package artifacts
traversed by the build to the file specified via `-o`. This file can
then be passed to `lake cache put` to upload both it and the built
artifacts from the local cache to the remote cache.

The remote cache service can be customized using the following
environment variables:

* `LAKE_CACHE_KEY`: This is the authorization key for the remote cache.
Lake uploads artifacts via `curl` using the AWS Signature Version 4
protocol, so this should be the S3 `<key>:<secret>` pair expected by
`curl`.

* `LAKE_CACHE_ARTIFACT_ENDPOINT`: This is the base URL to upload (or
download) artifacts to a given remote cache. Artifacts will be stored at
`<endpoint>/<scope/<content-hash>.art`.

* `LAKE_CACHE_REVISION_ENDPOINT`: This is the base URL to upload (or
download) input-to-output mappings to a given remote cache. Mappings are
indexed by the Git revision of the package, and are stored at
`<endpoint>/<scope/<rev>.jsonl`.

The `<scope>` is provided through the `--scope` option to `lake cache
put`. This option is used to prevent one package from overwriting the
artifacts/mappings of another. Lake artifact hashes and Git revisions
hashes are not cryptographically secure, so it is not safe for a service
to store untrusted files across packages in a single flat store.

Once artifacts are available in a remote cache, the `lake cache get`
command can be used to retrieve them. By default, it will fetch
artifacts for the root package's dependencies from Reservoir using its
API. But, like `cache put`, it can be configured to use a custom
endpoint with the above environment variables and an explicit `--scope`.
When so configured, `cache get` will instead download artifacts for the
root package. Lake only downloads artifacts for a single package in this
case, because it cannot deduce the necessary package scopes without
Reservoir.

**Significant local cache changes**

* Lake now always has a cache directory. If Lake cannot find a good
candidate directory on the system for the cache, it will instead store
the cache at `.lake/cache` within the workspace.

* If the local cache is disabled, Lake will not save built artifacts to
the cache. However, Lake will, nonetheless, always attempt to lookup
build artifacts in the cache. If found, the cached artifact will be
copied to the the build location ("restored").

* Input-to-outputs mappings in the local cache are no longer stored in a
single file for a package, but rather in individual files per input (in
the `outputs` subdirectory of the cache).

* Outputs in a trace file, outputs file, or mappings file are now an
`ArtifactDescr`, which is currently composed of both the content hash
and the file extension.

* Trace files now contain a date-based `schemaVersion` to help make
version to version migration easier. Hashes in JSON and in artifacts
names now use a 16-digit hexadecimal encoding (instead of a variable
decimal encoding).

* `buildArtifactUnlessUpToDate` now returns an `Artifact` instead of a
`FilePath`.

**NOTE:** The Lake local cache is still disabled by default. This means
that built artifacts, by default, will not be placed in the cache
directory, and thus will not be available for `lake cache put` to
upload. Users must first explicitly enable the cache by either setting
the `LAKE_ARTIFACT_CACHE` environment variable to a truthy value or by
setting the `enableArtifactCache` package configuration option to
`true`.

Author: tydeu

src/lake/Lake/Build/Common.lean

@@ -42,6 +42,8 @@ public structure BuildConfig where
   ansiMode : AnsiMode := .auto
   /-- Whether to print a message when the build finishes successfully (if not quiet). -/
   showSuccess : Bool := false
+  /-- File to save input-to-output mappings from the build of the worksoace's root -/
+  outputsFile? : Option FilePath := none
 
 /--
 Whether the build should show progress information.

src/lake/Lake/Build/Context.lean

@@ -511,6 +511,16 @@ public def Module.setupFacetConfig : ModuleFacetConfig setupFacet :=
 public def Module.depsFacetConfig : ModuleFacetConfig depsFacet :=
   mkFacetJobConfig fun mod => (·.toOpaque) <$> mod.setup.fetch
 
+/-- Remove all existing artifacts produced by the Lean build of the module. -/
+public def Module.clearOutputArtifacts (mod : Module) : IO PUnit := do
+  removeFileIfExists mod.oleanFile
+  removeFileIfExists mod.oleanServerFile
+  removeFileIfExists mod.oleanPrivateFile
+  removeFileIfExists mod.ileanFile
+  removeFileIfExists mod.irFile
+  removeFileIfExists mod.cFile
+  removeFileIfExists mod.bcFile
+
 /-- Remove any cached file hashes of the module build outputs (in `.hash` files). -/
 public def Module.clearOutputHashes (mod : Module) : IO PUnit := do
   clearFileHash mod.oleanFile
@@ -535,31 +545,34 @@ public def Module.cacheOutputHashes (mod : Module) : IO PUnit := do
   if Lean.Internal.hasLLVMBackend () then
     cacheFileHash mod.bcFile
 
-private def ModuleOutputHashes.getArtifactsFrom?
-  (cache : Cache) (hashes : ModuleOutputHashes)
+private def ModuleOutputDescrs.getArtifactsFrom?
+  (cache : Cache) (descrs : ModuleOutputDescrs)
 : BaseIO (Option ModuleOutputArtifacts) := OptionT.run do
   let mut arts : ModuleOutputArtifacts := {
-    olean := ← cache.getArtifact? hashes.olean "olean"
-    ilean := ← cache.getArtifact? hashes.ilean "ilean"
-    c :=← cache.getArtifact? hashes.c "c"
+    olean := ← cache.getArtifact? descrs.olean
+    ilean := ← cache.getArtifact? descrs.ilean
+    c :=← cache.getArtifact? descrs.c
   }
-  if let some hash := hashes.oleanServer? then
-    arts := {arts with oleanServer? := some (← cache.getArtifact? hash "olean.server")}
-  if let some hash := hashes.oleanPrivate? then
-    arts := {arts with oleanPrivate? := some (← cache.getArtifact? hash "olean.private")}
-  if let some hash := hashes.ir? then
-    arts := {arts with ir? := some (← cache.getArtifact? hash "ir")}
+  if let some hash := descrs.oleanServer? then
+    arts := {arts with oleanServer? := some (← cache.getArtifact? hash)}
+  if let some hash := descrs.oleanPrivate? then
+    arts := {arts with oleanPrivate? := some (← cache.getArtifact? hash)}
+  if let some hash := descrs.ir? then
+    arts := {arts with ir? := some (← cache.getArtifact? hash)}
   if Lean.Internal.hasLLVMBackend () then
-    arts := {arts with bc? := some (← cache.getArtifact? (← hashes.bc?) "bc")}
+    arts := {arts with bc? := some (← cache.getArtifact? (← descrs.bc?))}
   return arts
 
-@[inline] private def ModuleOutputHashes.getArtifacts?
-  [MonadLakeEnv m] [MonadLiftT BaseIO m] [Monad m] (hashes : ModuleOutputHashes)
-: m (Option ModuleOutputArtifacts) := do hashes.getArtifactsFrom? (← getLakeCache)
+@[inline] def resolveModuleOutputs?
+   [MonadWorkspace m] [MonadLiftT BaseIO m] [MonadError m] [Monad m]  (outputs : Json)
+: m (Option ModuleOutputArtifacts) := do
+  match fromJson? outputs with
+  | .ok (descrs : ModuleOutputDescrs) => descrs.getArtifactsFrom? (← getLakeCache)
+  | .error e => error e
 
-private instance
-  [MonadLakeEnv m] [MonadLiftT BaseIO m] [Monad m]
-: ResolveArtifacts m ModuleOutputHashes ModuleOutputArtifacts := ⟨ ModuleOutputHashes.getArtifacts?⟩
+instance
+  [MonadWorkspace m] [MonadLiftT BaseIO m] [MonadError m] [Monad m]
+: ResolveOutputs m ModuleOutputArtifacts := ⟨resolveModuleOutputs?⟩
 
 /-- Save module build artifacts to the local Lake cache. Requires the artifact cache to be enabled. -/
 private def Module.cacheOutputArtifacts (mod : Module) : JobM ModuleOutputArtifacts := do
@@ -578,22 +591,38 @@ where
   @[inline] cacheIfExists? art ext := do
     cacheIf? (← art.pathExists) art ext
 
+private def restoreModuleArtifact (file : FilePath) (art : Artifact) : JobM Artifact := do
+  unless (← file.pathExists) do
+    logVerbose s!"restored artifact from cache to: {file}"
+    createParentDirs file
+    copyFile art.path file
+    writeFileHash file art.hash
+  return art.useLocalFile file
+
 /--
 Some module build artifacts must be located in the build directory (e.g., ILeans).
 This copies the required artifacts from the local Lake cache to the build directory and
 updates the data structure with the new paths.
 -/
-private def Module.restoreArtifacts (mod : Module) (cached : ModuleOutputArtifacts) : JobM ModuleOutputArtifacts := do
+private def Module.restoreNeededArtifacts (mod : Module) (cached : ModuleOutputArtifacts) : JobM ModuleOutputArtifacts := do
+  return {cached with
+    ilean := ← restoreModuleArtifact mod.ileanFile cached.ilean
+  }
+
+private def Module.restoreAllArtifacts (mod : Module) (cached : ModuleOutputArtifacts) : JobM ModuleOutputArtifacts := do
   return {cached with
-    ilean := ← restore mod.ileanFile cached.ilean
+    olean := ← restoreModuleArtifact mod.oleanFile cached.olean
+    oleanServer? := ← restoreSome mod.oleanServerFile cached.oleanServer?
+    oleanPrivate? := ← restoreSome mod.oleanPrivateFile cached.oleanPrivate?
+    ilean := ← restoreModuleArtifact mod.ileanFile cached.ilean
+    ir? := ← restoreSome mod.oleanFile cached.ir?
+    c := ← restoreModuleArtifact mod.cFile cached.c
+    bc? := ← restoreSome mod.oleanFile cached.bc?
   }
 where
-  restore file art := do
-    unless (← file.pathExists) do
-      logVerbose s!"restored artifact from cache to: {file}"
-      copyFile art.path file
-      writeFileHash file art.hash
-    return art.useLocalFile file
+  @[inline] restoreSome file art? :=
+    art?.mapM (restoreModuleArtifact file)
+
 
 private def Module.mkArtifacts (mod : Module) (srcFile : FilePath) (isModule : Bool) : ModuleArtifacts where
   lean? := srcFile
@@ -605,31 +634,27 @@ private def Module.mkArtifacts (mod : Module) (srcFile : FilePath) (isModule : B
   c? := mod.cFile
   bc? := if Lean.Internal.hasLLVMBackend () then some mod.bcFile else none
 
-private def Module.computeOutputHashes (mod : Module) (isModule : Bool) : FetchM ModuleOutputHashes :=
+private def Module.computeArtifacts (mod : Module) (isModule : Bool) : FetchM ModuleOutputArtifacts :=
   return {
-    olean := ← computeFileHash mod.oleanFile
-    oleanServer? := ← if isModule then some <$> computeFileHash mod.oleanServerFile else pure none
-    oleanPrivate? := ← if isModule then some <$> computeFileHash mod.oleanPrivateFile else pure none
-    ilean := ← computeFileHash mod.ileanFile
-    ir? := ← if isModule then some <$> computeFileHash mod.irFile else pure none
-    c := ← computeFileHash mod.cFile
-    bc? := ← if Lean.Internal.hasLLVMBackend () then some <$> computeFileHash mod.bcFile else pure none
+    olean := ← compute mod.oleanFile "olean"
+    oleanServer? := ← computeIf isModule mod.oleanServerFile "olean.server"
+    oleanPrivate? := ← computeIf isModule mod.oleanPrivateFile "olean.private"
+    ilean := ← compute mod.ileanFile "ilean"
+    ir? := ← computeIf isModule mod.irFile "ir"
+    c := ← compute mod.cFile "c"
+    bc? := ← computeIf (Lean.Internal.hasLLVMBackend ()) mod.bcFile "bc"
   }
+where
+  @[inline] compute file ext := do
+    computeArtifact file ext
+  computeIf c file ext := do
+     if c then return some (← compute file ext) else return none
 
-private def Module.fetchLocalArtifacts (mod : Module) (isModule : Bool) : FetchM ModuleOutputArtifacts :=
-  return {
-    olean := ← fetchLocalArtifact mod.oleanFile
-    oleanServer? := ← if isModule then some <$> fetchLocalArtifact mod.oleanServerFile else pure none
-    oleanPrivate? := ← if isModule then some <$> fetchLocalArtifact mod.oleanPrivateFile else pure none
-    ilean := ← fetchLocalArtifact mod.ileanFile
-    ir? := ← if isModule then some <$> fetchLocalArtifact mod.irFile else pure none
-    c := ← fetchLocalArtifact mod.cFile
-    bc? := ← if Lean.Internal.hasLLVMBackend () then some <$> fetchLocalArtifact mod.bcFile else pure none
-  }
+instance : ToOutputJson ModuleOutputArtifacts := ⟨(toJson ·.descrs)⟩
 
 private def Module.buildLean
   (mod : Module) (depTrace : BuildTrace) (srcFile : FilePath) (setup : ModuleSetup)
-: JobM ModuleOutputHashes := buildAction depTrace mod.traceFile do
+: JobM ModuleOutputArtifacts := buildAction depTrace mod.traceFile do
   let args := mod.weakLeanArgs ++ mod.leanArgs
   let relSrcFile := relPathFrom mod.pkg.dir srcFile
   let directImports := (← (← mod.input.fetch).await).imports
@@ -639,7 +664,7 @@ private def Module.buildLean
   compileLeanModule srcFile relSrcFile setup mod.setupFile arts args
     (← getLeanPath) (← getLean)
   mod.clearOutputHashes
-  mod.computeOutputHashes setup.isModule
+  mod.computeArtifacts setup.isModule
 
 private def traceOptions (opts : LeanOptions) (caption := "opts") : BuildTrace :=
   opts.values.foldl (init := .nil caption) fun t n v =>
@@ -671,18 +696,38 @@ private def Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifac
     let depTrace ← getTrace
     let inputHash := depTrace.hash
     let savedTrace ← readTraceFile mod.traceFile
-    if let some ref := mod.pkg.cacheRef? then
-      if let some arts ← resolveArtifactsUsing? ModuleOutputHashes inputHash mod.traceFile savedTrace ref then
-        return ← mod.restoreArtifacts arts
-    let upToDate ← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace
-    unless upToDate do
-      discard <| mod.buildLean depTrace srcFile setup
-    if let some ref := mod.pkg.cacheRef? then
-      let arts ← mod.cacheOutputArtifacts
-      ref.insert inputHash arts.hashes
-      return arts
-    else
-      mod.fetchLocalArtifacts setup.isModule
+    let cache ← getLakeCache
+    let fetchArtsFromCache? restoreAll := do
+      let arts? ← getArtifacts? inputHash mod.traceFile savedTrace cache mod.pkg
+      if let some arts := arts? then
+        if savedTrace.isDifferentFrom inputHash then
+          mod.clearOutputArtifacts
+        if restoreAll then
+          some <$> mod.restoreAllArtifacts arts
+        else
+          some <$> mod.restoreNeededArtifacts arts
+      else
+        return none
+    let arts ← id do
+      if (← mod.pkg.isArtifactCacheEnabled) then
+        if let some arts ← fetchArtsFromCache? false then
+          return arts
+        else
+          unless (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) do
+            discard <| mod.buildLean depTrace srcFile setup
+          let arts ← mod.cacheOutputArtifacts
+          cache.writeOutputs mod.pkg.cacheScope inputHash arts.descrs
+          return arts
+      else
+        if (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) then
+          mod.computeArtifacts setup.isModule
+        else if let some arts ← fetchArtsFromCache? true then
+          return arts
+        else
+          mod.buildLean depTrace srcFile setup
+    if let some ref := mod.pkg.outputsRef? then
+      ref.insert inputHash arts.descrs
+    return arts
 
 /-- The `ModuleFacetConfig` for the builtin `leanArtsFacet`. -/
 public def Module.leanArtsFacetConfig : ModuleFacetConfig leanArtsFacet :=

src/lake/Lake/Build/Module.lean

@@ -14,42 +14,42 @@ open Lean (Json ToJson FromJson)
 
 namespace Lake
 
-/-- The content hashes of the output artifacts of a module build. -/
-public structure ModuleOutputHashes where
-  olean : Hash := .nil
-  oleanServer? : Option Hash := none
-  oleanPrivate? : Option Hash := none
-  ilean : Hash := .nil
-  ir? : Option Hash := none
-  c : Hash := .nil
-  bc? : Option Hash := none
+/-- The descriptions of the output artifacts of a module build. -/
+public structure ModuleOutputDescrs where
+  olean : ArtifactDescr
+  oleanServer? : Option ArtifactDescr := none
+  oleanPrivate? : Option ArtifactDescr := none
+  ilean : ArtifactDescr
+  ir? : Option ArtifactDescr := none
+  c : ArtifactDescr
+  bc? : Option ArtifactDescr := none
 
-public def ModuleOutputHashes.oleanHashes (hashes : ModuleOutputHashes) : Array Hash := Id.run do
-  let mut oleanHashes := #[hashes.olean]
-  if let some hash := hashes.oleanServer? then
-    oleanHashes := oleanHashes.push hash
-  if let some hash := hashes.oleanPrivate? then
-    oleanHashes := oleanHashes.push hash
-  return oleanHashes
+public def ModuleOutputDescrs.oleanParts (self : ModuleOutputDescrs) : Array ArtifactDescr := Id.run do
+  let mut descrs := #[self.olean]
+  if let some hash := self.oleanServer? then
+    descrs := descrs.push hash
+  if let some hash := self.oleanPrivate? then
+    descrs := descrs.push hash
+  return descrs
 
-public protected def ModuleOutputHashes.toJson (hashes : ModuleOutputHashes) : Json := Id.run do
+public protected def ModuleOutputDescrs.toJson (self : ModuleOutputDescrs) : Json := Id.run do
   let mut obj : JsonObject := {}
-  obj := obj.insert "o" hashes.oleanHashes
-  obj := obj.insert "i" hashes.ilean
-  if let some ir := hashes.ir? then
+  obj := obj.insert "o" self.oleanParts
+  obj := obj.insert "i" self.ilean
+  if let some ir := self.ir? then
     obj := obj.insert "r" ir
-  obj := obj.insert "c" hashes.c
-  if let some bc := hashes.bc? then
+  obj := obj.insert "c" self.c
+  if let some bc := self.bc? then
     obj := obj.insert "b" bc
   return obj
 
-public instance : ToJson ModuleOutputHashes := ⟨ModuleOutputHashes.toJson⟩
+public instance : ToJson ModuleOutputDescrs := ⟨ModuleOutputDescrs.toJson⟩
 
-public protected def ModuleOutputHashes.fromJson? (val : Json) : Except String ModuleOutputHashes := do
+public protected def ModuleOutputDescrs.fromJson? (val : Json) : Except String ModuleOutputDescrs := do
   let obj ← JsonObject.fromJson? val
-  let oleanHashes : Array Hash ← obj.get "o"
+  let oleanHashes : Array ArtifactDescr ← obj.get "o"
   let some olean := oleanHashes[0]?
-    | throw "expected a least one 'o' (OLean) hash"
+    | throw "expected a least one 'o' (.olean) hash"
   return {
     olean := olean
     oleanServer? := oleanHashes[1]?
@@ -60,7 +60,7 @@ public protected def ModuleOutputHashes.fromJson? (val : Json) : Except String M
     bc? := ← obj.get? "b"
   }
 
-public instance : FromJson ModuleOutputHashes := ⟨ModuleOutputHashes.fromJson?⟩
+public instance : FromJson ModuleOutputDescrs := ⟨ModuleOutputDescrs.fromJson?⟩
 
 /-- The output artifacts of a module build. -/
 public structure ModuleOutputArtifacts where
@@ -73,11 +73,11 @@ public structure ModuleOutputArtifacts where
   bc? : Option Artifact := none
 
 /-- Content hashes of the artifacts. -/
-public def ModuleOutputArtifacts.hashes (arts : ModuleOutputArtifacts) : ModuleOutputHashes where
-  olean := arts.olean.hash
-  oleanServer? := arts.oleanServer?.map (·.hash)
-  oleanPrivate? := arts.oleanPrivate?.map (·.hash)
-  ilean := arts.ilean.hash
-  ir? := arts.ir?.map (·.hash)
-  c := arts.c.hash
-  bc? := arts.bc?.map (·.hash)
+public def ModuleOutputArtifacts.descrs (arts : ModuleOutputArtifacts) : ModuleOutputDescrs where
+  olean := arts.olean.descr
+  oleanServer? := arts.oleanServer?.map (·.descr)
+  oleanPrivate? := arts.oleanPrivate?.map (·.descr)
+  ilean := arts.ilean.descr
+  ir? := arts.ir?.map (·.descr)
+  c := arts.c.descr
+  bc? := arts.bc?.map (·.descr)

src/lake/Lake/Build/ModuleArtifacts.lean

@@ -11,6 +11,7 @@ public import Lake.Config.FacetConfig
 public import Lake.Build.Job.Monad
 public import Lake.Build.Infos
 import Lake.Util.Git
+import Lake.Util.Url
 import Lake.Util.Proc
 import Lake.Build.Actions
 import Lake.Build.Common

src/lake/Lake/Build/Package.lean

@@ -222,14 +222,6 @@ public def monitorJobs
     didBuild := s.didBuild
   }
 
-/-- Save input mappings to the local Lake artifact cache (if enabled). -/
-public def Workspace.saveInputs (ws : Workspace) : LogIO Unit := do
-  unless ws.lakeCache.isDisabled do
-    ws.packages.forM fun pkg => do
-      if let some ref := pkg.cacheRef? then
-        let inputsFile := pkg.inputsFileIn ws.lakeCache
-        (← ref.get).save inputsFile
-
 /-- Exit code to return if `--no-build` is set and a build is required. -/
 public def noBuildCode : ExitCode := 3
 
@@ -260,16 +252,25 @@ public def Workspace.runFetchM
   let showTime := isVerbose || !useAnsi
   let {failures, numJobs, didBuild} ← monitorJobs #[job] ctx.registeredJobs
     out failLv outLv minAction showOptional useAnsi showProgress showTime
-  -- Save input mappings to cache
-  match (← ws.saveInputs.run {}) with
-  | .ok _ log =>
-    if !log.isEmpty && isVerbose then
-      print! out "There were issues saving input mappings to the local artifact cache:\n"
-      log.replay (logger := .stream out outLv useAnsi)
-  | .error _ log =>
-    print! out "Failed to save input mappings to the local artifact cache.\n"
-    if isVerbose then
-      log.replay (logger := .stream out outLv useAnsi)
+  -- Save input-to-output mappings
+  if let some outputsFile := cfg.outputsFile? then
+    let logger := .stream out outLv useAnsi
+    unless ws.isRootArtifactCacheEnabled do
+      logger.logEntry <| .warning s!"{ws.root.name}: \
+        the artifact cache is not enabled for this package, so the artifacts described \
+        by the mappings produced by `-o` will not necessarily be available in the cache."
+    if let some ref := ws.root.outputsRef? then
+      match (← (← ref.get).writeFile outputsFile {}) with
+      | .ok _ log =>
+        if !log.isEmpty && isVerbose then
+          print! out "There were issues saving input-to-output mappings from the build:\n"
+          log.replay (logger := logger)
+      | .error _ log =>
+        print! out "Failed to save input-to-output mappings from the build.\n"
+        if isVerbose then
+          log.replay (logger := logger)
+    else
+      print! out "Workspace missing input-to-output mappings from build. (This is likely a bug in Lake.)\n"
   -- Report
   let isNoBuild := cfg.noBuild
   if failures.isEmpty then