From c3d9d0d9310fe758ecd6de7ab818def678f1c721 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Fri, 26 Sep 2025 16:58:32 -0400 Subject: [PATCH] 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. --- src/lake/Lake/Build/Common.lean | 2 +- src/lake/Lake/Build/Module.lean | 2 +- src/lake/Lake/Config/Package.lean | 4 ++++ src/lake/Lake/Config/PackageConfig.lean | 8 ++++++++ src/lake/tests/cache/lakefile.lean | 16 ++++++++++++++++ src/lake/tests/cache/lakefile.toml | 16 ---------------- src/lake/tests/cache/online-test.sh | 2 +- src/lake/tests/cache/test.sh | 23 +++++++++++++++++++++-- 8 files changed, 52 insertions(+), 21 deletions(-) create mode 100644 src/lake/tests/cache/lakefile.lean delete mode 100644 src/lake/tests/cache/lakefile.toml diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index afedb4dd8b..2050c99d41 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/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 diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 047e1b5783..08b827cfc0 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/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 diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 56d3cfb9d3..d8d3083cfe 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/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) diff --git a/src/lake/Lake/Config/PackageConfig.lean b/src/lake/Lake/Config/PackageConfig.lean index 3aa5dc5a50..cbaaa8e627 100644 --- a/src/lake/Lake/Config/PackageConfig.lean +++ b/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, diff --git a/src/lake/tests/cache/lakefile.lean b/src/lake/tests/cache/lakefile.lean new file mode 100644 index 0000000000..2d49a64243 --- /dev/null +++ b/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 diff --git a/src/lake/tests/cache/lakefile.toml b/src/lake/tests/cache/lakefile.toml deleted file mode 100644 index b723800ec7..0000000000 --- a/src/lake/tests/cache/lakefile.toml +++ /dev/null @@ -1,16 +0,0 @@ -name = "test" -enableArtifactCache = true - -[[lean_lib]] -name = "Test" - -[[lean_lib]] -name = "Module" -leanOptions.experimental.module = true - -[[lean_lib]] -name = "Ignored" - -[[lean_exe]] -name = "test" -root = "Main" diff --git a/src/lake/tests/cache/online-test.sh b/src/lake/tests/cache/online-test.sh index 04a90dc059..c9eb241df0 100755 --- a/src/lake/tests/cache/online-test.sh +++ b/src/lake/tests/cache/online-test.sh @@ -1,4 +1,4 @@ -#!/usr/bin/env bash +gi#!/usr/bin/env bash source ../common.sh ./clean.sh diff --git a/src/lake/tests/cache/test.sh b/src/lake/tests/cache/test.sh index 4a464615ba..6ee3cd79ec 100755 --- a/src/lake/tests/cache/test.sh +++ b/src/lake/tests/cache/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