Skip to content

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

Merged
tydeu merged 1 commit intoleanprover:masterfrom
tydeu:lake/fix-cache-ltar-restore
Mar 19, 2026
Merged

fix: lake: ltar caching bug with build -o#12993
tydeu merged 1 commit intoleanprover:masterfrom
tydeu:lake/fix-cache-ltar-restore

Conversation

@tydeu
Copy link
Copy Markdown
Member

@tydeu tydeu commented Mar 19, 2026

This PR fixes a bug with Lake where caching an ltar produced via lake build -o would fail if restoreAllArtifacts was also true.

@tydeu tydeu added changelog-lake Lake lake-ci Run all Lake tests labels Mar 19, 2026
@tydeu tydeu force-pushed the lake/fix-cache-ltar-restore branch from 99002ea to a18efae Compare March 19, 2026 22:00
@tydeu tydeu added this pull request to the merge queue Mar 19, 2026
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 19, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1b63e7dfc6d95cbd608d700ccbac567f2c040ce2 --onto 61a3443a9569d548a235f785b9a33984bb7ff622. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-19 22:56:02)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1b63e7dfc6d95cbd608d700ccbac567f2c040ce2 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-19 22:56:04)

Merged via the queue into leanprover:master with commit d78525b Mar 19, 2026
19 checks passed
@tydeu tydeu deleted the lake/fix-cache-ltar-restore branch March 19, 2026 23:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-lake Lake lake-ci Run all Lake tests toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants