Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 38 additions & 9 deletions .github/workflows/basis-build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,11 +17,15 @@ on:
workflow_dispatch:

permissions:
contents: write
contents: read

concurrency:
group: basis-build-${{ github.ref }}
cancel-in-progress: true
# PR builds share a group per branch so a new push cancels the superseded
# run. Every other run gets a group per commit: a group holds only one
# pending run, so a shared mainline group would still drop the middle one
# of three quick pushes and leave that commit without a release.
group: basis-build-${{ github.event_name == 'pull_request' && github.ref || github.sha }}
cancel-in-progress: ${{ github.event_name == 'pull_request' }}

jobs:
build:
Expand Down Expand Up @@ -91,6 +95,8 @@ jobs:
if: github.event_name != 'pull_request'
needs: [build]
runs-on: ubuntu-24.04
permissions:
contents: write
steps:
- name: download all artifacts
uses: actions/download-artifact@v8
Expand All @@ -101,14 +107,37 @@ jobs:
shell: bash
run: |
tag="basis-${GITHUB_SHA:0:10}"
files=(
z3-arm64-macos/z3-arm64-macos
z3-arm64-macos/z3-arm64-macos.sha256
z3-x86-linux/z3-x86-linux
z3-x86-linux/z3-x86-linux.sha256
SHA256SUMS
)
# The binaries are not byte-reproducible, so a re-run must not
# replace a published release whose hash verus-tools-mcp may
# already pin. An intentional replacement needs a manual
# `gh release delete`. `gh release create` uploads assets to a
# draft and publishes it last, so a draft here means an earlier
# run was interrupted; nobody can have pinned it, so redo it.
if release=$(gh release view "$tag" --repo "$GITHUB_REPOSITORY" --json isDraft,assets 2>/dev/null); then
if [ "$(jq -r .isDraft <<<"$release")" = true ]; then
echo "::warning::deleting draft release $tag left by an interrupted run"
gh release delete -y "$tag" --repo "$GITHUB_REPOSITORY"
else
missing=$(jq -r --args '$ARGS.positional - [.assets[].name] | join(" ")' \
"${files[@]##*/}" <<<"$release")
if [ -n "$missing" ]; then
echo "::error::published release $tag is missing assets: $missing; delete it by hand to rebuild"
exit 1
fi
echo "::notice::release $tag already exists with all assets; keeping it"
exit 0
fi
fi
cat */*.sha256 > SHA256SUMS
gh release delete -y "$tag" --repo "$GITHUB_REPOSITORY" --cleanup-tag 2>/dev/null || true
gh release create "$tag" --repo "$GITHUB_REPOSITORY" \
--target "$GITHUB_SHA" \
--title "Basis z3 build $tag" \
--notes "$(printf 'Pinned Basis build of z3 at %s.\n\n```\n%s\n```' "$GITHUB_SHA" "$(cat SHA256SUMS)")" \
z3-arm64-macos/z3-arm64-macos \
z3-arm64-macos/z3-arm64-macos.sha256 \
z3-x86-linux/z3-x86-linux \
z3-x86-linux/z3-x86-linux.sha256 \
SHA256SUMS
"${files[@]}"