Skip to content

fix: preserve restored Lake archives for output tracking - #15189

Draft
kim-em wants to merge 2 commits into
masterfrom
lake-reuse-cached-archives
Draft

kim-em wants to merge 2 commits into
masterfrom
lake-reuse-cached-archives

Conversation

@kim-em

@kim-em kim-em commented Sep 16, 2026

Copy link
Copy Markdown
Collaborator

This PR preserves downloaded module archives so lake build -o reuses them instead of recompressing identical outputs. It also preserves their platform-independence flag.

TauCeti’s sandboxed build, step 28, log line 5635 starts lake build --no-build -o .lake/outputs.jsonl at 07:42:40.943 and finishes at 07:46:33.754: 3m53s. The measured local improvement is 277s to 5.7s, with all 5,455 mappings unchanged.

By default, archive retention uses hard links; if unavailable, it skips retention without copying. LAKE_COPY_CACHE_ARCHIVES=true explicitly enables the copy fallback, independently of restoreAllArtifacts.

Tests cover archive reuse, actual cross-filesystem hard-link failures, copy opt-in, read-only caches, platform-independent mappings, environment propagation, and source-change invalidation.

🤖 prepared with codex

This PR avoids recompressing module archives restored from the artifact cache when collecting build outputs.
@kim-em kim-em added the changelog-lake Lake label Sep 16, 2026
@kim-em
kim-em requested a review from tydeu as a code owner September 16, 2026 22:52
@kim-em kim-em added the changelog-lake Lake label Sep 16, 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 Sep 16, 2026
@kim-em
kim-em marked this pull request as draft September 16, 2026 23:28
This PR retains cached archives through hard links by default and adds LAKE_COPY_CACHE_ARCHIVES to explicitly allow copying when hard links fail.
@kim-em

kim-em commented Sep 17, 2026

Copy link
Copy Markdown
Collaborator Author

We've deployed a TauCeti CI workaround: save the verified input-to-archive records before building, then hard-link unchanged archives before stock Lake generates the final mapping with --no-build --rehash -o. Reuse never copies archive payloads; failed links retain the existing packing path.

The deployed staging step reused 5,639 archives, then generated the mapping in 4.4s (01:13:50.213–01:13:54.619 UTC). CI, cache publication, and public readback all passed.

The workaround's code links here so we can remove it once our pinned Lean includes this fix or something similar.

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