Skip to content

Commit 7ca0b5e

Browse files
dicethedevpablodeymo
dicethedev
and
pablodeymo
authored
ci: download latest leanSpec fixture release instead of generating fixtures (#385)
## 🗒️ 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: - CI performance - fixture consistency - workflow simplicity - alignment with released leanSpec vectors It also removes the overhead and complexity of generating fixtures during CI runs. --- ## What Changed ### `ci.yml` - Removed: - leanSpec checkout step - fixture generation steps - Added: - latest release SHA fetch step - fixture cache restore keyed by release SHA - download of `fixtures-prod-scheme.tar.gz` - SHA256 verification - extraction into `leanSpec/fixtures` --- ### `Makefile` Updated the `leanSpec/fixtures` target: - Removed: - `uv run fill ...` fixture generation flow - Added: - release download - SHA verification - extraction workflow --- ## `CLAUDE.md` Updated development documentation to reflect the new fixture workflow: - fixtures are now downloaded from released leanSpec assets - local development no longer regenerates fixtures directly --- ## Correctness / Behavior Guarantees ### Preserved Invariants - Existing test paths still use `leanSpec/fixtures` - `make test` behavior remains unchanged - Test harness logic remains unchanged ### Behavior Changes - CI now consumes published leanSpec release fixtures - Fixture cache invalidation now occurs when the release SHA changes ### Reviewer Notes - No runtime or product behavior changes - Changes are limited to: - CI fixture acquisition - local `make leanSpec/fixtures` workflow --- ## Tests Added / Run No new unit or integration tests were added. ### Verification Performed - `make -n leanSpec/fixtures` - validated updated Makefile target expansion - Parsed `ci.yml` - validated YAML structure using Python --- ## Related Issues / PRs - Closes #376 ## ✅ Verification Checklist - [x] Ran `make fmt` — clean - [x] Ran `make lint` (`clippy -D warnings`) — clean - [x] Ran `cargo test --workspace --release` — all passing --------- Co-authored-by: Pablo Deymonnaz <pdeymon@fi.uba.ar>
1 parent 0062339 commit 7ca0b5e

3 files changed

Lines changed: 56 additions & 92 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 37 additions & 81 deletions
Original file line numberDiff line numberDiff line change
@@ -47,100 +47,56 @@ jobs:
4747
steps:
4848
- uses: actions/checkout@v6
4949

50-
# Read the pinned leanSpec commit from the Makefile (single source of truth)
51-
- name: Get leanSpec pinned commit
52-
id: lean-spec
53-
run: echo "commit=$(sed -n 's/^LEAN_SPEC_COMMIT_HASH:= *//p' Makefile)" >> $GITHUB_OUTPUT
50+
- name: Get leanSpec fixtures release info
51+
id: fixtures-release
52+
run: |
53+
api_url="https://api.github.com/repos/leanEthereum/leanSpec/releases/latest"
54+
json=$(curl -sL "$api_url")
55+
fixtures_url=$(echo "$json" | python3 -c "import sys,json; j=json.load(sys.stdin); print(next(a.get('browser_download_url') for a in j.get('assets',[]) if a.get('name')=='fixtures-prod-scheme.tar.gz'))")
56+
sha_url=$(echo "$json" | python3 -c "import sys,json; j=json.load(sys.stdin); print(next(a.get('browser_download_url') for a in j.get('assets',[]) if a.get('name')=='fixtures-prod-scheme.tar.gz.sha256'))")
57+
sha=$(curl -sL "$sha_url" | cut -d' ' -f1)
58+
{
59+
echo "url=$fixtures_url"
60+
echo "sha_url=$sha_url"
61+
echo "sha=$sha"
62+
} >> $GITHUB_OUTPUT
5463
5564
- name: Restore test fixtures cache
5665
id: cache-fixtures
5766
uses: actions/cache/restore@v5
5867
with:
5968
path: leanSpec/fixtures
60-
key: leanspec-fixtures-${{ steps.lean-spec.outputs.commit }}
61-
62-
# All fixture generation steps are skipped when the cache hits
63-
- name: Checkout leanSpec at pinned commit
64-
if: steps.cache-fixtures.outputs.cache-hit != 'true'
65-
uses: actions/checkout@v6
66-
with:
67-
repository: leanEthereum/leanSpec
68-
ref: ${{ steps.lean-spec.outputs.commit }}
69-
path: leanSpec
70-
71-
- name: Install uv and Python 3.14
72-
if: steps.cache-fixtures.outputs.cache-hit != 'true'
73-
uses: astral-sh/setup-uv@v4
74-
with:
75-
enable-cache: true
76-
cache-dependency-glob: "leanSpec/pyproject.toml"
77-
python-version: "3.14"
78-
79-
- name: Sync leanSpec dependencies
80-
if: steps.cache-fixtures.outputs.cache-hit != 'true'
81-
working-directory: leanSpec
82-
run: uv sync --no-progress
69+
key: leanspec-fixtures-${{ steps.fixtures-release.outputs.sha }}
8370

84-
- name: Get production keys URL hash
71+
- name: Download leanSpec fixtures release
72+
id: download-fixtures
8573
if: steps.cache-fixtures.outputs.cache-hit != 'true'
86-
id: prod-keys-url
87-
working-directory: leanSpec
8874
run: |
89-
URL=$(uv run python -c "from consensus_testing.keys import KEY_DOWNLOAD_URLS; print(KEY_DOWNLOAD_URLS['prod'])")
90-
HASH=$(echo -n "$URL" | sha256sum | awk '{print $1}')
91-
echo "hash=$HASH" >> $GITHUB_OUTPUT
92-
93-
- name: Restore production keys cache
94-
if: steps.cache-fixtures.outputs.cache-hit != 'true'
95-
id: cache-prod-keys
96-
uses: actions/cache/restore@v5
97-
with:
98-
path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme
99-
key: prod-keys-${{ steps.prod-keys-url.outputs.hash }}
100-
101-
- name: Download production keys
102-
if: steps.cache-fixtures.outputs.cache-hit != 'true' && steps.cache-prod-keys.outputs.cache-hit != 'true'
103-
working-directory: leanSpec
104-
run: uv run python -m consensus_testing.keys --download --scheme prod
105-
106-
# Save production keys even if a later step fails, so a re-run does
107-
# not have to re-download. See: https://github.com/actions/cache/tree/main/save#always-save-cache
108-
#
109-
# `cache-hit == 'false'` (rather than `!= 'true'`) only matches when
110-
# the restore step actually ran and missed: when fixtures were already
111-
# cached, the restore was skipped and `cache-hit` is empty, so save
112-
# is skipped too.
113-
- name: Save production keys cache
114-
if: always() && steps.cache-prod-keys.outputs.cache-hit == 'false'
115-
uses: actions/cache/save@v5
116-
with:
117-
path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme
118-
key: ${{ steps.cache-prod-keys.outputs.cache-primary-key }}
119-
120-
# `-n 1` (not `-n auto`) runs a single leanVM prover at a time. The
121-
# devnet5 prover peaks at ~12 GiB per proof (measured), so more workers
122-
# blow past the 4-vCPU/16 GiB runner's RAM: `-n auto` (4 provers) hard
123-
# OOM-killed the runner, `-n 2` thrashed and lost its heartbeat so GitHub
124-
# cancelled the job. One prover peaks ~12.4 GiB with 0 swap and completes
125-
# in ~2h36m. The Makefile keeps `-n auto` for local machines with more RAM.
126-
- name: Generate test fixtures
127-
id: generate-fixtures
128-
if: steps.cache-fixtures.outputs.cache-hit != 'true'
129-
working-directory: leanSpec
130-
run: uv run fill --fork Lstar -n 1 --scheme prod -o fixtures
131-
132-
# Save fixtures only when generation actually SUCCEEDED. A bare
133-
# `always()` here previously saved the (empty) fixtures dir when
134-
# generation was cancelled or OOM-killed mid-run, poisoning the cache:
135-
# later runs hit the empty cache, skipped generation, and the Rust tests
136-
# failed with no fixtures. Gating on the generate step's outcome keeps
137-
# the "save even if the later Rust test step fails" intent without ever
138-
# persisting a partial fixture set.
75+
tmpdir=$(mktemp -d)
76+
trap 'rm -rf "$tmpdir"' EXIT
77+
fixtures_url="${{ steps.fixtures-release.outputs.url }}"
78+
sha_url="${{ steps.fixtures-release.outputs.sha_url }}"
79+
echo "Downloading fixtures from $fixtures_url"
80+
curl -L -f -o "$tmpdir/fixtures-prod-scheme.tar.gz" "$fixtures_url"
81+
curl -L -f -o "$tmpdir/fixtures-prod-scheme.tar.gz.sha256" "$sha_url"
82+
expected=$(cut -d' ' -f1 "$tmpdir/fixtures-prod-scheme.tar.gz.sha256")
83+
actual=$(sha256sum "$tmpdir/fixtures-prod-scheme.tar.gz" | awk '{print $1}')
84+
if [ "$expected" != "$actual" ]; then
85+
echo "SHA256 mismatch: expected $expected, got $actual"
86+
exit 1
87+
fi
88+
rm -rf leanSpec/fixtures
89+
mkdir -p leanSpec/fixtures
90+
tar -xzf "$tmpdir/fixtures-prod-scheme.tar.gz" -C leanSpec/fixtures --strip-components=1
91+
92+
# Save fixtures only when the download actually SUCCEEDED, so a
93+
# cancelled or failed download never persists a partial fixture set,
94+
# while still saving even if the later Rust test step fails.
13995
- name: Save test fixtures cache
14096
if: >-
14197
always()
14298
&& steps.cache-fixtures.outputs.cache-hit != 'true'
143-
&& steps.generate-fixtures.outcome == 'success'
99+
&& steps.download-fixtures.outcome == 'success'
144100
uses: actions/cache/save@v5
145101
with:
146102
path: leanSpec/fixtures

‎CLAUDE.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ Not to be confused with Ethereum consensus clients AKA Beacon Chain clients AKA
77

88
**Main branch:** `main`
99
**Rust version:** 1.92.0 (edition 2024)
10-
**Test fixtures commit:** Check `LEAN_SPEC_COMMIT_HASH` in Makefile
10+
**Test fixtures release:** Download latest production fixtures from leanSpec releases
1111

1212
## Codebase Structure (10 crates)
1313

@@ -81,7 +81,7 @@ make test # All tests + forkchoice spec tests
8181
### Common Operations
8282
```bash
8383
.claude/skills/test-pr-devnet/scripts/test-branch.sh # Test branch in multi-client devnet
84-
rm -rf leanSpec && make leanSpec/fixtures # Regenerate test fixtures (requires uv)
84+
rm -rf leanSpec && make leanSpec/fixtures # Download latest released test fixtures
8585
make docker-build # Build Docker image (DOCKER_TAG=local)
8686
make run-devnet # Run local devnet with lean-quickstart
8787
```

‎Makefile‎

Lines changed: 17 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -38,15 +38,23 @@ shadow-docker-build: ## 👻🐳 Build a Shadow-compatible Docker image
3838
-t ghcr.io/lambdaclass/ethlambda:$(DOCKER_TAG)-shadow .
3939
@echo
4040

41-
# 2026-06-03
42-
LEAN_SPEC_COMMIT_HASH:=30ffb6cab54ca6d2e2e1c82e8e2713ebb9a8fa3f
43-
44-
leanSpec:
45-
git clone https://github.com/leanEthereum/leanSpec.git --single-branch
46-
cd leanSpec && git checkout $(LEAN_SPEC_COMMIT_HASH)
47-
48-
leanSpec/fixtures: leanSpec
49-
cd leanSpec && uv run fill --fork Lstar -n auto --scheme prod -o fixtures
41+
LEAN_SPEC_FIXTURES_URL ?= https://github.com/leanEthereum/leanSpec/releases/latest/download/fixtures-prod-scheme.tar.gz
42+
LEAN_SPEC_FIXTURES_SHA_URL ?= $(LEAN_SPEC_FIXTURES_URL).sha256
43+
44+
leanSpec/fixtures:
45+
tmpdir=$$(mktemp -d); \
46+
trap 'rm -rf "$$tmpdir"' EXIT; \
47+
curl -L -f -o "$$tmpdir/fixtures-prod-scheme.tar.gz" "$(LEAN_SPEC_FIXTURES_URL)"; \
48+
curl -L -f -o "$$tmpdir/fixtures-prod-scheme.tar.gz.sha256" "$(LEAN_SPEC_FIXTURES_SHA_URL)"; \
49+
expected=$$(cut -d' ' -f1 "$$tmpdir/fixtures-prod-scheme.tar.gz.sha256"); \
50+
actual=$$(sha256sum "$$tmpdir/fixtures-prod-scheme.tar.gz" | awk '{print $$1}'); \
51+
if [ "$$expected" != "$$actual" ]; then \
52+
echo "SHA256 mismatch: expected $$expected, got $$actual" >&2; \
53+
exit 1; \
54+
fi; \
55+
rm -rf leanSpec/fixtures; \
56+
mkdir -p leanSpec/fixtures; \
57+
tar -xzf "$$tmpdir/fixtures-prod-scheme.tar.gz" -C leanSpec/fixtures --strip-components=1
5058

5159
lean-quickstart:
5260
git clone https://github.com/blockblaz/lean-quickstart.git --depth 1 --single-branch

0 commit comments

Comments
 (0)