feat: lake: cached compressed module artifacts (#12914)

This PR adds packing and unpacking of module artifacts into `.ltar`
archives using `leantar`.

src/lake/Lake/Build/Common.lean

@@ -499,43 +499,71 @@ public def cacheArtifact
 /-- **For internal use only.** -/
 public class ResolveOutputs (α : Type) where
   /-- **For internal use only.** -/
-  resolveOutputs (out : Json)
-    (service? : Option CacheServiceName) (scope? : Option CacheServiceScope) : JobM α
+  resolveOutputs (out : CacheOutput) : JobM α
+
 
 open ResolveOutputs in
 /--
-Retrieve artifacts from the Lake cache using the outputs stored
-in either the saved trace file or in the cached input-to-content mapping.
+Retrieve artifacts from the Lake cache using only the outputs
+stored in the cached input-to-content mapping.
 
 **For internal use only.**
 -/
-@[specialize] public nonrec def getArtifacts?
-  [ResolveOutputs α] (inputHash : Hash) (savedTrace : SavedTrace) (pkg : Package)
+@[specialize] private def getArtifactsUsingCache?
+  [ResolveOutputs α] (inputHash : Hash) (pkg : Package)
 : JobM (Option α) := do
-  let cache ← getLakeCache
-  let updateCache ← pkg.isArtifactCacheWritable
-  if let some out ← cache.readOutputs? pkg.cacheScope inputHash then
+  if let some out ← (← getLakeCache).readOutputs? pkg.cacheScope inputHash then
     try
-      return some (← resolveOutputs out.data out.service? out.scope?)
+      return some (← resolveOutputs out)
     catch e =>
       let log ← takeLogFrom e
       let msg := s!"input '{inputHash.toString.take 7}' found in package artifact cache, \
         but some output(s) have issues:"
       let msg := log.entries.foldl (s!"{·}\n- {·.message}") msg
       logWarning msg
+      return none
+  else
+    return none
+
+open ResolveOutputs in
+/--
+Retrieve artifacts from the Lake cache using only the outputs stored in the saved trace file.
+
+**For internal use only.**
+-/
+@[specialize] public def getArtifactsUsingTrace?
+  [ResolveOutputs α] (inputHash : Hash) (savedTrace : SavedTrace) (pkg : Package)
+: JobM (Option α) := do
   if let .ok data := savedTrace then
     if data.depHash == inputHash then
       if let some out := data.outputs? then
         try
-          let arts ← resolveOutputs out none none
-          if updateCache then
-            if let .error e ← (cache.writeOutputs pkg.cacheScope inputHash out).toBaseIO then
+          let arts ← resolveOutputs (.ofData out)
+          if (← pkg.isArtifactCacheWritable) then
+            let act := (← getLakeCache).writeOutputs pkg.cacheScope inputHash out
+            if let .error e ← act.toBaseIO then
               logWarning s!"could not write outputs to cache: {e}"
           return some arts
         catch e =>
           dropLogFrom e
   return none
 
+open ResolveOutputs in
+/--
+Retrieve artifacts from the Lake cache using the outputs stored in either
+the saved trace file or (unless `traceOnly` is `true`) in the cached input-to-content mapping.
+
+**For internal use only.**
+-/
+@[inline] public nonrec def getArtifacts?
+  [ResolveOutputs α] (inputHash : Hash) (savedTrace : SavedTrace) (pkg : Package)
+: JobM (Option α) := do
+  if let some a ← getArtifactsUsingCache? inputHash pkg then
+    return some a
+  if let some a ← getArtifactsUsingTrace? inputHash savedTrace pkg then
+    return some a
+  return none
+
 /-- **For internal use only.** -/
 public def resolveArtifact
   (descr : ArtifactDescr)
@@ -549,6 +577,7 @@ public def resolveArtifact
   | .error (.noFileOrDirectory ..) =>
     -- we redownload artifacts on any error
     if let some service := service? then
+      updateAction .fetch
       if let some service := ws.findCacheService? service.toString then
         let some scope := scope?
           | error s!"artifact with associated cache service but no scope"
@@ -573,19 +602,17 @@ public def resolveArtifact
   | .error e =>
     error s!"failed to retrieve artifact from cache: {e}"
 
-def resolveArtifactOutput
-  (out : Json) (service? : Option CacheServiceName) (scope? : Option CacheServiceScope)
-  (exe := false)
-: JobM Artifact := do
-  match fromJson? out with
-  | .ok descr => resolveArtifact descr service? scope? exe
-  | .error e => error s!"ill-formed artifact output:\n{out.render.pretty 80 2}\n{e}"
+/-- **For internal use only.** -/
+public def resolveArtifactOutput (out : CacheOutput) (exe := false) : JobM Artifact := do
+  match fromJson? out.data with
+  | .ok descr => resolveArtifact descr out.service? out.scope? exe
+  | .error e => error s!"ill-formed artifact output:\n{out.data.render.pretty 80 2}\n{e}"
 
 set_option linter.unusedVariables false in
 /-- An artifact equipped with information about whether it is executable. -/
 def XArtifact (exe : Bool) := Artifact
 
-instance : ResolveOutputs (XArtifact exe) := ⟨resolveArtifactOutput (exe := exe)⟩
+instance : ResolveOutputs (XArtifact exe) := ⟨(resolveArtifactOutput (exe := exe))⟩
 
 /--
 Construct an artifact from a path outside the Lake artifact cache.
@@ -675,8 +702,9 @@ public def buildArtifactUnlessUpToDate
           if let some art ← fetchArt? (restore := true) then
             return art
         doBuild depTrace traceFile
-    if let some outputsRef := pkg.outputsRef? then
-      outputsRef.insert inputHash art.descr
+    if pkg.isRoot then
+      if let some outputsRef := (← getBuildContext).outputsRef? then
+        outputsRef.insert inputHash art.descr
     setTrace art.trace
     setMTime art traceFile
   else

src/lake/Lake/Build/Context.lean

@@ -6,6 +6,7 @@ Authors: Mac Malone
 module
 
 prelude
+public import Lake.Config.Cache
 public import Lake.Config.Context
 public import Lake.Build.Job.Basic
 
@@ -48,6 +49,11 @@ public def JobQueue := IO.Ref (Array OpaqueJob)
 public structure BuildContext extends BuildConfig, Context where
   leanTrace : BuildTrace
   registeredJobs : JobQueue
+  /--
+  Input-to-output(s) map for hashes of the root package's artifacts.
+  If `none`, tracking outputs is disabled for this build.
+  -/
+  outputsRef? : Option CacheRef := none
 
 /-- A transformer to equip a monad with a `BuildContext`. -/
 public abbrev BuildT := ReaderT BuildContext

src/lake/Lake/Build/Facets.lean

@@ -126,6 +126,9 @@ Its trace just includes its dependencies.
 -/
 builtin_facet leanArts : Module => ModuleOutputArtifacts
 
+/-- A compressed archive (produced via `leantar`) of the module's build artifacts. -/
+builtin_facet ltar : Module => FilePath
+
 /-- The `olean` file produced by `lean`. -/
 builtin_facet olean : Module => FilePath
 

src/lake/Lake/Build/Infos.lean

@@ -180,6 +180,9 @@ namespace Module
 @[inherit_doc cFacet] public abbrev bc (self : Module) :=
   self.facetCore bcFacet
 
+@[inherit_doc ltarFacet] public abbrev ltar (self : Module) :=
+  self.facetCore ltarFacet
+
 @[inherit_doc oFacet] public abbrev o (self : Module) :=
   self.facetCore oFacet
 

src/lake/Lake/Build/Module.lean

@@ -562,6 +562,7 @@ public def Module.depsFacetConfig : ModuleFacetConfig depsFacet :=
 /-- Remove all existing artifacts produced by the Lean build of the module. -/
 public def Module.clearOutputArtifacts (mod : Module) : IO PUnit := do
   try
+    removeFileIfExists mod.ltarFile
     removeFileIfExists mod.oleanFile
     removeFileIfExists mod.oleanServerFile
     removeFileIfExists mod.oleanPrivateFile
@@ -575,6 +576,7 @@ public def Module.clearOutputArtifacts (mod : Module) : IO PUnit := do
 /-- Remove any cached file hashes of the module build outputs (in `.hash` files). -/
 public def Module.clearOutputHashes (mod : Module) : IO PUnit := do
   try
+    clearFileHash mod.ltarFile
     clearFileHash mod.oleanFile
     clearFileHash mod.oleanServerFile
     clearFileHash mod.oleanPrivateFile
@@ -587,6 +589,8 @@ public def Module.clearOutputHashes (mod : Module) : IO PUnit := do
 
 /-- Cache the file hashes of the module build outputs in `.hash` files. -/
 public def Module.cacheOutputHashes (mod : Module) : IO PUnit := do
+  if (← mod.ltarFile.pathExists) then
+    cacheFileHash mod.ltarFile
   cacheFileHash mod.oleanFile
   if (← mod.oleanServerFile.pathExists) then
     cacheFileHash mod.oleanServerFile
@@ -599,37 +603,68 @@ public def Module.cacheOutputHashes (mod : Module) : IO PUnit := do
   if Lean.Internal.hasLLVMBackend () then
     cacheFileHash mod.bcFile
 
-def resolveModuleOutputs
-  (out : Json) (service? : Option CacheServiceName) (scope? : Option CacheServiceScope)
+def ModuleOutputDescrs.resolve
+  (descrs : ModuleOutputDescrs) (service? : Option CacheServiceName) (scope? : Option CacheServiceScope)
 : JobM ModuleOutputArtifacts := do
-  match fromJson? out with
-  | .ok (descrs : ModuleOutputDescrs) => do
-    let arts : ModuleOutputArtifacts := {
-      olean := ← resolve descrs.olean
-      oleanServer? := ← descrs.oleanServer?.mapM resolve
-      oleanPrivate? := ← descrs.oleanPrivate?.mapM resolve
-      ir? := ← descrs.ir?.mapM resolve
-      ilean := ← resolve descrs.ilean
-      c :=← resolve descrs.c
-      bc? := none
-    }
-    if Lean.Internal.hasLLVMBackend () then
-      let some descr := descrs.bc?
-        | error "LLVM backend enabled but module outputs lack bitcode"
-      return {arts with bc? := some (← resolve descr)}
-    else
-      return arts
-  | .error e =>
-    error s!"ill-formed module outputs:\n{out.render.pretty 80 2}\n{e}"
+  let arts : ModuleOutputArtifacts := {
+    isModule := descrs.isModule
+    olean := ← resolve descrs.olean
+    oleanServer? := ← descrs.oleanServer?.mapM resolve
+    oleanPrivate? := ← descrs.oleanPrivate?.mapM resolve
+    ir? := ← descrs.ir?.mapM resolve
+    ilean := ← resolve descrs.ilean
+    c := ← resolve descrs.c
+    ltar? := ← descrs.ltar?.mapM resolve
+  }
+  if Lean.Internal.hasLLVMBackend () then
+    let some descr := descrs.bc?
+      | error "LLVM backend enabled but module outputs lack bitcode"
+    return {arts with bc? := some (← resolve descr)}
+  else
+    return arts
 where @[inline] resolve descr := resolveArtifact descr service? scope?
 
-instance : ResolveOutputs ModuleOutputArtifacts := ⟨resolveModuleOutputs⟩
+def resolveModuleOutputArtifacts (out : CacheOutput) : JobM ModuleOutputArtifacts := do
+  match fromJson? out.data with
+  | .ok (descrs : ModuleOutputDescrs) => descrs.resolve out.service? out.scope?
+  | .error e => error s!"ill-formed module outputs:\n{out.data.render.pretty 80 2}\n{e}"
+
+instance : ResolveOutputs ModuleOutputArtifacts := ⟨resolveModuleOutputArtifacts⟩
+
+inductive ModuleOutputs
+| ltar (art : Artifact)
+| arts (arts : ModuleOutputArtifacts)
+
+instance : Coe ModuleOutputArtifacts ModuleOutputs := ⟨.arts⟩
+
+def resolveModuleOutputs (out : CacheOutput) : JobM ModuleOutputs := do
+  if let .str descr := out.data then
+    match ArtifactDescr.ofFilePath? descr with
+    | .ok descr =>
+      return .ltar (← resolveArtifact descr out.service? out.scope?)
+    | .error e =>
+      error s!"ill-formed module archive output:\n{out.data.render.pretty 80 2}\n{e}"
+  else
+    match fromJson? out.data with
+    | .ok (descrs : ModuleOutputDescrs) =>
+      if let some descr := descrs.ltar? then
+        try
+          descrs.resolve out.service? out.scope?
+        catch e =>
+          dropLogFrom e
+          return .ltar (← resolveArtifact descr out.service? out.scope?)
+      else
+        descrs.resolve out.service? out.scope?
+    | .error e => error s!"ill-formed module outputs:\n{out.data.render.pretty 80 2}\n{e}"
+
+instance : ResolveOutputs ModuleOutputs := ⟨resolveModuleOutputs⟩
 
 /-- Save module build artifacts to the local Lake cache. -/
 private def Module.cacheOutputArtifacts
   (mod : Module)  (isModule : Bool) (useLocalFile : Bool)
 : JobM ModuleOutputArtifacts := do
   return {
+    isModule
     olean := ← cache mod.oleanFile "olean"
     oleanServer? := ← cacheIf? isModule mod.oleanServerFile "olean.server"
     oleanPrivate? := ← cacheIf? isModule mod.oleanPrivateFile "olean.private"
@@ -637,6 +672,7 @@ private def Module.cacheOutputArtifacts
     ilean := ← cache mod.ileanFile "ilean"
     c := ← cache mod.cFile "c"
     bc? := ← cacheIf? (Lean.Internal.hasLLVMBackend ()) mod.bcFile "bc"
+    ltar? := ← cacheIf? (← mod.ltarFile.pathExists) mod.ltarFile "ltar"
   }
 where
   @[inline] cache file ext := do
@@ -664,11 +700,12 @@ private def Module.restoreAllArtifacts (mod : Module) (cached : ModuleOutputArti
     ir? := ← restoreSome mod.irFile cached.ir?
     c := ← restoreArtifact mod.cFile cached.c
     bc? := ← restoreSome mod.bcFile cached.bc?
+    ltar? := ← restoreSome mod.ltarFile cached.ltar?
   }
 where
   @[inline] restoreSome file art? := art?.mapM (restoreArtifact file ·)
 
-public protected def Module.checkExists (self : Module) (isModule : Bool) : BaseIO Bool := do
+public def Module.checkArtifactsExsist (self : Module) (isModule : Bool) : BaseIO Bool := do
   unless (← self.oleanFile.pathExists) do return false
   unless (← self.ileanFile.pathExists) do return false
   unless (← self.cFile.pathExists) do return false
@@ -680,22 +717,30 @@ public protected def Module.checkExists (self : Module) (isModule : Bool) : Base
     unless (← self.irFile.pathExists) do return false
   return true
 
+public protected def Module.checkExists (self : Module) (isModule : Bool) : BaseIO Bool := do
+  self.ltarFile.pathExists <||> self.checkArtifactsExsist isModule
+
 @[deprecated Module.checkExists (since := "2025-03-04")]
 public instance : CheckExists Module := ⟨Module.checkExists (isModule := false)⟩
 
 public protected def Module.getMTime (self : Module) (isModule : Bool) : IO MTime := do
-  let mut mtime :=
-    (← getMTime self.oleanFile)
-    |> max (← getMTime self.ileanFile)
-    |> max (← getMTime self.cFile)
-  if Lean.Internal.hasLLVMBackend () then
-    mtime := max mtime (← getMTime self.bcFile)
-  if isModule then
-    mtime := mtime
-    |> max (← getMTime self.oleanServerFile)
-    |> max (← getMTime self.oleanPrivateFile)
-    |> max (← getMTime self.irFile)
-  return mtime
+  try
+    let mut mtime :=
+      (← getMTime self.oleanFile)
+      |> max (← getMTime self.ileanFile)
+      |> max (← getMTime self.cFile)
+    if Lean.Internal.hasLLVMBackend () then
+      mtime := max mtime (← getMTime self.bcFile)
+    if isModule then
+      mtime := mtime
+      |> max (← getMTime self.oleanServerFile)
+      |> max (← getMTime self.oleanPrivateFile)
+      |> max (← getMTime self.irFile)
+    return mtime
+  catch e =>
+    try getMTime self.ltarFile catch
+    | .noFileOrDirectory .. => throw e
+    | e => throw e
 
 @[deprecated Module.getMTime (since := "2025-03-04")]
 public instance : GetMTime Module := ⟨Module.getMTime (isModule := false)⟩
@@ -711,7 +756,6 @@ private def ModuleOutputArtifacts.setMTime (self : ModuleOutputArtifacts) (mtime
     bc? := self.bc?.map ({· with mtime})
   }
 
-
 private def Module.mkArtifacts (mod : Module) (srcFile : FilePath) (isModule : Bool) : ModuleArtifacts where
   lean? := srcFile
   olean? := mod.oleanFile
@@ -724,6 +768,7 @@ private def Module.mkArtifacts (mod : Module) (srcFile : FilePath) (isModule : B
 
 private def Module.computeArtifacts (mod : Module) (isModule : Bool) : FetchM ModuleOutputArtifacts :=
   return {
+    isModule
     olean := ← compute mod.oleanFile "olean"
     oleanServer? := ← computeIf isModule mod.oleanServerFile "olean.server"
     oleanPrivate? := ← computeIf isModule mod.oleanPrivateFile "olean.private"
@@ -741,6 +786,66 @@ where
 
 instance : ToOutputJson ModuleOutputArtifacts := ⟨(toJson ·.descrs)⟩
 
+def Module.packLtar (self : Module) (arts : ModuleOutputArtifacts) : JobM Artifact := do
+  let arts ← id do
+    if (← self.checkArtifactsExsist arts.isModule) then
+      return arts
+    else self.restoreAllArtifacts arts
+  let args ← id do
+    let mut args := #[
+      "-C", self.leanLibDir.toString,
+      "-C", self.irDir.toString,
+      self.ltarFile.toString,
+      self.fileName "trace"
+    ]
+    let addArt args idx art :=
+      args.push "-i" |>.push idx |>.push (self.fileName art.ext)
+    -- Note: oleans parts must be in the order of `.olean`, `.olean.server`, `.olean.private`
+    args := addArt args "0" arts.olean
+    if let some art := arts.oleanServer? then
+      args := addArt args "0" art
+    if let some art := arts.oleanPrivate? then
+      args := addArt args "0" art
+    args := addArt args "0" arts.ilean
+    if let some art := arts.ir? then
+      args := addArt args "0" art
+    args := addArt args "1" arts.c
+    if Lean.Internal.hasLLVMBackend () then
+      let some art := arts.bc?
+        | error "LLVM backend enabled but module outputs lack bitcode"
+      args := addArt args "1" art
+    return args
+  proc (quiet := true) {cmd := (← getLeantar).toString, args}
+  if (← self.pkg.isArtifactCacheWritable) then
+    cacheArtifact self.ltarFile "ltar" (← self.pkg.restoreAllArtifacts)
+  else
+    computeArtifact self.ltarFile "ltar"
+
+def Module.unpackLtar (self : Module) (ltar : FilePath) : JobM Unit := do
+  let args := #[
+    "-C", self.leanLibDir.toString,
+    "-C", self.irDir.toString,
+    "-x", ltar.toString
+  ]
+  proc (quiet := true) {cmd := (← getLeantar).toString, args}
+
+private def Module.recBuildLtar (self : Module) : FetchM (Job FilePath) := do
+  withRegisterJob s!"{self.name}:ltar" <| withCurrPackage self.pkg do
+  (← self.leanArts.fetch).mapM fun arts => do
+    let art ← arts.ltar?.getDM do
+      if (← getNoBuild) then
+        modify ({· with wantsRebuild := true})
+        error "archive does not exist and needs to be built"
+      else
+        self.packLtar arts
+    newTrace s!"{self.name.toString}:ltar"
+    addTrace art.trace
+    return art.path
+
+/-- The `ModuleFacetConfig` for the builtin `ltarFacet`. -/
+public def Module.ltarFacetConfig : ModuleFacetConfig ltarFacet :=
+  mkFacetJobConfig recBuildLtar
+
 private def Module.buildLean
   (mod : Module) (depTrace : BuildTrace) (srcFile : FilePath) (setup : ModuleSetup)
 : JobM ModuleOutputArtifacts := buildAction depTrace mod.traceFile do
@@ -786,45 +891,100 @@ private def Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifac
     addPureTrace mod.pkg.id? "Package.id?"
     addPureTrace mod.leanArgs "Module.leanArgs"
     setTraceCaption s!"{mod.name.toString}:leanArts"
-    let depTrace ← getTrace
-    let inputHash := depTrace.hash
-    let savedTrace ← readTraceFile mod.traceFile
-    have : CheckExists Module := ⟨Module.checkExists (isModule := setup.isModule)⟩
-    have : GetMTime Module := ⟨Module.getMTime (isModule := setup.isModule)⟩
-    let fetchArtsFromCache? restoreAll := do
-      let some arts ← getArtifacts? inputHash savedTrace mod.pkg
-        | return none
+    let arts ← fetchCore setup srcFile srcTrace
+    let arts ← trackOutputsIfEnabled arts
+    let arts ← adjustMTime arts
+    return arts
+where
+  fetchFromCache? setup savedTrace restoreAll : JobM (ModuleOutputArtifacts ⊕ SavedTrace) := do
+    let inputHash := (← getTrace).hash
+    let some ltarOrArts ← getArtifacts? inputHash savedTrace mod.pkg
+      | return .inr savedTrace
+    match (ltarOrArts : ModuleOutputs)  with
+    | .ltar ltar =>
+      mod.clearOutputArtifacts
+      mod.unpackLtar ltar.path
+      -- Note: This branch implies that only the ltar output is (validly) cached.
+      -- Thus, we use only the new trace unpacked from the ltar to resolve further artifacts.
+      let savedTrace ← readTraceFile mod.traceFile
+      let arts? ← getArtifactsUsingTrace? inputHash savedTrace mod.pkg
+      if let some (arts : ModuleOutputArtifacts) := arts? then
+        -- on initial unpack from cache ensure all artifacts uniformly
+        -- end up in the build directory and, if writable, the cache
+        let arts ← mod.restoreAllArtifacts {arts with ltar? := some ltar}
+        if (← mod.pkg.isArtifactCacheWritable) then
+          .inl <$> mod.cacheOutputArtifacts setup.isModule restoreAll
+        else
+          return .inl arts
+      else
+        return .inr savedTrace
+    | .arts arts =>
       unless (← savedTrace.replayOrFetchIfUpToDate inputHash) do
         mod.clearOutputArtifacts
         writeFetchTrace mod.traceFile inputHash (toJson arts.descrs)
-      if restoreAll then
-        some <$> mod.restoreAllArtifacts arts
-      else
-        some <$> mod.restoreNeededArtifacts arts
-    let arts ← id do
-      if (← mod.pkg.isArtifactCacheWritable) then
-        let restore ← mod.pkg.restoreAllArtifacts
-        if let some arts ← fetchArtsFromCache? restore then
+      let arts ←
+        if restoreAll then
+          mod.restoreAllArtifacts arts
+        else
+          mod.restoreNeededArtifacts arts
+      return .inl arts
+  fetchCore setup srcFile srcTrace : JobM ModuleOutputArtifacts := do
+    let depTrace ← getTrace
+    have : GetMTime Module := ⟨Module.getMTime (isModule := setup.isModule)⟩
+    have : CheckExists Module := ⟨Module.checkExists (isModule := setup.isModule)⟩
+    let savedTrace ← readTraceFile mod.traceFile
+    if (← mod.pkg.isArtifactCacheWritable) then
+      let restore ← mod.pkg.restoreAllArtifacts
+      match (← fetchFromCache? setup savedTrace restore) with
+      | .inl arts =>
+        return arts
+      | .inr savedTrace =>
+        let status ← savedTrace.replayIfUpToDate' (oldTrace := srcTrace.mtime) mod depTrace
+        if status.isUpToDate then
+          unless (← mod.checkArtifactsExsist setup.isModule) do
+            mod.unpackLtar mod.ltarFile
+        else
+          discard <| mod.buildLean depTrace srcFile setup
+        if status.isCacheable then
+          let arts ← mod.cacheOutputArtifacts setup.isModule restore
+          (← getLakeCache).writeOutputs mod.pkg.cacheScope depTrace.hash arts.descrs
           return arts
         else
-          let status ← savedTrace.replayIfUpToDate' (oldTrace := srcTrace.mtime) mod depTrace
-          unless status.isUpToDate do
-            discard <| mod.buildLean depTrace srcFile setup
-          if status.isCacheable then
-            let arts ← mod.cacheOutputArtifacts setup.isModule restore
-            (← getLakeCache).writeOutputs mod.pkg.cacheScope inputHash arts.descrs
-            return arts
-          else
-            mod.computeArtifacts setup.isModule
-      else if (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) then
+          mod.computeArtifacts setup.isModule
+    else
+      if (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) then
+        unless (← mod.checkArtifactsExsist setup.isModule) do
+          mod.unpackLtar mod.ltarFile
         mod.computeArtifacts setup.isModule
       else
         if (← mod.pkg.isArtifactCacheReadable) then
-          if let some arts ← fetchArtsFromCache? true then
-            return arts
-        mod.buildLean depTrace srcFile setup
-    if let some ref := mod.pkg.outputsRef? then
-      ref.insert inputHash arts.descrs
+          match (← fetchFromCache? setup savedTrace true) with
+          | .inl arts =>
+              return arts
+          | .inr savedTrace =>
+            if (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) then
+              mod.computeArtifacts setup.isModule
+            else
+              mod.buildLean depTrace srcFile setup
+        else
+          mod.buildLean depTrace srcFile setup
+  trackOutputsIfEnabled arts : JobM ModuleOutputArtifacts := do
+    if mod.pkg.isRoot then
+      if let some ref := (← getBuildContext).outputsRef? then
+        let inputHash := (← getTrace).hash
+        if let some ltar := arts.ltar? then
+          ref.insert inputHash ltar.descr
+          return arts
+        else
+          let ltar ← id do
+            if (← mod.ltarFile.pathExists) then
+              computeArtifact mod.ltarFile "ltar"
+            else
+              mod.packLtar arts
+          ref.insert inputHash ltar.descr
+          return {arts with ltar? := some ltar}
+    return arts
+  adjustMTime arts : JobM ModuleOutputArtifacts := do
     match (← getMTime mod.traceFile |>.toBaseIO) with
     | .ok mtime =>
       return arts.setMTime mtime
@@ -846,7 +1006,7 @@ public def Module.leanArtsFacetConfig : ModuleFacetConfig leanArtsFacet :=
       /-
       Avoid recompiling unchanged OLean files.
       OLean files transitively include their imports.
-      THowever, imports are pre-resolved by Lake, so they are not included in their trace.
+      However, imports are pre-resolved by Lake, so they are not included in their trace.
       -/
       newTrace s!"{mod.name.toString}:{facet}"
       addTrace art.trace
@@ -891,7 +1051,7 @@ public def Module.cFacetConfig : ModuleFacetConfig cFacet :=
       let art := arts.c
       /-
       Avoid recompiling unchanged C files.
-      C files are assumed to incorporate their own content
+      C files are assumed to only incorporate their own content
       and not transitively include their inputs (e.g., imports).
       They do, however, include `lean/lean.h`.
       Lean also produces LF-only C files, so no line ending normalization.
@@ -1031,6 +1191,7 @@ public def Module.initFacetConfigs : DNameMap ModuleFacetConfig :=
   |>.insert importArtsFacet importArtsFacetConfig
   |>.insert importAllArtsFacet importAllArtsFacetConfig
   |>.insert exportInfoFacet exportInfoFacetConfig
+  |>.insert ltarFacet ltarFacetConfig
   |>.insert oleanFacet oleanFacetConfig
   |>.insert oleanServerFacet oleanServerFacetConfig
   |>.insert oleanPrivateFacet oleanPrivateFacetConfig

src/lake/Lake/Build/ModuleArtifacts.lean

@@ -15,6 +15,7 @@ namespace Lake
 
 /-- The descriptions of the output artifacts of a module build. -/
 public structure ModuleOutputDescrs where
+  isModule : Bool
   olean : ArtifactDescr
   oleanServer? : Option ArtifactDescr := none
   oleanPrivate? : Option ArtifactDescr := none
@@ -22,6 +23,7 @@ public structure ModuleOutputDescrs where
   ir? : Option ArtifactDescr := none
   c : ArtifactDescr
   bc? : Option ArtifactDescr := none
+  ltar? : Option ArtifactDescr := none
 
 public def ModuleOutputDescrs.oleanParts (self : ModuleOutputDescrs) : Array ArtifactDescr := Id.run do
   let mut descrs := #[self.olean]
@@ -33,6 +35,7 @@ public def ModuleOutputDescrs.oleanParts (self : ModuleOutputDescrs) : Array Art
 
 public protected def ModuleOutputDescrs.toJson (self : ModuleOutputDescrs) : Json := Id.run do
   let mut obj : JsonObject := {}
+  obj := obj.insert "m" self.isModule
   obj := obj.insert "o" self.oleanParts
   obj := obj.insert "i" self.ilean
   if let some ir := self.ir? then
@@ -40,6 +43,8 @@ public protected def ModuleOutputDescrs.toJson (self : ModuleOutputDescrs) : Jso
   obj := obj.insert "c" self.c
   if let some bc := self.bc? then
     obj := obj.insert "b" bc
+  if let some ltar := self.ltar? then
+    obj := obj.insert "l" ltar
   return obj
 
 public instance : ToJson ModuleOutputDescrs := ⟨ModuleOutputDescrs.toJson⟩
@@ -50,6 +55,7 @@ public protected def ModuleOutputDescrs.fromJson? (val : Json) : Except String M
   let some olean := oleanHashes[0]?
     | throw "expected a least one 'o' (.olean) hash"
   return {
+    isModule := (← obj.get? "m").getD (oleanHashes.size > 1)
     olean := olean
     oleanServer? := oleanHashes[1]?
     oleanPrivate? := oleanHashes[2]?
@@ -57,12 +63,14 @@ public protected def ModuleOutputDescrs.fromJson? (val : Json) : Except String M
     ir? := ← obj.get? "r"
     c := ← obj.get "c"
     bc? := ← obj.get? "b"
+    ltar? := ← obj.get? "l"
   }
 
 public instance : FromJson ModuleOutputDescrs := ⟨ModuleOutputDescrs.fromJson?⟩
 
 /-- The output artifacts of a module build. -/
 public structure ModuleOutputArtifacts where
+  isModule : Bool
   olean : Artifact
   oleanServer? : Option Artifact := none
   oleanPrivate? : Option Artifact := none
@@ -70,9 +78,11 @@ public structure ModuleOutputArtifacts where
   ir? : Option Artifact := none
   c : Artifact
   bc? : Option Artifact := none
+  ltar? : Option Artifact := none
 
 /-- Content hashes of the artifacts. -/
 public def ModuleOutputArtifacts.descrs (arts : ModuleOutputArtifacts) : ModuleOutputDescrs where
+  isModule := arts.isModule
   olean := arts.olean.descr
   oleanServer? := arts.oleanServer?.map (·.descr)
   oleanPrivate? := arts.oleanPrivate?.map (·.descr)
@@ -80,3 +90,4 @@ public def ModuleOutputArtifacts.descrs (arts : ModuleOutputArtifacts) : ModuleO
   ir? := arts.ir?.map (·.descr)
   c := arts.c.descr
   bc? := arts.bc?.map (·.descr)
+  ltar? := arts.ltar?.map (·.descr)

src/lake/Lake/Build/Run.lean

@@ -260,14 +260,14 @@ public def monitorJobs
 public def noBuildCode : ExitCode := 3
 
 def Workspace.saveOutputs
-  [logger : MonadLog BaseIO] (ws : Workspace)
+  [logger : MonadLog BaseIO] (ws : Workspace) (outputsRef? : Option CacheRef)
   (out : IO.FS.Stream) (outputsFile : FilePath) (isVerbose : Bool)
 : BaseIO Unit := do
   unless ws.isRootArtifactCacheWritable do
     logWarning s!"{ws.root.prettyName}: \
       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
+  if let some ref := outputsRef? then
     match (← (← ref.get).writeFile outputsFile {}) with
     | .ok _ log =>
       if !log.isEmpty && isVerbose then
@@ -314,27 +314,34 @@ def monitorJob (ctx : MonitorContext) (job : Job α) : BaseIO (BuildResult α) :
   else
     return {toMonitorResult := result, out := .error "build failed"}
 
-def mkBuildContext' (ws : Workspace) (cfg : BuildConfig) (jobs : JobQueue) : BuildContext where
+def mkBuildContext'
+  (ws : Workspace) (cfg : BuildConfig) (jobs : JobQueue)
+: BaseIO BuildContext := return {
   opaqueWs := ws
   toBuildConfig := cfg
+  outputsRef? := ← id do
+    if cfg.outputsFile?.isSome then
+      some <$> CacheRef.mk
+    else
+      return none
   registeredJobs := jobs
   leanTrace := .ofHash (pureHash ws.lakeEnv.leanGithash)
     s!"Lean {Lean.versionStringCore}, commit {ws.lakeEnv.leanGithash}"
+}
 
 def Workspace.startBuild
-  (ws : Workspace)  (cfg : BuildConfig) (jobs : JobQueue) (build : FetchM α)
-  (caption := "job computation")
+  (bctx : BuildContext) (build : FetchM α) (caption := "job computation")
 : BaseIO (Job α) := do
-  let bctx := mkBuildContext' ws cfg jobs
   let compute := Job.async build (caption := caption)
   compute.run.run'.run bctx |>.run nilTrace
 
-def Workspace.finalizeBuild
-  (ws : Workspace) (cfg : BuildConfig) (ctx : MonitorContext) (result : BuildResult α)
+def finalizeBuild
+  (cfg : BuildConfig) (bctx : BuildContext ) (mctx : MonitorContext) (result : BuildResult α)
 : IO α := do
-  reportResult cfg ctx.out result
+  reportResult cfg mctx.out result
   if let some outputsFile := cfg.outputsFile? then
-    ws.saveOutputs (logger := ctx.logger) ctx.out outputsFile (cfg.verbosity matches .verbose)
+    bctx.workspace.saveOutputs (logger := mctx.logger)
+      bctx.outputsRef? mctx.out outputsFile (cfg.verbosity matches .verbose)
   match result.out with
   | .ok a =>
     return a
@@ -354,9 +361,10 @@ public def Workspace.runFetchM
 : IO α := do
   let jobs ← mkJobQueue
   let mctx ← mkMonitorContext cfg jobs
-  let job ← ws.startBuild cfg jobs build caption
+  let bctx ← mkBuildContext' ws cfg jobs
+  let job ← startBuild bctx build caption
   let result ← monitorJob mctx job
-  ws.finalizeBuild cfg mctx result
+  finalizeBuild cfg bctx mctx result
 
 def monitorBuild (mctx : MonitorContext) (job : Job (Job α)) : BaseIO (BuildResult α) := do
   let result ← monitorJob mctx job
@@ -382,7 +390,8 @@ public def Workspace.checkNoBuild
   let jobs ← mkJobQueue
   let cfg := {noBuild := true}
   let mctx ← mkMonitorContext cfg jobs
-  let job ← ws.startBuild cfg jobs build
+  let bctx ← mkBuildContext' ws cfg jobs
+  let job ← startBuild bctx build
   let result ← monitorBuild mctx job
   return result.isOk -- `isOk` means no failures, and thus no `--no-build` failures
 
@@ -392,9 +401,10 @@ public def Workspace.runBuild
 : IO α := do
   let jobs ← mkJobQueue
   let mctx ← mkMonitorContext cfg jobs
-  let job ← ws.startBuild cfg jobs build
+  let bctx ← mkBuildContext' ws cfg jobs
+  let job ← startBuild bctx build
   let result ← monitorBuild mctx job
-  ws.finalizeBuild cfg mctx result
+  finalizeBuild cfg bctx mctx result
 
 /-- Produce a build job in the Lake monad's workspace and await the result. -/
 @[inline] public def runBuild

src/lake/Lake/Config/Cache.lean

@@ -166,8 +166,7 @@ where go as o := do
   match o with
   | .null =>
     return as
-  | .bool b =>
-    logError s!"unsupported output: {b}"
+  | .bool _ => -- boolean metadata is allowed (as of 2025-03-13)
     return as
   | .num o =>
     match Hash.ofJsonNumber? o with
@@ -297,7 +296,8 @@ public structure CacheOutput where
 
 namespace CacheOutput
 
-@[inline] def ofData (data : Json) : CacheOutput := {data}
+/-- **For internal use only.** -/
+@[inline] public def ofData (data : Json) : CacheOutput := {data}
 
 public protected def toJson (out : CacheOutput) : Json := Id.run do
   let mut obj :=

src/lake/Lake/Config/Module.lean

@@ -77,6 +77,9 @@ public abbrev pkg (self : Module) : Package :=
 @[inline] public def rootDir (self : Module) : FilePath :=
   self.lib.rootDir
 
+@[inline] public def fileName (ext : String) (self : Module) : String :=
+  FilePath.addExtension self.name.getString! ext |>.toString
+
 @[inline] public def filePath (dir : FilePath) (ext : String) (self : Module) : FilePath :=
   Lean.modToFilePath dir self.name ext
 
@@ -92,6 +95,9 @@ public abbrev pkg (self : Module) : Package :=
 @[inline] public def leanLibPath (ext : String) (self : Module) : FilePath :=
   self.filePath self.pkg.leanLibDir ext
 
+@[inline] public def leanLibDir (self : Module) : FilePath :=
+  Lean.modToFilePath self.pkg.leanLibDir self.name.getPrefix ""
+
 @[inline] public def oleanFile (self : Module) : FilePath :=
   self.leanLibPath "olean"
 
@@ -104,18 +110,21 @@ public abbrev pkg (self : Module) : Package :=
 @[inline] public def ileanFile (self : Module) : FilePath :=
   self.leanLibPath "ilean"
 
+@[inline] public def irFile (self : Module) : FilePath :=
+  self.leanLibPath "ir"
+
 @[inline] public def traceFile (self : Module) : FilePath :=
   self.leanLibPath "trace"
 
 @[inline] public def irPath (ext : String) (self : Module) : FilePath :=
   self.filePath self.pkg.irDir ext
 
+@[inline] public def irDir (self : Module) : FilePath :=
+  Lean.modToFilePath self.pkg.irDir self.name.getPrefix ""
+
 @[inline] public def setupFile (self : Module) : FilePath :=
   self.irPath "setup.json"
 
-@[inline] public def irFile (self : Module) : FilePath :=
-  self.leanLibPath "ir"
-
 @[inline] public def cFile (self : Module) : FilePath :=
   self.irPath "c"
 
@@ -134,6 +143,9 @@ public def bcFile? (self : Module) : Option FilePath :=
 @[inline] public def bcoFile (self : Module) : FilePath :=
   self.irPath "bc.o"
 
+@[inline] public def ltarFile (self : Module) : FilePath :=
+  self.irPath "ltar"
+
 /-- Suffix for single module dynlibs (e.g., for precompilation). -/
 public def dynlibSuffix := "-1"
 

src/lake/Lake/Config/Monad.lean

@@ -300,6 +300,10 @@ variable [Functor m]
 @[inline] public def getLeanc : m FilePath :=
   (·.leanc) <$> getLeanInstall
 
+/-- Returns the path of the {lit}`leantar` binary in the detected Lean installation. -/
+@[inline] public def getLeantar : m FilePath :=
+  (·.leantar) <$> getLeanInstall
+
 /-- Returns the path of the {lit}`libleanshared` library in the detected Lean installation. -/
 @[inline] public def getLeanSharedLib : m FilePath :=
   (·.sharedLib) <$> getLeanInstall

src/lake/Lake/Config/Package.lean

@@ -78,16 +78,6 @@ public structure Package where
   testDriver : String := config.testDriver
   /-- The driver used for `lake lint` when this package is the workspace root. -/
   lintDriver : String := config.lintDriver
-  /--
-  Input-to-output(s) map for hashes of package artifacts.
-  If `none`, the artifact cache is disabled for the package.
-  -/
-  inputsRef? : Option CacheRef := none
-  /--
-  Input-to-output(s) map for hashes of package artifacts.
-  If `none`, the artifact cache is disabled for the package.
-  -/
-  outputsRef? : Option CacheRef := none
 
 deriving Inhabited
 

src/lake/Lake/Load/Workspace.lean

@@ -32,7 +32,6 @@ public def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
   Lean.searchPathRef.set config.lakeEnv.leanSearchPath
   let lakeConfig ← loadLakeConfig config.lakeEnv
   let (root, env?) ← loadPackageCore "[root]" {config with pkgIdx := 0}
-  let root := {root with outputsRef? := ← CacheRef.mk}
   let ws : Workspace := {
     root
     lakeEnv := config.lakeEnv

tests/lake/lakefile.toml

@@ -1,6 +1,7 @@
 name = "lake"
 srcDir = "../../src/lake"
 defaultTargets = ["Lake", "lake"]
+leanOptions.backward.do.legacy = false
 
 [[lean_lib]]
 name = "Lake"

tests/lake/tests/ltar/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json produced.*

tests/lake/tests/ltar/lakefile.toml

@@ -0,0 +1,4 @@
+name = "test"
+
+[[lean_lib]]
+name = "Test"

tests/lake/tests/ltar/test.sh

@@ -0,0 +1,54 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+./clean.sh
+
+# Store Lake cache in a local directory
+export LAKE_CACHE_DIR=
+
+#-------------------------------------------------------------------------------
+# The tests covers the (offline) use of `leantar` in Lake
+#-------------------------------------------------------------------------------
+
+# Test regular build does not produce an `ltar`
+test_run build +Test -v
+test_exp ! -f .lake/build/ir/Test.ltar
+
+# Test use of `--no-build` with the `ltar` facet
+test_err "archive does not exist and needs to be built" \
+  build +Test:ltar --no-build -v
+
+# Test the build of the `ltar` facet
+test_run build +Test:ltar -v
+test_exp -f .lake/build/ir/Test.ltar
+
+# Test that Lake unpacks the archive if the module's artifacts are missing
+test_cmd rm .lake/build/lib/lean/Test.olean
+test_out "leantar" build +Test --no-build -v
+test_exp -f .lake/build/lib/lean/Test.olean
+
+# Test that Lake unpacks an modification time up-to-date archive
+# when the module's artifacts and trace are missing with `--old`
+test_cmd rm .lake/build/lib/lean/Test.olean .lake/build/lib/lean/Test.trace
+test_fails build +Test --no-build -v
+test_out "leantar" build +Test --no-build --old -v
+test_exp -f .lake/build/lib/lean/Test.olean
+
+# Test caching and restoring the `ltar`
+LAKE_ARTIFACT_CACHE=true test_run build +Test -v
+test_cmd ls .lake/cache/artifacts/*.ltar
+rm -rf .lake/build
+test_not_out "leantar" build +Test --no-build -v
+test_exp -f .lake/build/ir/Test.ltar
+
+# Test unpacking the archive from the cache
+rm -rf .lake/build .lake/cache/artifacts/*.[!l]*
+test_out "leantar" build +Test --no-build -v
+
+# Test producing an `ltar` without already restored artifacts
+rm -rf .lake/cache .lake/build
+LAKE_ARTIFACT_CACHE=true test_run build +Test -v
+rm -rf .lake/build
+LAKE_ARTIFACT_CACHE=true test_run build +Test:ltar -v
+test_exp -f .lake/build/lib/lean/Test.olean # forces restore
+test_exp -f .lake/build/ir/Test.ltar