max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: refactor pr release workflow (#3020)

Browse source 
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
This commit is contained in:
Joachim Breitner 2023-12-12 01:45:10 +01:00 • committed by GitHub
parent e2f957109f
commit fa26d222cb
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 28 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

55
.github/workflows/pr-release.yml vendored
View file

@ -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.

16
script/most-recent-nightly-tag.sh
View file

@ -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"