chore: bump leanVM to 8fcbd779 and leanSpec to latest main #1403
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: CI | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| branches: ["**"] | |
| workflow_dispatch: | |
| # Cancel in-progress runs when a new commit is pushed to the same PR or branch | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} | |
| cancel-in-progress: true | |
| env: | |
| CARGO_NET_GIT_FETCH_WITH_CLI: "true" | |
| CARGO_NET_RETRY: "10" | |
| jobs: | |
| lint: | |
| name: Lint | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - name: Setup Rust | |
| uses: dtolnay/rust-toolchain@master | |
| with: | |
| toolchain: "1.92.0" | |
| components: rustfmt, clippy | |
| - name: Setup cache | |
| uses: Swatinem/rust-cache@v2 | |
| - name: Check formatting | |
| run: cargo fmt --all -- --check | |
| - name: Cargo check | |
| run: cargo check --workspace --all-targets | |
| - name: Clippy | |
| run: cargo clippy --workspace --all-targets -- -D warnings | |
| test: | |
| name: Test | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v6 | |
| # Read the pinned leanSpec commit from the Makefile (single source of truth) | |
| - name: Get leanSpec pinned commit | |
| id: lean-spec | |
| run: echo "commit=$(sed -n 's/^LEAN_SPEC_COMMIT_HASH:= *//p' Makefile)" >> $GITHUB_OUTPUT | |
| - name: Restore test fixtures cache | |
| id: cache-fixtures | |
| uses: actions/cache/restore@v5 | |
| with: | |
| path: leanSpec/fixtures | |
| key: leanspec-fixtures-${{ steps.lean-spec.outputs.commit }} | |
| # All fixture generation steps are skipped when the cache hits | |
| - name: Checkout leanSpec at pinned commit | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| uses: actions/checkout@v6 | |
| with: | |
| repository: leanEthereum/leanSpec | |
| ref: ${{ steps.lean-spec.outputs.commit }} | |
| path: leanSpec | |
| - name: Install uv and Python 3.14 | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| uses: astral-sh/setup-uv@v4 | |
| with: | |
| enable-cache: true | |
| cache-dependency-glob: "leanSpec/pyproject.toml" | |
| python-version: "3.14" | |
| - name: Sync leanSpec dependencies | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| working-directory: leanSpec | |
| run: uv sync --no-progress | |
| - name: Get production keys URL hash | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| id: prod-keys-url | |
| working-directory: leanSpec | |
| run: | | |
| URL=$(uv run python -c "from consensus_testing.keys import KEY_DOWNLOAD_URLS; print(KEY_DOWNLOAD_URLS['prod'])") | |
| HASH=$(echo -n "$URL" | sha256sum | awk '{print $1}') | |
| echo "hash=$HASH" >> $GITHUB_OUTPUT | |
| - name: Restore production keys cache | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| id: cache-prod-keys | |
| uses: actions/cache/restore@v5 | |
| with: | |
| path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme | |
| key: prod-keys-${{ steps.prod-keys-url.outputs.hash }} | |
| - name: Download production keys | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' && steps.cache-prod-keys.outputs.cache-hit != 'true' | |
| working-directory: leanSpec | |
| run: uv run python -m consensus_testing.keys --download --scheme prod | |
| # Save production keys even if a later step fails, so a re-run does | |
| # not have to re-download. See: https://github.com/actions/cache/tree/main/save#always-save-cache | |
| # | |
| # `cache-hit == 'false'` (rather than `!= 'true'`) only matches when | |
| # the restore step actually ran and missed: when fixtures were already | |
| # cached, the restore was skipped and `cache-hit` is empty, so save | |
| # is skipped too. | |
| - name: Save production keys cache | |
| if: always() && steps.cache-prod-keys.outputs.cache-hit == 'false' | |
| uses: actions/cache/save@v5 | |
| with: | |
| path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme | |
| key: ${{ steps.cache-prod-keys.outputs.cache-primary-key }} | |
| # `-n 1` (not `-n auto`) runs a single leanVM prover at a time. The | |
| # devnet5 prover peaks at ~4-5 GiB per proof; more workers multiply that | |
| # past the 4-vCPU/16 GiB runner's RAM. `-n auto` (4 provers) OOM-killed | |
| # the runner outright; `-n 2` (2 provers) thrashed and lost its heartbeat | |
| # mid-generation, so GitHub cancelled the job. One prover (~4.5 GiB) | |
| # should stay responsive. The Makefile keeps `-n auto` for local machines. | |
| # | |
| # The background sampler logs RAM/swap every 15s so we can confirm memory | |
| # is the cause and tune the worker count. Remove once generation is green. | |
| - name: Generate test fixtures | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| working-directory: leanSpec | |
| run: | | |
| ( while true; do | |
| echo "[mem $(date -u +%H:%M:%S)] $(free -m | awk 'NR==2{m=sprintf("mem_used=%sMiB avail=%sMiB",$3,$7)} NR==3{s=sprintf("swap_used=%sMiB",$3)} END{print m, s}')" | |
| sleep 15 | |
| done ) & | |
| MON=$! | |
| trap 'kill "$MON" 2>/dev/null' EXIT | |
| uv run fill --fork Lstar -n 1 --scheme prod -o fixtures | |
| # Save fixtures even if a later step fails, so a re-run does not | |
| # have to regenerate them. See: https://github.com/actions/cache/tree/main/save#always-save-cache | |
| - name: Save test fixtures cache | |
| if: always() && steps.cache-fixtures.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@v5 | |
| with: | |
| path: leanSpec/fixtures | |
| key: ${{ steps.cache-fixtures.outputs.cache-primary-key }} | |
| # Ensure make sees fixtures as up-to-date (its timestamp must be | |
| # newer than leanSpec/, which intermediate steps may have modified). | |
| - name: Mark fixtures as up-to-date | |
| run: touch leanSpec/fixtures | |
| - name: Setup Rust | |
| uses: dtolnay/rust-toolchain@master | |
| with: | |
| toolchain: "1.92.0" | |
| - name: Setup cache | |
| uses: Swatinem/rust-cache@v2 | |
| - name: Run tests | |
| run: make test |