feat: add a few basic checks for PR descriptions by grunweg · Pull Request #40181 · leanprover-community/mathlib4

grunweg · 2026-06-03T12:08:18Z

Not exhaustive, but hopefully this is already useful.

depends on: chore: add further tests for the title checks around capitalisation #40179
depends on: fix: label parsing in the check_title workflow #40234

Please carefully double-check the CI variable changes: this is what the Github documentation search told me (which is AI-powered); at some point, I gave up trying to verify this by hand.

github-actions · 2026-06-03T12:09:40Z

PR summary 706a62f36d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ validatePRBody

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 706a62f36d
Reference commit c87658adb9

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

.github/workflows/build_template.yml
.github/workflows/check_pr_titles.yaml

mathlib-dependent-issues · 2026-06-03T13:33:23Z

This PR/issue depends on:

chore: add further tests for the title checks around capitalisation #40179
fix: label parsing in the check_title workflow #40234
By Dependent Issues (🤖). Happy coding!

Not hooked up yet

Not exhaustive, but hopefully this is already useful. This PR only implements the checks; a separate PR will run them in CI.

Run the PR description check only when the title starts with "feat" and the PR is not labelled `easy`. The title-format check still runs for all PRs; only the description check is gated. Also fix label parsing: labels were read via `args.variableArgsAs!`, but none are declared, so the `--labels` flag was parsed and discarded and `labels` was always empty (the `WIP`-skip never fired either). Read the flag and split it on newlines, matching the workflow's `jq -r '.[].name'` output. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

bryangingechen

Some tweaks / fixes (with help from Claude code).

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

grunweg · 2026-06-04T16:59:24Z

Thanks for the review; I have addressed all comments. #40234 is just the fix for the label parsing.

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

SnirBroshi · 2026-06-05T13:29:47Z

+  -- commit message at the first line starting with "---" (its `cut_body_after = "\n---"`),
+  -- so that is exactly what we treat as a fold here.
+  let before := description.lines.toList.takeWhile (fun l ↦ !l.startsWith "---")
+  -- If `after` is non-empty, there is a fold.


Can we lint against descriptions without a fold? (if after.isEmpty)
There's no reason to delete the fold from the PR template, and I also think this will filter out many slop PRs since they ignore the template and replace everything with slop (and might not notice CI failing).

SnirBroshi · 2026-06-05T13:38:04Z

+  if before.isEmpty && !after.isEmpty then
+    errors := errors.push
+      "warning: your PR description is non-empty, but everything is after the '---' line\n\
+      note: the final PR commit message only uses what is above that line"


after includes the fold itself, so a PR description that is just a fold will error here but there is nothing after the --- line, so the warning text will seem strange.

I suggest something like:

let beforeContainsText := before.any (·.any (·.isAlpha)) let afterContainsText := after.any (·.any (·.isAlpha))

and then using these booleans here. Other than accounting for the fold, this will also take care of descriptions such as

. ---

I also suggest using these booleans for the "description is empty" check.

grunweg added the CI Modifies the continuous integration setup or other automation label Jun 3, 2026

github-actions Bot added the t-linter Linter label Jun 3, 2026

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 3, 2026

github-actions Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 3, 2026

grunweg and others added 9 commits June 4, 2026 11:40

chore: add further tests for the title checks around capitalisation

4a5ead9

wip: some checks for PR description

e731709

Not hooked up yet

chore: test setup

8dee506

feat: add a few basic checks for PR descriptions

73b0b47

Not exhaustive, but hopefully this is already useful. This PR only implements the checks; a separate PR will run them in CI.

Partially hook this up in CI

c05630e

chore: also hook up CI workflow to pass the PR body

f4427e4

fixup

5f1a94f

Revert bad change

021e7dc

grunweg force-pushed the validate-description-also branch from 7be2826 to 021e7dc Compare June 4, 2026 09:41

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 4, 2026

grunweg temporarily deployed to cache-upload-forks June 4, 2026 09:48 — with GitHub Actions Inactive

grunweg added 2 commits June 4, 2026 11:49

Fixup CLI logic: need to ensure the input is passed nicely

e6ee17d

Fixup final workflow step

afb6106

bryangingechen reviewed Jun 4, 2026

View reviewed changes

grunweg and others added 2 commits June 4, 2026 18:45

Tweaks from code review

a8cfdcc

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Fix warning; tests for the fixes from the previous commit

f666051

grunweg temporarily deployed to cache-upload-forks June 4, 2026 16:50 — with GitHub Actions Inactive

grunweg added 2 commits June 4, 2026 18:51

Fixups

172929f

Back to newline-separated

c9de899

grunweg mentioned this pull request Jun 4, 2026

fix: label parsing in the check_title workflow #40234

Open

grunweg temporarily deployed to cache-upload-forks June 4, 2026 17:00 — with GitHub Actions Inactive

Update .github/workflows/check_pr_titles.yaml

5d13376

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Remove noisy line

706a62f

SnirBroshi reviewed Jun 5, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add a few basic checks for PR descriptions#40181

feat: add a few basic checks for PR descriptions#40181
grunweg wants to merge 17 commits into
leanprover-community:masterfrom
grunweg:validate-description-also

grunweg commented Jun 3, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jun 3, 2026 •

edited

Loading

Declarations diff (regex)

Uh oh!

mathlib-dependent-issues Bot commented Jun 3, 2026 •

edited

Loading

Uh oh!

bryangingechen left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jun 4, 2026

Uh oh!

SnirBroshi Jun 5, 2026

Uh oh!

SnirBroshi Jun 5, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

grunweg commented Jun 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jun 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 706a62f36d

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean -- pending)

⚠️ Workflow documentation reminder

Uh oh!

mathlib-dependent-issues Bot commented Jun 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

bryangingechen left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jun 4, 2026

Uh oh!

SnirBroshi Jun 5, 2026

Choose a reason for hiding this comment

Uh oh!

SnirBroshi Jun 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

grunweg commented Jun 3, 2026 •

edited

Loading

github-actions Bot commented Jun 3, 2026 •

edited

Loading

mathlib-dependent-issues Bot commented Jun 3, 2026 •

edited

Loading

SnirBroshi Jun 5, 2026 •

edited

Loading