Anne's suggestions #4
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
| name: Autolabel PRs | |
| on: | |
| pull_request_target: | |
| types: [opened] | |
| push: | |
| paths: | |
| - scripts/autolabel.lean | |
| - .github/workflows/add_label_from_diff.yaml | |
| # Limit permissions for GITHUB_TOKEN for the entire workflow | |
| permissions: | |
| contents: read | |
| pull-requests: write # Only allow PR comments/labels | |
| # All other permissions are implicitly 'none' | |
| jobs: | |
| add_topic_label: | |
| name: Add topic label | |
| runs-on: ubuntu-latest | |
| # Don't run on forks, where we wouldn't have permissions to add the label anyway. | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| steps: | |
| - name: Checkout master branch to build autolabel from | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| with: | |
| ref: master | |
| path: tools | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| lake-package-directory: tools # Building here | |
| - name: Build autolabel from master | |
| working-directory: tools | |
| run: | | |
| lake build autolabel | |
| - name: Checkout branch to label | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| with: | |
| ref: ${{ github.event.pull_request.head.sha || github.sha }} | |
| fetch-depth: 0 | |
| path: pr-branch | |
| - name: Run autolabel | |
| working-directory: pr-branch | |
| run: | | |
| labels="$("${GITHUB_WORKSPACE}/tools/.lake/build/bin/autolabel")" | |
| printf '%s\n' "${labels}" | |
| # extract | |
| label="$(printf '%s' "${labels}" | sed -n 's=^::notice::.*#\[\([^,]*\)\].*=\1=p')" | |
| printf 'label: "%s"\n' "${label}" | |
| if [ -n "${label}" ] && [ -n "${PR_NUMBER}" ] | |
| then | |
| printf 'Applying label %s\n' "${label}" | |
| # we use curl rather than octokit/request-action so that the job won't fail | |
| # (and send an annoying email) if the labels don't exist | |
| url="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/labels" | |
| printf 'url: %s\n' "${url}" | |
| jsonLabel="$(printf '{"labels":["%s"]}' "${label}")" | |
| printf 'jsonLabel: %s\n' "${jsonLabel}" | |
| curl --request POST \ | |
| --header 'Accept: application/vnd.github+json' \ | |
| --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' \ | |
| --header 'X-GitHub-Api-Version: 2022-11-28' \ | |
| --url "${url}" \ | |
| --data "${jsonLabel}" | |
| else | |
| echo "There is no single label that we could apply, so we are not applying any label." | |
| fi | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| # the PR number could be undefined in workflows triggered by 'push', | |
| # in which case we only log the applicable label and exit | |
| PR_NUMBER: ${{ github.event.pull_request.number }} |