From fa26d222cb16408e22272ae8178603925f406473 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 12 Dec 2023 01:45:10 +0100 Subject: [PATCH] chore: refactor pr release workflow (#3020) In particular: * Do not use deprecated `potiuk/get-workflow-origin`. * Use a bare checkout to push PR to `pr-releases` * Replace `script/most-recent-nightly-tag.sh` by a one-liner inside the workflow, so that th workflow is self-contained --- .github/workflows/pr-release.yml | 55 ++++++++++++++++--------------- script/most-recent-nightly-tag.sh | 16 --------- 2 files changed, 28 insertions(+), 43 deletions(-) delete mode 100755 script/most-recent-nightly-tag.sh diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 63ee7e555c..943914ac9f 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -18,25 +18,18 @@ jobs: runs-on: ubuntu-latest if: github.event.workflow_run.conclusion == 'success' && github.repository == 'leanprover/lean4' steps: - - name: Retrieve information about the original workflow - uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin + - name: Retrieve PR number and head commit + uses: actions/github-script@v7 id: workflow-info with: - token: ${{ secrets.GITHUB_TOKEN }} - sourceRunId: ${{ github.event.workflow_run.id }} - - name: Checkout - # Only proceed if the previous workflow had a pull request number. - if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} - uses: actions/checkout@v3 - with: - token: ${{ secrets.PR_RELEASES_TOKEN }} - # Since `workflow_run` runs on master, we need to specify which commit to check out, - # so that we tag the PR. - # It's important that we use `sourceHeadSha` here, not `targetCommitSha` - # as we *don't* want the synthetic merge with master. - ref: ${{ steps.workflow-info.outputs.sourceHeadSha }} - # We need a full checkout, so that we can push the PR commits to the `lean4-pr-releases` repo. - fetch-depth: 0 + script: | + const reply = await github.rest.actions.getWorkflowRun({ + owner: context.repo.owner, + repo: context.repo.repo, + run_id: context.payload.workflow_run.id, + }) + core.setOutput('pullRequestNumber', reply.data.pull_requests[0].number) + core.setOutput('sourceHeadSha', reply.data.pull_requests[0].head.sha) - name: Download artifact from the previous workflow. if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} @@ -47,14 +40,22 @@ jobs: path: artifacts name: build-.* name_is_regexp: true - - name: Prepare release + + - name: Push branch and 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 }}" + git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ 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 + git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} + - name: Delete existing release if present if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} run: | - git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git # Try to delete any existing release for the current PR. gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true - git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} - git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} env: GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }} - name: Release @@ -84,7 +85,7 @@ jobs: id: most-recent-nightly-tag if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} run: | - echo "MOST_RECENT_NIGHTLY=$(script/most-recent-nightly-tag.sh)" >> $GITHUB_ENV + git ls-remote https://github.com/leanprover/lean4-nightly.git 'refs/tags/nightly-*' --sort version:refname |tail -n1| sed 's,.*refs/tags/nightly-,MOST_RECENT_NIGHTLY=,' >> $GITHUB_ENV - name: 'Setup jq' if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} @@ -96,9 +97,9 @@ jobs: id: ready run: | echo "Most recent nightly: $MOST_RECENT_NIGHTLY" - NIGHTLY_SHA=$(git rev-parse nightly-$MOST_RECENT_NIGHTLY^{commit}) + NIGHTLY_SHA=$(git ls-remote https://github.com/leanprover/lean4-nightly.git nightly-2023-12-04|cut -f1) echo "SHA of most recent nightly: $NIGHTLY_SHA" - MERGE_BASE_SHA=$(git merge-base origin/master HEAD) + MERGE_BASE_SHA=$(git -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}") echo "SHA of merge-base: $MERGE_BASE_SHA" if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then echo "Most recent nightly tag agrees with the merge base." @@ -116,7 +117,7 @@ jobs: else echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA" echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA" - git log -10 + git -C lean4.git log -10 origin/master MESSAGE="- ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch." fi @@ -162,9 +163,9 @@ jobs: else echo "The message already exists in the comment body." fi - echo "::set-output name=mathlib_ready::false" + echo "mathlib_ready=false" >> $GITHUB_OUTPUT else - echo "::set-output name=mathlib_ready::true" + echo "mathlib_ready=true" >> $GITHUB_OUTPUT fi # We next automatically create a Mathlib branch using this toolchain. diff --git a/script/most-recent-nightly-tag.sh b/script/most-recent-nightly-tag.sh deleted file mode 100755 index 173981fd49..0000000000 --- a/script/most-recent-nightly-tag.sh +++ /dev/null @@ -1,16 +0,0 @@ -#!/bin/bash - -# Prefix for tags to search for -tag_prefix="nightly-" - -# Fetch all tags from the remote repository -git fetch https://github.com/leanprover/lean4-nightly.git --tags > /dev/null - -# Get the most recent commit that has a matching tag -tag_name=$(git tag --merged HEAD --list "${tag_prefix}*" | sort -rV | head -n 1 | sed "s/^$tag_prefix//") - -if [ -z "$tag_name" ]; then - exit 1 -fi - -echo "$tag_name"