Skip to content

[Merged by Bors] - feat: Create a partition from an element of Sym #21550

[Merged by Bors] - feat: Create a partition from an element of Sym

[Merged by Bors] - feat: Create a partition from an element of Sym #21550

name: Label New Contributors
# Written with ChatGPT: https://chat.openai.com/share/3777ceb1-d722-4705-bacd-ba3f04b387be
on: pull_request
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@v7
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;
// 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,
},
});