PR release #54700
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
| # Push a release to the lean4-pr-releases repository, whenever someone pushes to a PR branch. | |
| # This needs to run with the `secrets.PR_RELEASES_TOKEN` token available, | |
| # but PR branches will generally come from forks, | |
| # so it is not possible to run this using the `pull_request` or `pull_request_target` workflows. | |
| # Instead we use `workflow_run`, which essentially allows us to escalate privileges | |
| # (but only runs the CI as described in the `master` branch, not in the PR branch). | |
| # The main specification/documentation for this workflow is at | |
| # https://leanprover-community.github.io/contribute/tags_and_branches.html | |
| # Keep that in sync! | |
| name: PR release | |
| on: | |
| workflow_run: # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run | |
| workflows: [CI] | |
| types: [completed] | |
| jobs: | |
| on-success: | |
| runs-on: ubuntu-latest | |
| # Run even if CI fails, as long as build artifacts are available | |
| # The "Verify release artifacts exist" step will fail if necessary artifacts are missing | |
| if: github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4' | |
| steps: | |
| - name: Retrieve information about the original workflow | |
| uses: potiuk/get-workflow-origin@e2dae063368361e4cd1f510e8785cd73bca9352e # v1_5 | |
| # This action is deprecated and archived, but it seems hard to find a | |
| # better solution for getting the PR number. Also, it must not be | |
| # updated to v1_6 because that release is broken! | |
| # see https://github.com/orgs/community/discussions/25220 for some discussion | |
| id: workflow-info | |
| with: | |
| token: ${{ secrets.GITHUB_TOKEN }} | |
| sourceRunId: ${{ github.event.workflow_run.id }} | |
| - name: Download artifact from the previous workflow. | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| id: download-artifact | |
| uses: dawidd6/action-download-artifact@b6e2e70617bc3265edd6dab6c906732b2f1ae151 # v21 | |
| with: | |
| run_id: ${{ github.event.workflow_run.id }} | |
| path: artifacts | |
| name: build-.* | |
| name_is_regexp: true | |
| # Verify artifacts were downloaded before any side effects (tag creation, release deletion). | |
| - 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[@]}" | |
| - name: Push tag | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| run: | | |
| git init --bare lean4.git | |
| git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git | |
| git -C lean4.git fetch -n origin master | |
| git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}" | |
| # Create both the original tag and the SHA-suffixed tag | |
| SHORT_SHA="${{ steps.workflow-info.outputs.sourceHeadSha }}" | |
| SHORT_SHA="${SHORT_SHA:0:7}" | |
| # Export the short SHA for use in subsequent steps | |
| echo "SHORT_SHA=${SHORT_SHA}" >> "$GITHUB_ENV" | |
| git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}" | |
| git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" "${{ steps.workflow-info.outputs.sourceHeadSha }}" | |
| git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git | |
| # `lean4-pr-releases` is not a fork of `lean4`, so without negotiation `git push` cannot | |
| # tell which objects it already has (this repo only fetched `master` and the PR commit) | |
| # and sends the entire history, exceeding GitHub's 2 GiB pack limit. `push.negotiate` | |
| # discovers a recent common commit from the remote's tags, shrinking the pack to the PR delta. | |
| # TODO: Should we even push sources here at all? | |
| git -C lean4.git -c push.negotiate=true push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} | |
| git -C lean4.git -c push.negotiate=true push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" | |
| - name: Delete existing releases if present | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| run: | | |
| # 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 }} | |
| # 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 != '' }} | |
| 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: | |
| GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }} | |
| - name: Release (SHA-suffixed format) | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| 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: | |
| GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }} | |
| - name: Report release status (short format) | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| uses: actions/github-script@v9 | |
| with: | |
| script: | | |
| await github.rest.repos.createCommitStatus({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}", | |
| state: "success", | |
| context: "PR toolchain", | |
| description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}", | |
| }); | |
| - name: Report release status (SHA-suffixed format) | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| uses: actions/github-script@v9 | |
| with: | |
| script: | | |
| await github.rest.repos.createCommitStatus({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}", | |
| state: "success", | |
| context: "PR toolchain (SHA-suffixed)", | |
| description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}", | |
| }); | |
| - name: Add toolchain-available label | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| uses: actions/github-script@v9 | |
| with: | |
| script: | | |
| await github.rest.issues.addLabels({ | |
| issue_number: ${{ steps.workflow-info.outputs.pullRequestNumber }}, | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| labels: ['toolchain-available'] | |
| }) | |
| # Finally, create/update the adaptation PR in the downstream repo. This is | |
| # the second entry point into the adaptation-pr-create action; the other | |
| # lives in `adaptation-pr.yml`. Unlike there, the toolchain release was | |
| # just created above, so it is known to exist and there is no need to look | |
| # it up first. | |
| - name: Create GitHub App token | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| uses: actions/create-github-app-token@v3 | |
| id: app-token | |
| with: | |
| client-id: ${{ vars.DOWNSTREAM_LEAN4_APP_CLIENT_ID }} | |
| private-key: ${{ secrets.DOWNSTREAM_LEAN4_APP_PRIVATE_KEY }} | |
| repositories: lean4,downstream-lean4 | |
| - name: Configure git | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| uses: leanprover/downstream-lean4/.downstream/actions/configure-git@master | |
| with: | |
| name: ${{ steps.app-token.outputs.app-slug }}[bot] | |
| - name: Checkout downstream repo | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| uses: actions/checkout@v6 | |
| with: | |
| repository: leanprover/downstream-lean4 | |
| ref: green | |
| token: ${{ steps.app-token.outputs.token }} | |
| path: downstream | |
| filter: tree:0 | |
| fetch-depth: 0 | |
| - name: Create adaptation PR | |
| id: create-adaptation-pr | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| uses: leanprover/downstream-lean4/.downstream/actions/adaptation-pr-create@master | |
| with: | |
| app-token: ${{ steps.app-token.outputs.token }} | |
| app-slug: ${{ steps.app-token.outputs.app-slug }} | |
| upstream-pr: ${{ steps.workflow-info.outputs.pullRequestNumber }} | |
| upstream-ci-green: true # We just created the toolchain release | |
| upstream-label: downstream | |
| upstream-label-force: downstream-force | |
| downstream-repo: leanprover/downstream-lean4 | |
| downstream-clone: downstream | |
| override-toolchain: leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} | |
| - name: Add toolchain-available label to adaptation PR | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.create-adaptation-pr.outputs.number != '' }} | |
| env: | |
| GH_TOKEN: ${{ steps.app-token.outputs.token }} | |
| ADAPTATION_PR: ${{ steps.create-adaptation-pr.outputs.number }} | |
| run: gh pr edit "$ADAPTATION_PR" --repo leanprover/downstream-lean4 --add-label toolchain-available |