pr-release.yml

# 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