chore: new PR changelog template

.github/PULL_REQUEST_TEMPLATE.md

@@ -5,11 +5,18 @@
 * 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 it does not have this label,
+  it must instead be categorized with one of the `changelog-*` labels. Ask a reviewer for help
+  if in doubt.
+* You can manage the changelog labels and `awaiting-review`, `awaiting-author`, and `WIP` labels 
+  yourself, by writing a comment containing one of these labels on its own line.
 * 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.
 
 ---
 
+This PR <short changelog summary for feat/fix, see above>.
+
 Closes #0000 (`RFC` or `bug` issue number fixed by this PR, if any)

.github/workflows/labels-from-comments.yml

@@ -11,7 +11,7 @@ on:
 
 jobs:
   update-label:
-    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci'))
+    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci')  || contains(github.event.comment.body, 'changelog-'))
     runs-on: ubuntu-latest
 
     steps:
@@ -20,7 +20,7 @@ jobs:
       with:
         github-token: ${{ secrets.GITHUB_TOKEN }}
         script: |
-          const { owner, repo, number: issue_number  } = context.issue;
+          const { owner, repo, number: issue_number, labels } = context.issue;
           const commentLines = context.payload.comment.body.split('\r\n');
 
           const awaitingReview = commentLines.includes('awaiting-review');
@@ -47,3 +47,11 @@ jobs:
           if (releaseCI) {
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] });
           }
+
+          if (const chlog = commentLines.find(line => line.startsWith("changelog-")) {
+            if (const previous = labels.find(label => label.name.startsWith("changelog-")) {
+              await github.rest.issues.removeLabel({ owner, repo, issue_number, name: previous.name });
+            }
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: [chlog] });
+          }
+

.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]
+
+jobs:
+  check-pr-title:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check PR title
+        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.');
+              }
+            }