CI: publish per-commit Verus releases, matching the cvc5 and z3 forks - #3
Merged
Conversation
build.yml already produces verus-arm64-macos.zip and verus-x86-linux.zip, but only as workflow artifacts. Those expire and need an authenticated API call to fetch, so nothing downstream can pin "the Verus built from commit X" the way verus-tools-mcp pins cvc5 and z3 against published binaries and hardcoded hashes. This adds basis-build.yml, which calls the existing build.yml and publishes its zips to a per-commit release tagged basis-<sha10> with sha256 sidecars and a SHA256SUMS roll-up. It mirrors the basis-build workflows on BasisResearch/cvc5 and BasisResearch/z3, including the delete-then-create so a re-run replaces its own release rather than failing. The assets are zips of the whole target-verus/release tree rather than bare binaries, since Verus needs vstd.vir and its libraries alongside the executable. That is the one way this differs from the solver forks. No change to build.yml, so the existing artifact flow and rolling-release keep working unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ms3PAGBHqqyGftGLY4xfcf
Branch protection requires a review this account cannot give, so the harness needs releases before the PR can merge. Adding ci/basis-build-publish to the push trigger lets the branch publish now. Builds from any ref other than main are marked --prerelease, so a release cut from an unmerged branch never claims "Latest" on the fork and the temporary state is visible rather than silent. Reverting is deleting one line from the trigger list; the prerelease branch then goes dead on its own once main is the only publishing ref. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ms3PAGBHqqyGftGLY4xfcf
naiimic
self-requested a review
September 3, 2026 22:38
naiimic
approved these changes
Sep 3, 2026
Author
|
Thanks @naiimic !!! |
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
2 participants
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.
Why
build.ymlalready buildsverus-arm64-macos.zipandverus-x86-linux.zip, but only as workflow artifacts. Artifacts expire and need an authenticated API call to fetch, so nothing downstream can pin the Verus built from commit X.verus-tools-mcppins cvc5 and z3 by downloading published release binaries and verifying them against hardcoded sha256 hashes. Verus has no equivalent, which leaves it the one unpinned component of the stack:resolve_verus_bin()falls back throughVERUS_BINto a checkout to bareveruson PATH, so two runs of the same MCP commit can silently use different verifiers.What
Adds
.github/workflows/basis-build.yml, which calls the existingbuild.ymland publishes its zips to a per-commit release taggedbasis-<sha10>with sha256 sidecars and aSHA256SUMSroll-up.It mirrors the
basis-buildworkflows already running onBasisResearch/cvc5(publishing frommain) andBasisResearch/z3(frommaster), including:workflow_dispatch; publish only when not a PRconcurrencyscoped per ref so PR runs do not cancelmainbuildsgh release delete --cleanup-tagbefore create, so a re-run replaces its own release rather than failing on an existing tagcontents: writescoped to the publish job onlyRelease notes carry the Verus version, taken from
build.yml's existingversionoutput.The one difference from the solver forks
The assets are zips of the whole
target-verus/releasetree, not bare binaries, because Verus needsvstd.virand its libraries alongside the executable. Consumers download and unzip rather than chmod-and-run.Risk
No change to
build.yml, so the existing artifact flow androlling-release.ymlare untouched. The new workflow only adds a publish step on top of a build that already runs green on this fork.Worth a look at whether
mainis the right and only publish branch. cvc5 and z3 each publish from their default branch and nothing else, which this matches now thatblock-non-mcpis merged.