feat: check indentation of doc-strings by grunweg · Pull Request #27897 · leanprover-community/mathlib4

grunweg · 2025-08-03T11:49:06Z

Likely will require further adaptations to mathlib. May land piece-wise. But at first, let's see how big the overall fallout actually is.
(So far: 100 lines of implementation and tests, and 170 lines of fix-ups; which are probably mostly complete, but not entirely.)

depends on: feat: check indentation of doc-strings, basic version #27898
depends on: [Merged by Bors] - chore: add a few missing codeblock fences to doc-strings #39245
depends on: [Merged by Bors] - chore: fix odd indentation in a few doc-strings #39246
depends on: [Merged by Bors] - doc: add newlines to clarify paragraph breaks #39247

github-actions · 2025-08-03T11:50:18Z

PR summary 424dce2f30

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ ItemStatus
+ bar
+ baz
+ check
+ foo
+ hoge
+ hogehoge
+ hogehoge'
+ more
+ more'
+ sdf
+ sdf'
+ sdf''
+ sdf'''
+ startsNumberedItem

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.

No changes to strong technical debt.

No changes to weak technical debt.

Continuation of #24166. Works towards the linter in #27897.

mathlib4-merge-conflict-bot · 2025-08-04T16:13:51Z

This pull request has conflicts, please merge master and resolve them.

…community#27899) Continuation of leanprover-community#24166. Works towards the linter in leanprover-community#27897.

mathlib4-merge-conflict-bot · 2025-08-08T06:36:31Z

This pull request has conflicts, please merge master and resolve them.

mathlib4-merge-conflict-bot · 2025-08-14T06:17:05Z

This pull request has conflicts, please merge master and resolve them.

…community#27899) Continuation of leanprover-community#24166. Works towards the linter in leanprover-community#27897.

joneugster

Thanks for your work on this front!

I think the linter itself would profit from some cleanup/optimising to make it more readable and avoid duplicated loops.

joneugster · 2026-05-08T16:13:19Z

 namespace Style

+/-- Check if a doc-string conforms to some basic style guidelines.
+TODO: flesh out which ones and why! -/


is this still a draft-PR?

joneugster · 2026-05-08T16:15:21Z

+    if indent.contains '\t' then
+      msgs := msgs.push m!"error: line '{line}' starts with a tab; use spaces instead"


Out of curiosity, isn't this already covered by another linter?

joneugster · 2026-05-08T16:16:32Z

+    let indent := line.takeWhile Char.isWhitespace
+    if let some n := prev_ident then
+      if line.trimLeft.startsWith "- " || line.startsWith "* " then
+        -- De-denting is possibly by any number of levels.


is that a word?

grunweg · 2026-05-12T10:58:08Z

Thanks for your review! I added a lot of tests, fixed all errors in mathlib --- and just completely rewrote the algorithm (which might find further locations to fix). To keep history sane, I just force-pushed (sorry for that!). Before progressing further, probably most mathlib fixes should be merged first.

There is no reason for this, and this makes it easier to lint them. Found by the linter in #27897.

Found by the linter in #27897, but I expect the move to Verso would also have discovered this.

There is no reason for this, and this makes it easier to lint them. Found by the linter in #27897.

Found by the linter in #27897, but I expect the move to Verso would also have discovered this.

There is no reason for this, and this makes it easier to lint them. Found by the linter in #27897.

These are strictly speaking, required by markdown, and make it more clear to the reader that a new paragraph begins. This corrects some generated documentation entries to have proper paragraph breaks. Found by the linter in #27897.

grunweg · 2026-05-13T01:43:09Z

For the record, the new algorithm has a new class of false positives: for doc-strings which are indented, it warns too much.

mathlib-dependent-issues · 2026-05-13T02:06:35Z

This PR/issue depends on:

~~feat: check indentation of doc-strings, basic version #27898~~
~~[Merged by Bors] - chore: add a few missing codeblock fences to doc-strings #39245~~
~~[Merged by Bors] - chore: fix odd indentation in a few doc-strings #39246~~
~~[Merged by Bors] - doc: add newlines to clarify paragraph breaks #39247~~
By Dependent Issues (🤖). Happy coding!

grunweg added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-linter Linter labels Aug 3, 2025

grunweg mentioned this pull request Aug 3, 2025

feat: check indentation of doc-strings, basic version #27898

Closed

3 tasks

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 3, 2025

grunweg mentioned this pull request Aug 3, 2025

[Merged by Bors] - chore: correctly indent enumeration items in doc-strings #27899

Closed

mathlib-bors Bot pushed a commit that referenced this pull request Aug 4, 2025

chore: correctly indent enumeration items in doc-strings (#27899)

d19971e

Continuation of #24166. Works towards the linter in #27897.

mathlib4-merge-conflict-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 Aug 4, 2025

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 Aug 6, 2025

mathlib4-merge-conflict-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 Aug 8, 2025

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 Aug 11, 2025

mathlib4-merge-conflict-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 Aug 14, 2025

Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025

chore: correctly indent enumeration items in doc-strings (leanprover-…

35b88b7

…community#27899) Continuation of leanprover-community#24166. Works towards the linter in leanprover-community#27897.

Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025

chore: correctly indent enumeration items in doc-strings (leanprover-…

fbb8308

…community#27899) Continuation of leanprover-community#24166. Works towards the linter in leanprover-community#27897.

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

mathlib-dependent-issues Bot deleted a comment from mathlib4-dependent-issues-bot Feb 15, 2026

grunweg removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 8, 2026

joneugster reviewed May 8, 2026

View reviewed changes

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label May 8, 2026

grunweg added 4 commits May 12, 2026 12:42

chore: add more codeblocks

48e0e56

chore: fix weird indentation

46a2298

chore: clarifying newlines

066c407

linter, tests, annotate three false positives

c0b3163

This was referenced May 12, 2026

[Merged by Bors] - chore: add a few missing codeblock fences to doc-strings #39245

Closed

[Merged by Bors] - chore: fix odd indentation in a few doc-strings #39246

Closed

[Merged by Bors] - doc: add newlines to clarify paragraph breaks #39247

Closed

grunweg force-pushed the docstring-indent branch from cdcce4c to c0b3163 Compare May 12, 2026 10:56

grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 12, 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 May 12, 2026

mathlib-bors Bot pushed a commit that referenced this pull request May 12, 2026

chore: fix odd indentation in a few doc-strings

a390ae7

There is no reason for this, and this makes it easier to lint them. Found by the linter in #27897.

mathlib-bors Bot pushed a commit that referenced this pull request May 12, 2026

chore: add a few missing codeblock fences to doc-strings (#39245)

588cc30

Found by the linter in #27897, but I expect the move to Verso would also have discovered this.

mathlib-bors Bot pushed a commit that referenced this pull request May 12, 2026

chore: fix odd indentation in a few doc-strings (#39246)

2355696

There is no reason for this, and this makes it easier to lint them. Found by the linter in #27897.

mathlib-bors Bot pushed a commit that referenced this pull request May 12, 2026

chore: add a few missing codeblock fences to doc-strings (#39245)

d9cff27

Found by the linter in #27897, but I expect the move to Verso would also have discovered this.

mathlib-bors Bot pushed a commit that referenced this pull request May 12, 2026

chore: fix odd indentation in a few doc-strings (#39246)

d78ab65

There is no reason for this, and this makes it easier to lint them. Found by the linter in #27897.

mathlib-bors Bot pushed a commit that referenced this pull request May 12, 2026

chore: fix odd indentation in a few doc-strings (#39246)

bcb9e00

There is no reason for this, and this makes it easier to lint them. Found by the linter in #27897.

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label May 13, 2026

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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: check indentation of doc-strings#27897

feat: check indentation of doc-strings#27897
grunweg wants to merge 4 commits into
leanprover-community:masterfrom
grunweg:docstring-indent

grunweg commented Aug 3, 2025 •

edited

Loading

Uh oh!

github-actions Bot commented Aug 3, 2025 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Aug 4, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Aug 8, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Aug 14, 2025

Uh oh!

joneugster left a comment •

edited

Loading

Uh oh!

joneugster May 8, 2026

Uh oh!

Uh oh!

joneugster May 8, 2026

Uh oh!

joneugster May 8, 2026

Uh oh!

grunweg commented May 12, 2026

Uh oh!

grunweg commented May 13, 2026

Uh oh!

mathlib-dependent-issues Bot commented May 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

		if indent.contains '\t' then
		msgs := msgs.push m!"error: line '{line}' starts with a tab; use spaces instead"

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 424dce2f30

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Aug 4, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Aug 8, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Aug 14, 2025

Uh oh!

joneugster left a comment • 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!

joneugster May 8, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

joneugster May 8, 2026

Choose a reason for hiding this comment

Uh oh!

joneugster May 8, 2026

Choose a reason for hiding this comment

Uh oh!

grunweg commented May 12, 2026

Uh oh!

grunweg commented May 13, 2026

Uh oh!

mathlib-dependent-issues Bot commented May 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

grunweg commented Aug 3, 2025 •

edited

Loading

github-actions Bot commented Aug 3, 2025 •

edited

Loading

joneugster left a comment •

edited

Loading