Skip to content

fix: make local artifact sharing safe across workspaces - #16301

Open
kim-em wants to merge 7 commits into
masterfrom
machine-lake-cache
Open

kim-em wants to merge 7 commits into
masterfrom
machine-lake-cache

Conversation

@kim-em

@kim-em kim-em commented Nov 6, 2026 •

Copy link
Copy Markdown
Collaborator

This PR makes Lake's local artifact cache safe to share between cooperating workspaces and adds an opt-in shared store with private fallback for unsupported invocations.

Artifacts are validated in invocation-unique temporary files before publication, output and revision metadata is replaced as complete files, and builds recover from cache entries disappearing during restoration or archive unpacking. Existing private-cache behavior and cached project configuration layouts are preserved.

LAKE_SHARED_CACHE_ROOT selects a toolchain-scoped namespace only for supported release installations with restored outputs and working hard links on the workspace filesystem. LAKE_CACHE_DIR remains the private fallback exported to child invocations, so older Lake binaries keep using private storage. Explicit private overrides remain effective. This adds no retention limits or work admission policy.

The integration tests exercise paused and overlapping HTTP downloads, killed publishers, controlled partial binary/text copies, extra download destinations in cold and warm stores, concurrent metadata publication, cross-workspace reuse and rebuild isolation, cached configuration alternation with stock Lake, executable permissions, archive overwrite isolation, and controlled artifact/store removal during restoration and unpacking. Existing cache and transfer fixtures cover private operation. The full Linux build and test suite passes in CI.

This PR publishes complete cache artifacts and mappings atomically, restores or rebuilds after eviction, and lets compatible executables select a shared local store while retaining a private fallback for older executables.
This PR reserves sibling temporary files with process and monotonic-clock identifiers, retaining exclusive creation and collision retry without requiring a system entropy source.
@kim-em kim-em added the changelog-lake Lake label Nov 6, 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 Nov 6, 2026
@kim-em
kim-em marked this pull request as ready for review November 6, 2026 05:20
@kim-em
kim-em requested a review from tydeu as a code owner November 6, 2026 05:20

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-lake Lake 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.

1 participant