chore: new PR changelog template (#5976)

Enables us to auto-generate the changelog from the list of PRs for a
modicum of summarizing/categorizing work on PR creation.

Does not (yet) allow external contributors to set category labels by
themselves as this creates issues with triggering one workflow from
another, it is not clear whether they should be allowed to create new
categories, and the reviewer/triage team likely is in a better position
to do the categorization anyway.

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