ci: extract install-cvc5, install-z3, restore-lake-cache into composite actions by tautschnig · Pull Request #1137 · strata-org/Strata

tautschnig · 2026-05-07T11:29:23Z

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:

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).

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

…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>

Copilot

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, and restore-lake-cache.
Updated .github/workflows/ci.yml and .github/workflows/cbmc.yml to 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>

…i-workflows

shigoel

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>

shigoel

Clean refactoring that eliminates ~108 lines of duplicated CI shell and introduces well-parameterized composite actions. Notably fixes a latent bug where ci.yml used arm64-win as the z3 archive name on aarch64 instead of the correct arm64-glibc-2.34. The use-restore-keys design on restore-lake-cache is a nice touch for preserving the #952 safety net. LGTM.

atomb

Code Review: PR #1137 — Extract CI composite actions

Summary

Extracts duplicated shell blocks for installing cvc5, z3, and restoring the lake cache into three reusable composite actions under .github/actions/. Rewires ci.yml and cbmc.yml to use them. Net change: -108 lines of duplicated shell, +17 lines of action usage. Also fixes a latent bug where ci.yml used the wrong archive name (arm64-win instead of arm64-glibc-2.34) for z3 on aarch64.

Features

Fixes a real bug. The existing ci.yml downloads z3-4.15.2-arm64-glibc-2.34.zip but sets ARCHIVE_NAME="z3-4.15.2-arm64-win" — the subsequent unzip would fail on aarch64 runners. The consolidated action uses the correct name.
Well-designed input interface. install-to (path vs system) cleanly handles the two installation modes. fail-on-cache-miss and use-restore-keys on restore-lake-cache correctly model the two cache usage patterns (upstream builder vs downstream consumer).
Good documentation. Each action has a clear description explaining its purpose, provenance, and future adoption plans. The restore-lake-cache action documents the rationale for use-restore-keys with a link to #952.
Correct cache key pattern. Reproduces the exact same key structure and fallback hierarchy as the original inline blocks.
Appropriate scoping. The build_doc job's cache (different prefix, multiple paths, multiple toolchain files) is correctly left untouched.
set -eu in shell scripts. Stricter than the original inline scripts — failures will be caught immediately.

Potential Issues

See inline comments for the significant items. Minor items:

No cleanup of downloaded archives — zip files and extracted directories accumulate in $GITHUB_WORKSPACE (~50-100MB). Same as before, not a regression.
wget -q consistency — The new actions consistently use wget -q, which is an improvement but means less verbose error output if a download fails in build_and_test_lean.
Version pinning discoverability — Default versions are now in .github/actions/*/action.yml rather than the workflow files. A comment in the workflows pointing to where versions are configured would help.
build_python z3 version skew — Uses z3 4.13.4 (pip) while other jobs use 4.15.2 (GitHub release). Not introduced by this PR, just noting.
python-fuzz.yml not yet converted — Consider whether to do it here or track as follow-up.

atomb

My agent's review above highlights some potential future improvements (mostly to things this PR didn't introduce), but I don't think any are blocking.

Two follow-ups consolidating the lake cache save/restore key shape and tightening the use-restore-keys input contract: 1. Add a save-lake-cache companion action that mirrors the restore-lake-cache key construction, and switch the build_and_test_lean Save lake cache step in ci.yml to use it. Both reviewers flagged the same drift risk: the consolidated restore action owned the key pattern, but the save step still had the key spelled out inline, so a future edit could easily desync the two and silently break the downstream jobs that read the cache with fail-on-cache-miss: "true" + use-restore-keys: "false". The two actions are now a single source of truth for the "lake-...-${{ github.sha }}" pattern. The unrelated build_docs_verso save step (different "docs-" prefix and multi-path) is left alone — separate flow, out of scope. 2. Tighten the use-restore-keys input description in restore-lake-cache to spell out that the value must be the string "true" or "false" (per atomb), so the YAML-string-vs-boolean caveat is documented at the input itself rather than implied by the internal "if" predicates. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…i-workflows

tautschnig requested review from a team and Copilot May 7, 2026 11:29

github-actions Bot added github_actions Pull requests that update GitHub Actions code Waiting-For-Review labels May 7, 2026

Copilot started reviewing on behalf of tautschnig May 7, 2026 11:30 View session

tautschnig mentioned this pull request May 7, 2026

Add hypothesmith-based fuzz testing for Python front-end #984

Open

Copilot AI reviewed May 7, 2026

View reviewed changes

Comment thread .github/actions/restore-lake-cache/action.yml Outdated

Comment thread .github/actions/restore-lake-cache/action.yml Outdated

Comment thread .github/actions/install-cvc5/action.yml Outdated

tautschnig and others added 2 commits May 15, 2026 22:29

Merge remote-tracking branch 'origin/main' into tautschnig/reusable-c…

53fec53

…i-workflows

shigoel reviewed May 15, 2026

View reviewed changes

Comment thread .github/actions/restore-lake-cache/action.yml

shigoel assigned tautschnig May 15, 2026

tautschnig assigned shigoel and unassigned tautschnig May 18, 2026

shigoel enabled auto-merge May 18, 2026 15:55

shigoel previously approved these changes May 18, 2026

View reviewed changes

github-actions Bot added Has 1 approval and removed Waiting-For-Review labels May 18, 2026

aqjune-aws reviewed May 18, 2026

View reviewed changes

Comment thread .github/workflows/ci.yml Outdated

atomb reviewed May 18, 2026

View reviewed changes

Comment thread .github/actions/restore-lake-cache/action.yml

atomb reviewed May 18, 2026

View reviewed changes

Comment thread .github/workflows/ci.yml

atomb previously approved these changes May 18, 2026

View reviewed changes

github-actions Bot removed the Has 1 approval label May 18, 2026

tautschnig and others added 2 commits May 19, 2026 08:40

Merge remote-tracking branch 'origin/main' into tautschnig/reusable-c…

7885311

…i-workflows

tautschnig dismissed stale reviews from atomb and shigoel via 7885311 May 19, 2026 08:46

github-actions Bot added the Waiting-For-Review label May 19, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

ci: extract install-cvc5, install-z3, restore-lake-cache into composite actions#1137

ci: extract install-cvc5, install-z3, restore-lake-cache into composite actions#1137
tautschnig wants to merge 6 commits into
mainfrom
tautschnig/reusable-ci-workflows

tautschnig commented May 7, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

shigoel left a comment

Uh oh!

Uh oh!

shigoel left a comment

Uh oh!

Uh oh!

atomb left a comment

Uh oh!

Uh oh!

Uh oh!

atomb left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

tautschnig commented May 7, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

shigoel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

shigoel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

atomb left a comment

Choose a reason for hiding this comment

Code Review: PR #1137 — Extract CI composite actions

Summary

Features

Potential Issues

Uh oh!

Uh oh!

Uh oh!

atomb left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants