chore: new PR changelog template

.github/PULL_REQUEST_TEMPLATE.md

@@ -5,11 +5,17 @@
 * 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 line 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.
 * Remove this section, up to and including the `---` before submitting.
 
 ---
 
-Closes #0000 (`RFC` or `bug` issue number fixed by this PR, if any)
+This PR <short changelog summary for feat/fix, see above>.
+
+Closes <`RFC` or `bug` issue number fixed by this PR, if any>

.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.');
+              }
+            }