max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: lake: ltar caching bug with build -o (#12993)

Browse source 
This PR fixes a bug with Lake where caching an `ltar` produced via `lake
build -o` would fail if `restoreAllArtifacts` was also `true`.
This commit is contained in:
Mac Malone 2026-03-19 18:51:09 -04:00 • committed by GitHub
parent 518a135777
commit d78525b302
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/lake/Lake/Build/Module.lean
View file

@ -817,7 +817,7 @@ def Module.packLtar (self : Module) (arts : ModuleOutputArtifacts) : JobM Artifa
return args
proc (quiet := true) {cmd := (← getLeantar).toString, args}
if (← self.pkg.isArtifactCacheWritable) then
cacheArtifact self.ltarFile "ltar" (← self.pkg.restoreAllArtifacts)
cacheArtifact self.ltarFile "ltar" (useLocalFile := ← self.pkg.restoreAllArtifacts)
else
computeArtifact self.ltarFile "ltar"

6
tests/lake/tests/ltar/restoreAll.toml Normal file
View file

@ -0,0 +1,6 @@
name = "test"
enableArtifactCache = true
restoreAllArtifacts = true
[[lean_lib]]
name = "Test"

9
tests/lake/tests/ltar/test.sh
View file

@ -45,6 +45,15 @@ test_exp -f .lake/build/ir/Test.ltar
rm -rf .lake/build .lake/cache/artifacts/*.[!l]*
test_out "leantar" build +Test --no-build -v
# Test caching an `ltar` through `-o` (with `restoreAllArtifacts = true`)
# This tests caching the ltar from within `Module.packLtar`
rm -rf .lake/cache .lake/build
test_run -f restoreAll.toml build +Test -v --wfail
test_exp ! -f .lake/build/ir/Test.ltar
test_run -f restoreAll.toml build +Test -v --wfail -o .lake/outputs.jsonl
test_cmd ls .lake/cache/artifacts/*.ltar
test_exp -f .lake/build/ir/Test.ltar
# Test producing an `ltar` without already restored artifacts
rm -rf .lake/cache .lake/build
LAKE_ARTIFACT_CACHE=true test_run build +Test -v