feat: lake: restoreAllArtifacts (#10576)

This PR adds a new package configuration option: `restoreAllArtifacts`.
When set to `true` and the Lake local artifact cache is enabled, Lake
will copy all cached artifacts into the build directory. This ensures
they are available for external consumers who expect build results to be
in the build directory.

Author: tydeu

src/lake/Lake/Build/Common.lean

@@ -562,7 +562,7 @@ public def buildArtifactUnlessUpToDate
       else
         return some art
     if (← pkg.isArtifactCacheEnabled) then
-      if let some art ← fetchArt? restore then
+      if let some art ← fetchArt? (restore || pkg.restoreAllArtifacts) then
         setTrace art.trace
         if let some outputsRef := pkg.outputsRef? then
           outputsRef.insert inputHash art.hash

src/lake/Lake/Build/Module.lean

@@ -710,7 +710,7 @@ private def Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifac
         return none
     let arts ← id do
       if (← mod.pkg.isArtifactCacheEnabled) then
-        if let some arts ← fetchArtsFromCache? false then
+        if let some arts ← fetchArtsFromCache? mod.pkg.restoreAllArtifacts then
           return arts
         else
           unless (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) do

src/lake/Lake/Config/Package.lean

@@ -344,6 +344,10 @@ public def nativeLibDir (self : Package) : FilePath :=
 @[inline] public def enableArtifactCache? (self : Package) : Option Bool :=
   self.config.enableArtifactCache?
 
+/-- The package's `restoreAllArtifacts` configuration. -/
+@[inline] public def restoreAllArtifacts (self : Package) : Bool :=
+  self.config.restoreAllArtifacts
+
 /-- The directory within the Lake cache were package-scoped files are stored. -/
 public def cacheScope (self : Package) :=
   self.name.toString (escape := false)

src/lake/Lake/Config/PackageConfig.lean

@@ -295,6 +295,14 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
   -/
   enableArtifactCache?, enableArtifactCache : Option Bool := none
   /--
+  Whether, when the local artifact cache is enabled, Lake should copy all cached
+  artifacts into the build directory. This ensures the build results are available
+  to external consumers who expect them in the build directory.
+
+  Defaults to `false`.
+  -/
+  restoreAllArtifacts : Bool := false
+  /--
   Whether native libraries (of this package) should be prefixed with `lib` on Windows.
 
   Unlike Unix, Windows does not require native libraries to start with `lib` and,

src/lake/tests/cache/lakefile.lean

@@ -0,0 +1,16 @@
+import Lake
+open System Lake DSL
+
+package test where
+  enableArtifactCache := true
+  restoreAllArtifacts := get_config? restoreAll |>.isSome
+
+lean_lib Test
+
+lean_lib Module where
+  leanOptions := #[⟨`experimental.module, true⟩]
+
+lean_lib Ignored
+
+lean_exe test where
+  root := `Main

src/lake/tests/cache/lakefile.toml

@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+gi#!/usr/bin/env bash
 source ../common.sh
 
 ./clean.sh

src/lake/tests/cache/online-test.sh

@@ -55,7 +55,8 @@ test_exp "$cache_art" != "$local_art"
 test_cmd cmp -s "$cache_art" "$local_art"
 
 # Verify supported artifacts end up in the cache directory
-test_run build test:exe Test:static Test:shared +Test:o.export +Test:o.noexport
+test_run build \
+  test:exe Test:static Test:shared +Test:o.export +Test:o.noexport +Module
 test_cached() {
   target="$1"; shift
   art="$($LAKE query $target)"
@@ -71,7 +72,6 @@ test_cached +Test:dynlib !
 test_cached +Test:olean
 test_cached +Test:ilean !
 test_cached +Test:c
-test_run build +Module
 test_cached +Module:olean
 test_cached +Module:olean.server
 test_cached +Module:olean.private
@@ -134,5 +134,24 @@ test_cmd_eq 3 wc -l < .lake/outputs.jsonl
 test_run build Test:static -o .lake/outputs.jsonl
 test_cmd_eq 6 wc -l < .lake/outputs.jsonl
 
+# Verify all artifacts end up in the cache directory with `restoreAllArtifacts`
+test_cmd cp -r "$CACHE_DIR" .lake/cache-backup
+test_cmd rm -rf "$CACHE_DIR"
+test_run build -R -KrestoreAll=true \
+  test:exe Test:static Test:shared +Test:o.export +Test:o.noexport +Module
+test_cached test:exe !
+test_cached Test:static !
+test_cached Test:shared !
+test_cached +Test:o.export !
+test_cached +Test:o.noexport !
+test_cached +Test:dynlib !
+test_cached +Test:olean !
+test_cached +Test:ilean !
+test_cached +Test:c !
+test_cached +Module:olean !
+test_cached +Module:olean.server !
+test_cached +Module:olean.private !
+test_cached +Module:ir !
+
 # Cleanup
 rm -f produced.out Ignored.lean