ci: download latest leanSpec fixture release instead of generating fixtures#385
ci: download latest leanSpec fixture release instead of generating fixtures#385dicethedev wants to merge 2 commits into
Conversation
Greptile SummaryThis PR replaces in-CI fixture generation (checkout +
Confidence Score: 3/5Not safe to merge as-is: the Makefile SHA check silently passes on mismatch, and the CI cache-save logic can persist bad fixture state under a valid cache key. The Makefile's integrity check — the main new safety mechanism — does nothing on failure because Both
|
| Filename | Overview |
|---|---|
| .github/workflows/ci.yml | Replaces fixture generation with download-and-verify from leanSpec releases; SHA used for cache key is fetched separately from the one used during verification (TOCTOU risk), and the always() cache save can poison the cache if the download step fails. |
| Makefile | SHA integrity check on line 40 is a no-op because ; does not propagate failure — a tampered or corrupted archive is silently extracted; leanSpec target is now dead code with no prerequisite relationship to leanSpec/fixtures. |
| CLAUDE.md | Documentation updated to reflect that fixtures are now downloaded from releases rather than regenerated locally — straightforward and accurate. |
Comments Outside Diff (1)
-
.github/workflows/ci.yml, line 85-90 (link)Cache save with
always()can poison the cache on download failureThe save step runs under
always() && steps.cache-fixtures.outputs.cache-hit != 'true', meaning it fires even when the "Download leanSpec fixtures release" step fails (e.g. network error, SHA mismatch). At that pointleanSpec/fixtureseither doesn't exist or holds stale content, but the save stores it under the SHA-keyed cache entry. On the next run the cache key matches (the SHA file hasn't changed), the restore step reports a hit, the download is skipped, and tests run against empty or stale fixtures without any error about the fixture state. The old workflow usedcache-hit == 'false'specifically to avoid this. Consider gating the save on the download step succeeding.Prompt To Fix With AI
This is a comment left during a code review. Path: .github/workflows/ci.yml Line: 85-90 Comment: **Cache save with `always()` can poison the cache on download failure** The save step runs under `always() && steps.cache-fixtures.outputs.cache-hit != 'true'`, meaning it fires even when the "Download leanSpec fixtures release" step fails (e.g. network error, SHA mismatch). At that point `leanSpec/fixtures` either doesn't exist or holds stale content, but the save stores it under the SHA-keyed cache entry. On the next run the cache key matches (the SHA file hasn't changed), the restore step reports a hit, the download is skipped, and tests run against empty or stale fixtures without any error about the fixture state. The old workflow used `cache-hit == 'false'` specifically to avoid this. Consider gating the save on the download step succeeding. How can I resolve this? If you propose a fix, please make it concise.
Prompt To Fix All With AI
Fix the following 4 code review issues. Work through them one at a time, proposing concise fixes.
---
### Issue 1 of 4
Makefile:40-43
**SHA check doesn't abort on mismatch**
The test `[ "$$expected" = "$$actual" ]` on line 40 is followed by `;` rather than `||` or `&&`, so its exit status is thrown away. In Make, the entire recipe runs in a single shell, and `;` does not propagate failure — the subsequent `rm -rf`, `mkdir -p`, and `tar` commands execute unconditionally regardless of whether the check passes. A mismatched or actively tampered archive is silently extracted. The CI workflow correctly uses `if [ ... ]; then exit 1; fi` but this Makefile equivalent does nothing.
### Issue 2 of 4
.github/workflows/ci.yml:85-90
**Cache save with `always()` can poison the cache on download failure**
The save step runs under `always() && steps.cache-fixtures.outputs.cache-hit != 'true'`, meaning it fires even when the "Download leanSpec fixtures release" step fails (e.g. network error, SHA mismatch). At that point `leanSpec/fixtures` either doesn't exist or holds stale content, but the save stores it under the SHA-keyed cache entry. On the next run the cache key matches (the SHA file hasn't changed), the restore step reports a hit, the download is skipped, and tests run against empty or stale fixtures without any error about the fixture state. The old workflow used `cache-hit == 'false'` specifically to avoid this. Consider gating the save on the download step succeeding.
### Issue 3 of 4
.github/workflows/ci.yml:50-61
**TOCTOU between SHA fetch for cache key and actual download**
The SHA is fetched once in "Get leanSpec fixtures SHA" (to build the cache key) and then the `.sha256` file is fetched again inside "Download leanSpec fixtures release" for verification. If a new leanSpec release lands between these two steps, the cache key reflects the old SHA while the downloaded artifacts belong to the new release. The integrity check still passes (both files are self-consistent from the new release), but the fixtures are then saved under the old SHA key, which will never match on the next run, causing an unnecessary re-download every time a release ships during a CI run.
### Issue 4 of 4
Makefile:30-31
**`leanSpec` target is now dead code**
`leanSpec/fixtures` was updated to no longer depend on the `leanSpec` prerequisite, so the `leanSpec` clone target is never invoked by any downstream rule. The `git checkout` line was also dropped in this PR, leaving the target in a half-refactored state (it clones but doesn't pin a revision). If nothing depends on it, consider removing it to avoid confusion.
Reviews (1): Last reviewed commit: "ci: download latest leanSpec fixture rel..." | Re-trigger Greptile
| leanSpec: | ||
| git clone https://github.com/leanEthereum/leanSpec.git --single-branch |
There was a problem hiding this comment.
leanSpec target is now dead code
leanSpec/fixtures was updated to no longer depend on the leanSpec prerequisite, so the leanSpec clone target is never invoked by any downstream rule. The git checkout line was also dropped in this PR, leaving the target in a half-refactored state (it clones but doesn't pin a revision). If nothing depends on it, consider removing it to avoid confusion.
Prompt To Fix With AI
This is a comment left during a code review.
Path: Makefile
Line: 30-31
Comment:
**`leanSpec` target is now dead code**
`leanSpec/fixtures` was updated to no longer depend on the `leanSpec` prerequisite, so the `leanSpec` clone target is never invoked by any downstream rule. The `git checkout` line was also dropped in this PR, leaving the target in a half-refactored state (it clones but doesn't pin a revision). If nothing depends on it, consider removing it to avoid confusion.
How can I resolve this? If you propose a fix, please make it concise.|
We might want to wait for devnet 5 to be merged to merge this. Otherwise, we'll have devnet 4 code running devnet 5 tests |
LFG |
🗒️ Description / Motivation
This PR updates the CI and test fixture workflow so leanSpec fixtures are downloaded from the published leanSpec release assets instead of being generated in CI from a pinned checkout.
The repository now publishes the latest production fixtures as release assets, so CI should consume those directly rather than regenerating them.
This improves:
It also removes the overhead and complexity of generating fixtures during CI runs.
What Changed
ci.ymlRemoved:
Added:
fixtures-prod-scheme.tar.gzleanSpec/fixturesMakefileUpdated the
leanSpec/fixturestarget:uv run fill ...fixture generation flowCLAUDE.mdUpdated development documentation to reflect the new fixture workflow:
Correctness / Behavior Guarantees
Preserved Invariants
leanSpec/fixturesmake testbehavior remains unchangedBehavior Changes
Reviewer Notes
make leanSpec/fixturesworkflowTests Added / Run
No new unit or integration tests were added.
Verification Performed
make -n leanSpec/fixturesci.ymlRelated Issues / PRs
✅ Verification Checklist
make fmt— cleanmake lint(clippy -D warnings) — cleancargo test --workspace --release— all passing