[Merged by Bors] - chore: rename IrreducibleCloseds fields to match naming convention #107465
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: Label New Contributors | |
| # Written with ChatGPT: https://chat.openai.com/share/3777ceb1-d722-4705-bacd-ba3f04b387be | |
| on: | |
| pull_request_target: | |
| types: | |
| - opened | |
| # 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: | |
| label-and-report-new-contributor: | |
| 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' | |
| permissions: | |
| checks: write | |
| pull-requests: write | |
| contents: read | |
| steps: | |
| - name: Label PR and report count | |
| uses: actions/github-script@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7.0.1 | |
| with: | |
| script: | | |
| const creator = context.payload.sender.login | |
| const { owner, repo } = context.repo; | |
| const opts = github.rest.issues.listForRepo.endpoint.merge({ | |
| ...context.issue, | |
| owner, | |
| repo, | |
| creator, | |
| state: 'closed' | |
| }) | |
| const issues = await github.paginate(opts) | |
| const pullRequestCount = issues.length; | |
| // We could filter out bot users here, with: | |
| // const isBot = (github.rest.users.getByUsername(creator).type === "Bot"); | |
| // But we choose to label PRs by new bot contributors as well. | |
| // Determine if the creator has 5 or fewer pull requests | |
| if (pullRequestCount <= 5) { | |
| // Add the "new-contributor" label to the current pull request | |
| await github.rest.issues.addLabels({ | |
| issue_number: context.issue.number, | |
| owner, | |
| repo, | |
| labels: ['new-contributor'] | |
| }); | |
| } | |
| // Create a check run with a message about the PR count by this author | |
| const message = `Found ${pullRequestCount} PRs by ${creator}.`; | |
| await github.rest.checks.create({ | |
| owner, | |
| repo, | |
| name: 'New Contributor Check', | |
| head_sha: context.payload.pull_request.head.sha, | |
| status: 'completed', | |
| conclusion: 'neutral', | |
| output: { | |
| title: message, | |
| summary: message, | |
| }, | |
| }); |