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