Skip to content

[anneal] Audit cached Lean artifacts against clean builds#3486

Open
mdittmer wants to merge 1 commit into
Gcz4iteion3frenivdjpngxluv7c3bshffrom
Gri3qjmi3mkxqhujr7xw3insogx5mpcm4
Open

[anneal] Audit cached Lean artifacts against clean builds#3486
mdittmer wants to merge 1 commit into
Gcz4iteion3frenivdjpngxluv7c3bshffrom
Gri3qjmi3mkxqhujr7xw3insogx5mpcm4

Conversation

@mdittmer

@mdittmer mdittmer commented Jul 13, 2026

Copy link
Copy Markdown
Collaborator

Split the Nix pipeline at a shared, path-rewritten source tree. Keep the default fast path cache-seeded with one trace traversal, and add a seed-free Lean build whose packaged output passes through the same pruning and archive finalizers.

Compare complete source, toolchain, and Lake build payloads, including raw ILean reference usages, hash sidecars, and stable trace dependency/output hashes. Regenerate the two stale candidate ILean files exposed by that audit, install both archives independently, and compare the complete normalized InfoView setup contract in isolated environments.

Run the clean reference build and equivalence checks in a standalone nightly workflow on main so ordinary push and pull-request jobs retain the fast path.


⬇️ Download this PR

Branch

git fetch origin refs/heads/Gri3qjmi3mkxqhujr7xw3insogx5mpcm4 && git checkout -b pr-Gri3qjmi3mkxqhujr7xw3insogx5mpcm4 FETCH_HEAD

Checkout

git fetch origin refs/heads/Gri3qjmi3mkxqhujr7xw3insogx5mpcm4 && git checkout FETCH_HEAD

Cherry Pick

git fetch origin refs/heads/Gri3qjmi3mkxqhujr7xw3insogx5mpcm4 && git cherry-pick FETCH_HEAD

Pull

git pull origin refs/heads/Gri3qjmi3mkxqhujr7xw3insogx5mpcm4

Stacked PRs enabled by GHerrit.

Split the Nix pipeline at a shared, path-rewritten source tree. Keep the default fast path cache-seeded with one trace traversal, and add a seed-free Lean build whose packaged output passes through the same pruning and archive finalizers.

Compare complete source, toolchain, and Lake build payloads, including raw ILean reference usages, hash sidecars, and stable trace dependency/output hashes. Regenerate the two stale candidate ILean files exposed by that audit, install both archives independently, and compare the complete normalized InfoView setup contract in isolated environments.

Run the clean reference build and equivalence checks in a standalone nightly workflow on main so ordinary push and pull-request jobs retain the fast path.

gherrit-pr-id: Gri3qjmi3mkxqhujr7xw3insogx5mpcm4
@codecov-commenter

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 91.85%. Comparing base (0c8cf6a) to head (c88afa3).

Additional details and impacted files
@@                        Coverage Diff                         @@
##           Gcz4iteion3frenivdjpngxluv7c3bshf    #3486   +/-   ##
==================================================================
  Coverage                              91.85%   91.85%           
==================================================================
  Files                                     20       20           
  Lines                                   6093     6093           
==================================================================
  Hits                                    5597     5597           
  Misses                                   496      496           

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants