doc(MeasureTheory): avoid lazy continuation lines #114419
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 | |
| id: contributor-check | |
| 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; | |
| core.setOutput('should_welcome', 'false'); | |
| 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'] | |
| }); | |
| core.setOutput('should_welcome', 'true'); | |
| } | |
| 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, | |
| }, | |
| }); | |
| - name: Post welcome comment for new contributor | |
| if: steps.contributor-check.outputs.should_welcome == 'true' | |
| uses: marocchino/sticky-pull-request-comment@70d2764d1a7d5d9560b100cbea0077fc8f633987 # v3.0.2 | |
| with: | |
| header: 'New Contributor Welcome' | |
| message: | | |
| ## Welcome new contributor! | |
| Thank you for contributing to Mathlib! If you haven't done so already, please review our [contribution guidelines](https://leanprover-community.github.io/contribute/index.html), as well as the [style guide](https://leanprover-community.github.io/contribute/style.html) and [naming conventions](https://leanprover-community.github.io/contribute/naming.html). In particular, we kindly remind contributors that we have [guidelines](https://leanprover-community.github.io/contribute/index.html#use-of-ai) regarding the use of AI when making pull requests. | |
| We use a [review queue](https://leanprover-community.github.io/queueboard/review_dashboard.html) to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the `awaiting-author` tag, or another reason described in the [Lifecycle of a PR](https://leanprover-community.github.io/contribute/index.html#lifecycle-of-a-pr). The review dashboard has [a dedicated webpage](https://leanprover-community.github.io/queueboard/on_the_queue.html?search=${{ github.event.pull_request.number }}) which shows whether your PR is on the review queue, and (if not), why. | |
| If you haven't already done so, please come to [https://leanprover.zulipchat.com/](https://leanprover.zulipchat.com/), introduce yourself, and mention your new PR. | |
| Thank you again for joining our community. |