From 2e8afdf74db2efda82632ac0df05bb84ac707766 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 27 Jan 2026 16:04:43 +1100 Subject: [PATCH] fix: use gh release create instead of action-gh-release (#12180) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 https://github.com/leanprover/lean4/pull/12175. 🤖 Prepared with Claude Code --------- Co-authored-by: Claude --- .github/workflows/pr-release.yml | 62 +++++++++++++++++++------------- 1 file changed, 38 insertions(+), 24 deletions(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index a2eb7343d0..dfcfef266f 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -62,42 +62,56 @@ jobs: git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" - - name: Delete existing release if present + - name: Delete existing releases if present if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} run: | - # Try to delete any existing release for the current PR (just the version without the SHA suffix). + # Delete any existing releases for this PR. + # The short format release is always recreated with the latest commit. + # The SHA-suffixed release should be unique per commit, but delete just in case. gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true + gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} -y || true env: GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }} + # Verify artifacts were downloaded (equivalent to fail_on_unmatched_files in the old action). + - name: Verify release artifacts exist + if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} + run: | + shopt -s nullglob + files=(artifacts/*/*) + if [ ${#files[@]} -eq 0 ]; then + echo "::error::No artifacts found matching artifacts/*/*" + exit 1 + fi + echo "Found ${#files[@]} artifacts to upload:" + printf '%s\n' "${files[@]}" + # We use `gh release create` instead of `softprops/action-gh-release` because + # the latter enumerates all releases to check for existing ones, which fails + # when the repository has more than 10000 releases (GitHub API pagination limit). + # Upstream fix: https://github.com/softprops/action-gh-release/pull/725 - name: Release (short format) if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} - uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b - with: - name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} - # There are coredumps files here as well, but all in deeper subdirectories. - files: artifacts/*/* - fail_on_unmatched_files: true - draft: false - tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} - repository: ${{ github.repository_owner }}/lean4-pr-releases + run: | + # There are coredump files in deeper subdirectories; artifacts/*/* gets the release archives. + gh release create \ + --repo ${{ github.repository_owner }}/lean4-pr-releases \ + --title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}" \ + --notes "" \ + pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} \ + artifacts/*/* env: - # The token used here must have `workflow` privileges. - GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }} + GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }} - name: Release (SHA-suffixed format) if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} - uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b - with: - name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }}) - # There are coredumps files here as well, but all in deeper subdirectories. - files: artifacts/*/* - fail_on_unmatched_files: true - draft: false - tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} - repository: ${{ github.repository_owner }}/lean4-pr-releases + run: | + gh release create \ + --repo ${{ github.repository_owner }}/lean4-pr-releases \ + --title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})" \ + --notes "" \ + pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} \ + artifacts/*/* env: - # The token used here must have `workflow` privileges. - GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }} + GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }} - name: Report release status (short format) if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}