perf: optimize CI pipeline: caching, artifact sharing, and fixture reuse

[guha-rahul]

This pr

• Upgrade cache actions from v3 to v4
• Add LeanSpec fixtures caching to skip regeneration when unchanged
  tracks figure and fix the CI long CI runs #385

[Copilot]

Pull request overview

Optimizes GitHub Actions CI runtime by upgrading caching infrastructure and adding fixture reuse to avoid regenerating LeanSpec fixtures when inputs haven’t changed.

Changes:

• Upgraded actions/cache usage from v3 to v4 across workflows.
• Added a new cache for leanSpec/fixtures and conditionally skipped fixture generation on cache hits (CI workflow).

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File	Description
.github/workflows/risc0.yml	Upgrades Zig package caching action to actions/cache@v4.
.github/workflows/ci.yml	Upgrades Zig cache to v4 and adds LeanSpec fixtures caching + conditional fixture generation.
.github/workflows/auto-release.yml	Upgrades Zig package caching action to actions/cache@v4.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 3 out of 3 changed files in this pull request and generated no new comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 1 out of 1 changed files in this pull request and generated 1 comment.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

restore-keys is likely counterproductive here: if the primary key doesn’t match, cache-hit will be false and the next step runs uv run fill --clean, which will delete the restored leanSpec/fixtures anyway. This can add time by downloading a large stale cache only to immediately wipe it. Consider removing restore-keys (or dropping --clean if the intent is to reuse partial restores).

Suggested change

	restore-keys: |
	${{ runner.os }}-leanspec-

[Copilot]

Copilot was unable to review this pull request because the user who requested the review is ineligible. To be eligible to request a review, you need a paid Copilot license, or your organization must enable Copilot code review.

[Copilot]

Pull request overview

Copilot reviewed 1 out of 1 changed files in this pull request and generated 2 comments.

Comments suppressed due to low confidence (2)

.github/workflows/ci.yml:152

• build now depends on deps, but deps is a matrix job (ubuntu + macos). In GitHub Actions, a matrix job ID in needs gates on all matrix runs, so each build matrix run will wait for both deps OS runs to finish. This increases the critical path and couples the OS lanes. Consider either removing the needs edge (rely on cross-run caches), or splitting deps into separate job IDs per OS so each lane only waits for its own warmup.

  build:
    needs: deps
    runs-on: ${{ matrix.os }}
    strategy:
      matrix:
        os: [ubuntu-latest, macos-latest]

.github/workflows/ci.yml:297

• test now depends on deps, but since deps is a matrix job, needs: deps will make each test matrix run wait for all deps matrix runs (both OSes). This likely increases overall wall-clock time and reduces parallelism. Suggest removing this dependency or restructuring deps into per-OS job IDs to avoid cross-OS gating.

  test:
    name: test
    needs: deps
    runs-on: ${{ matrix.os }}
    strategy:
      matrix:
        os: [ubuntu-latest, macos-latest]

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

dummy-prove now depends on deps, but because deps is a matrix job, this will gate each dummy-prove matrix run on completion of both deps OS runs. That reduces concurrency and can lengthen the pipeline. Consider dropping the dependency or splitting deps into per-OS jobs so each lane only waits on its matching warmup.

Suggested change

needs: deps

[Copilot]

The LeanSpec fixtures cache key is based on hashFiles('.gitmodules'), which won't change when the leanSpec submodule revision changes. Once a cache entry exists for this key, future updates to LeanSpec (or to the fixture generation logic) can keep reusing stale fixtures and also won't be able to save an updated cache under the same key. Use a key that tracks the LeanSpec revision/inputs (e.g., hash relevant files under leanSpec/ like its lockfile/scripts, or otherwise incorporate the submodule commit) so the cache invalidates correctly.

Suggested change

	key: ${{ runner.os }}-leanspec-${{ hashFiles('.gitmodules') }}
	key: ${{ runner.os }}-leanspec-${{ hashFiles('leanSpec/**') }}