Skip to content

Commit 2e8afdf

Browse files
kim-emclaude
andauthored
fix: use gh release create instead of action-gh-release (#12180)
This PR switches the PR release workflow from `softprops/action-gh-release` to `gh release create`. The `softprops/action-gh-release` action enumerates all releases to check for existing ones, which fails when the repository has more than 10000 releases due to GitHub API pagination limits. The `lean4-pr-releases` repository has accumulated over 10000 releases, causing the PR release workflow to fail with: ``` Only the first 10000 results are available. ``` This is currently blocking all PR toolchain releases, including #12175. 🤖 Prepared with Claude Code --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent c7f9410 commit 2e8afdf

File tree

1 file changed

+38
-24
lines changed

1 file changed

+38
-24
lines changed

.github/workflows/pr-release.yml

Lines changed: 38 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -62,42 +62,56 @@ jobs:
6262
git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
6363
git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
6464
git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}"
65-
- name: Delete existing release if present
65+
- name: Delete existing releases if present
6666
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
6767
run: |
68-
# Try to delete any existing release for the current PR (just the version without the SHA suffix).
68+
# Delete any existing releases for this PR.
69+
# The short format release is always recreated with the latest commit.
70+
# The SHA-suffixed release should be unique per commit, but delete just in case.
6971
gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true
72+
gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} -y || true
7073
env:
7174
GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
75+
# Verify artifacts were downloaded (equivalent to fail_on_unmatched_files in the old action).
76+
- name: Verify release artifacts exist
77+
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
78+
run: |
79+
shopt -s nullglob
80+
files=(artifacts/*/*)
81+
if [ ${#files[@]} -eq 0 ]; then
82+
echo "::error::No artifacts found matching artifacts/*/*"
83+
exit 1
84+
fi
85+
echo "Found ${#files[@]} artifacts to upload:"
86+
printf '%s\n' "${files[@]}"
87+
# We use `gh release create` instead of `softprops/action-gh-release` because
88+
# the latter enumerates all releases to check for existing ones, which fails
89+
# when the repository has more than 10000 releases (GitHub API pagination limit).
90+
# Upstream fix: https://github.com/softprops/action-gh-release/pull/725
7291
- name: Release (short format)
7392
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
74-
uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
75-
with:
76-
name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
77-
# There are coredumps files here as well, but all in deeper subdirectories.
78-
files: artifacts/*/*
79-
fail_on_unmatched_files: true
80-
draft: false
81-
tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
82-
repository: ${{ github.repository_owner }}/lean4-pr-releases
93+
run: |
94+
# There are coredump files in deeper subdirectories; artifacts/*/* gets the release archives.
95+
gh release create \
96+
--repo ${{ github.repository_owner }}/lean4-pr-releases \
97+
--title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}" \
98+
--notes "" \
99+
pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} \
100+
artifacts/*/*
83101
env:
84-
# The token used here must have `workflow` privileges.
85-
GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
102+
GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
86103

87104
- name: Release (SHA-suffixed format)
88105
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
89-
uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
90-
with:
91-
name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
92-
# There are coredumps files here as well, but all in deeper subdirectories.
93-
files: artifacts/*/*
94-
fail_on_unmatched_files: true
95-
draft: false
96-
tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}
97-
repository: ${{ github.repository_owner }}/lean4-pr-releases
106+
run: |
107+
gh release create \
108+
--repo ${{ github.repository_owner }}/lean4-pr-releases \
109+
--title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})" \
110+
--notes "" \
111+
pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} \
112+
artifacts/*/*
98113
env:
99-
# The token used here must have `workflow` privileges.
100-
GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
114+
GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
101115

102116
- name: Report release status (short format)
103117
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}

0 commit comments

Comments
 (0)