diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index c7f9bc32d09a..404720bbc1b0 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -5,6 +5,10 @@ * Include the link to your `RFC` or `bug` issue in the description. * If the issue does not already have approval from a developer, submit the PR as draft. * The PR title/description will become the commit message. Keep it up-to-date as the PR evolves. +* For `feat/fix` PRs, the first paragraph starting with "This PR" must be present and will become a + changelog entry unless the PR is labeled with `no-changelog`. If the PR does not have this label, + it must instead be categorized with one of the `changelog-*` labels (which will be done by a + reviewer for external PRs). * A toolchain of the form `leanprover/lean4-pr-releases:pr-release-NNNN` for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing `release-ci` on its own line. * If you rebase your PR onto `nightly-with-mathlib` then CI will test Mathlib against your PR. * You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line. @@ -12,4 +16,6 @@ --- -Closes #0000 (`RFC` or `bug` issue number fixed by this PR, if any) +This PR . + +Closes <`RFC` or `bug` issue number fixed by this PR, if any> diff --git a/.github/workflows/pr-body.yml b/.github/workflows/pr-body.yml new file mode 100644 index 000000000000..62c548db2d9b --- /dev/null +++ b/.github/workflows/pr-body.yml @@ -0,0 +1,24 @@ +name: Check PR body for changelog convention + +on: + merge_group: + pull_request: + types: [opened, synchronize, reopened, edited, labeled] + +jobs: + check-pr-body: + runs-on: ubuntu-latest + steps: + - name: Check PR body + uses: actions/github-script@v7 + with: + script: | + const { title, body, labels } = context.payload.pull_request; + if (/^(feat|fix):/.test(title) && !labels.some(label => label.name == "changelog-no")) { + if (!labels.some(label => label.name.startsWith("changelog-"))) { + core.setFailed('feat/fix PR must have a `changelog-*` label'); + } + if (!/^This PR [^<]/.test(body)) { + core.setFailed('feat/fix PR must have changelog summary starting with "This PR ..." as first line.'); + } + }