ci: extract install-cvc5, install-z3, restore-lake-cache into composite actions#1137
Open
tautschnig wants to merge 4 commits into
Open
ci: extract install-cvc5, install-z3, restore-lake-cache into composite actions#1137tautschnig wants to merge 4 commits into
tautschnig wants to merge 4 commits into
Conversation
…te actions The same ~15-line blocks for installing cvc5, installing z3, and restoring the lake cache were duplicated across ci.yml's three jobs (build_and_test_lean, check_pending_python, build_python), cbmc.yml, and python-fuzz.yml. Robin asked for this to be consolidated as part of the #984 review (flagged non-blocking there, handled here). Introduce three composite actions under .github/actions/: - install-cvc5: downloads the static cvc5 release zip, makes the binary available either on $GITHUB_PATH ('path', default) or in /usr/local/bin ('system'). Version defaults to 1.2.1. - install-z3: same shape for z3, version defaults to 4.15.2. This fixes a latent bug: cbmc.yml and build_and_test_lean used different aarch64 archive names ('arm64-glibc-2.34' vs. 'arm64-win'); the consolidated action uses the correct glibc-2.34 one for both. - restore-lake-cache: wraps actions/cache/restore@v5 with the established key pattern lake-<os>-<arch>-<toolchain>-<manifest>-<all .st>-<sha> plus the three fallback keys dropping each trailing component. Exposes a 'fail-on-cache-miss' input for jobs that depend on a cache saved for the same SHA by build_and_test_lean. Rewire ci.yml and cbmc.yml to use the new actions: - ci.yml: build_and_test_lean: install-cvc5, install-z3, restore-lake-cache. check_pending_python: install-cvc5 (system), restore-lake-cache (fail-on-cache-miss: true). build_python: install-cvc5 (system), restore-lake-cache (fail-on-cache-miss: true). (The pip-based z3 install here is deliberately left as-is — it is a different install flow.) - cbmc.yml: install-cvc5, install-z3, restore-lake-cache (fail-on-cache-miss: true). Net change: -108 lines of duplicated shell, +17 lines of action usage across the two workflow files, with the reusable definitions ready to be adopted by python-fuzz.yml and any future workflows. actionlint reports no new warnings (the pre-existing save-always warning on cbmc.yml line 22 is unrelated). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
github-actions
Bot
added
github_actions
Contributor
There was a problem hiding this comment.
Pull request overview
This PR consolidates repeated CI workflow logic for installing SMT solvers (cvc5, z3) and restoring the Lean .lake cache by introducing reusable composite actions under .github/actions/, then rewiring the existing CI workflows to use them.
Changes:
- Added composite actions:
install-cvc5,install-z3, andrestore-lake-cache. - Updated
.github/workflows/ci.ymland.github/workflows/cbmc.ymlto call the new actions instead of duplicating shell blocks. - Standardized z3 aarch64 archive handling via the shared installer action.
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| .github/workflows/ci.yml | Replaces duplicated cvc5/z3 install and lake cache restore blocks with composite action usage across relevant jobs. |
| .github/workflows/cbmc.yml | Replaces duplicated cvc5/z3 install and lake cache restore blocks with composite action usage. |
| .github/actions/restore-lake-cache/action.yml | New composite action wrapping actions/cache/restore@v5 with the repo’s standard lake cache key pattern. |
| .github/actions/install-z3/action.yml | New composite action that downloads/unpacks z3 for x86_64/aarch64 and exposes it via PATH or /usr/local/bin. |
| .github/actions/install-cvc5/action.yml | New composite action that downloads/unpacks static cvc5 for x86_64/aarch64 and exposes it via PATH or /usr/local/bin. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Replace stale python-fuzz.yml references with anchors to #984 (which introduces python-fuzz.yml) and tighten the restore-lake-cache key-prefix input description so it no longer suggests the action can serve sub- projects with their own toolchain/manifest (the action hardcodes hashFiles('lean-toolchain') and hashFiles('lake-manifest.json') from the repo root). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
shigoel
reviewed
May 15, 2026
Contributor
shigoel
left a comment
shigoel
left a comment
There was a problem hiding this comment.
Nice cleanup — the z3 aarch64 bug fix is a good catch. One behavioral concern flagged inline.
…ty net The pre-PR ci.yml and cbmc.yml deliberately omitted restore-keys for jobs that used fail-on-cache-miss: true, so those jobs would only accept the exact-SHA cache saved upstream by build_and_test_lean (per the soundness argument in #952: stale .lake directories produce incorrect CI results because Lake doesn't track external state, so cross-SHA cache reuse is unsafe for jobs that depend on Python/cvc5). The consolidated action always emitted the three fallback keys, which silently broke the safety net: a stale prefix match would satisfy the restore step and fail-on-cache-miss would never trigger. Restore the original behaviour by adding a use-restore-keys input (default "true") to the action and gating the restore step into two if-branches, one with the three fallback keys and one with no restore-keys at all. The cache-hit output is the OR of the two branches' outputs. The three downstream callers (ci.yml's check_pending_python and build_python, plus cbmc.yml) now pass use-restore-keys: "false" alongside fail-on-cache-miss: "true". Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The same ~15-line blocks for installing cvc5, installing z3, and restoring the lake cache were duplicated across ci.yml's three jobs (build_and_test_lean, check_pending_python, build_python), cbmc.yml, and python-fuzz.yml. Robin asked for this to be consolidated as part of the #984 review (flagged non-blocking there, handled here).
Introduce three composite actions under .github/actions/:
install-cvc5: downloads the static cvc5 release zip, makes the binary available either on $GITHUB_PATH ('path', default) or in /usr/local/bin ('system'). Version defaults to 1.2.1.
install-z3: same shape for z3, version defaults to 4.15.2. This fixes a latent bug: cbmc.yml and build_and_test_lean used different aarch64 archive names ('arm64-glibc-2.34' vs. 'arm64-win'); the consolidated action uses the correct glibc-2.34 one for both.
restore-lake-cache: wraps actions/cache/restore@v5 with the established key pattern lake-----<all .st>- plus the three fallback keys dropping each trailing component. Exposes a 'fail-on-cache-miss' input for jobs that depend on a cache saved for the same SHA by build_and_test_lean.
Rewire ci.yml and cbmc.yml to use the new actions:
build_python: install-cvc5 (system), restore-lake-cache
(fail-on-cache-miss: true).
(The pip-based z3 install here is deliberately left as-is —
it is a different install flow.)
install-cvc5, install-z3, restore-lake-cache (fail-on-cache-miss: true).
Net change: -108 lines of duplicated shell, +17 lines of action usage across the two workflow files, with the reusable definitions ready to be adopted by python-fuzz.yml and any future workflows.
actionlint reports no new warnings (the pre-existing save-always warning on cbmc.yml line 22 is unrelated).
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.