[Merged by Bors] - chore: rename IrreducibleCloseds fields to match naming convention #15930
Workflow file for this run
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 code | |
| uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| with: | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| fetch-depth: 0 | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: lake exe autolabel | |
| run: | | |
| # the checkout dance, to avoid a detached head | |
| git checkout master | |
| git checkout - | |
| labels="$(lake exe autolabel)" | |
| printf '%s\n' "${labels}" | |
| # extract | |
| label="$(printf '%s' "${labels}" | sed -n 's=.*#\[\([^,]*\)\].*=\1=p')" | |
| printf 'label: "%s"\n' "${label}" | |
| if [ -n "${label}" ] | |
| 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/${{ github.event.pull_request.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 }} |