lean-pr-testing-11447 #290
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@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0 | |
| with: | |
| script: | | |
| const MIN_MERGED = 5; | |
| const creator = context.payload.sender.login; | |
| const { owner, repo } = context.repo; | |
| console.log(`Checking closed issues for user: ${creator}`); | |
| let mergedByBorsPRs = []; | |
| let totalIssuesChecked = 0; | |
| // Paginate through issues, stopping when we have more than MIN_MERGED qualifying PRs | |
| for await (const response of github.paginate.iterator( | |
| github.rest.issues.listForRepo, | |
| { | |
| owner, | |
| repo, | |
| creator, | |
| state: 'closed', | |
| per_page: 100 | |
| } | |
| )) { | |
| totalIssuesChecked += response.data.length; | |
| // Filter this page for PRs with "[Merged by Bors] -" in the title | |
| const pageMatches = response.data.filter(item => | |
| item.pull_request && item.title.startsWith('[Merged by Bors] -') | |
| ); | |
| mergedByBorsPRs.push(...pageMatches); | |
| console.log(`Checked ${totalIssuesChecked} closed issues, found ${mergedByBorsPRs.length} PRs merged by Bors so far`); | |
| // Stop early if we've found more than MIN_MERGED | |
| if (mergedByBorsPRs.length > MIN_MERGED) { | |
| console.log(`Found more than ${MIN_MERGED} PRs, stopping pagination early`); | |
| break; | |
| } | |
| } | |
| const pullRequestCount = mergedByBorsPRs.length; | |
| console.log(`Found ${pullRequestCount} PRs merged by Bors`); | |
| // Determine if the creator has MIN_MERGED or fewer merged pull requests | |
| if (pullRequestCount <= MIN_MERGED) { | |
| console.log('Adding "new-contributor" label...'); | |
| await github.rest.issues.addLabels({ | |
| issue_number: context.issue.number, | |
| owner, | |
| repo, | |
| labels: ['new-contributor'] | |
| }); | |
| } | |
| console.log('Creating check run with a message about the PR count by this author...'); | |
| const message = `Found ${pullRequestCount} merged 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, | |
| }, | |
| }); |