[Merged by Bors] - feat: the doc-string linter by adomani · Pull Request #22095 · leanprover-community/mathlib4

adomani · 2025-02-19T17:35:03Z

The docString linter checks that doc-strings begin with

/-- <Text> or
/--⏎<Text>

and that <Text> does not begin with a space or a line break. Similarly for the characters preceding -/ at the end of a doc-string.

Discussed in Zulip

github-actions · 2025-02-19T17:36:01Z

PR summary 5b889058df

Import changes exceeding 2%

%	File
+5.26%	`Mathlib.Init`
+2.78%	`Mathlib.Logic.Function.Defs`
+5.00%	`Mathlib.Tactic.FunProp.Decl`

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
There are 5984 files with changed transitive imports taking up over 249633 characters: this is too many to display!
You can run `scripts/import_trans_difference.sh all` locally to see the whole output.

Declarations diff

+ docStringLinter
+ foo

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (2.00, 0.02)

Current number	Change	Type
100	2	adaptation notes

Current commit 5b889058df
Reference commit 062d4014b7

You can run this locally as

./scripts/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).

adomani · 2025-02-19T20:24:53Z

If we do a better job at tracking where the exceptions are, the warning can be logged "at" the right positions in the string and highlight what they refer to.

adomani · 2025-02-19T21:13:56Z

You can take a look at

https://github.com/leanprover-community/mathlib4/pull/new/adomani/docstring_linter_range

for a start at getting the warning where the issue is. The ppRoundtrip linter also has a mechanism to try to underline where the issue are.

adomani · 2025-02-20T21:02:56Z

+  if lines.any (·.startsWith " ")
+    -- For now, we skip cases where a line starts with "* " or "- " as these are probably markdown
+    -- code blocks. (We can later try to re-enable some linting there.)
+    && !lines.any (fun l ↦ l.startsWith "* " || l.startsWith "- ") then


How about including also ``` as an allowed start for exceptions?

Overall, I am still not sold on this check, as I find that it would require a more thorough parsing of markdown to really be effective.

grunweg

I just took a look: I think the implementation looks good, just minor comments.
I don't think the empty doc-strings need to block this from landing (as they are pre-existing). One could add an "empty doc-string linter" which complains about these specifically (the current error is not great), and also searches for e.g. doc-strings which are just TODO or TODO!. That can happen in a follow-up, though.

grunweg · 2025-02-27T18:40:11Z

(Let me add: I think this is basically ready to be maintainer merged, with the question of these doc-strings being the biggest open item.)

Co-authored-by: grunweg <[email protected]>

…unity/mathlib4 into adomani/docstring_linter

adomani

Michael, thank you so much for the review!

adomani · 2025-02-28T17:23:45Z

With respect to "empty" docstrings, I think that we can test whether a trimmed docstring contains no space and emit a warning then, with a more meaningful comment, such as "A doc-string that has at most one word is probably not a good docstring!" or something like this.

I would leave this for later, though.

grunweg

Thanks; I like your changes. Just two more nits.
Note to maintainers: this PR adds three manual linter exceptions, to declarations with an essentially empty doc-string. These were pre-existing; I don't think this PR should be blocked on that.
maintainer delegate

github-actions · 2025-02-28T18:27:07Z

🚀 Pull request has been placed on the maintainer queue by grunweg.

PatrickMassot · 2025-03-07T09:35:49Z

bors d+

mathlib-bors · 2025-03-07T09:35:51Z

✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

…inter

adomani · 2025-03-07T13:25:20Z

bors merge

The `docString` linter checks that doc-strings begin with * `/-- <Text>` or * `/--⏎<Text>` and that `<Text>` does not begin with a space or a line break. Similarly for the characters preceding `-/` at the end of a doc-string. Discussed in [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Style.20.3Abicycle.3A.20.3A.20indenting.20second.20lines.20in.20doc-strings)

mathlib-bors · 2025-03-07T14:33:26Z

Pull request successfully merged into master.

Build succeeded:

feat: the doc-string linter

fe8319e

adomani marked this pull request as draft February 19, 2025 17:35

adomani added the WIP Work in progress label Feb 19, 2025

github-actions bot added the t-linter Linter label Feb 19, 2025

adomani added 2 commits February 19, 2025 17:54

lint

1871e93

lint more

b9c5c3e

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 19, 2025

grunweg and others added 8 commits February 19, 2025 19:35

Add rough functionality

3b1fdf3

Refine

bced0a3

Add basic tests

314ca76

Present multiple errors

33d236c

Update and fix

f23ff5b

Add to Mathlib.Init, add myself as author

92829f7

minor tweaks

5bc12ac

import header, fix tests

ae675c5

adomani commented Feb 19, 2025

View reviewed changes

Comment thread Mathlib/Tactic/Linter/DocString.lean Outdated

grunweg added 6 commits February 19, 2025 21:58

chore(Lean,Tactic): un-indent some doc-strings

9b6f58d

chore(Geometry/Manifold): un-indent

224d985

Unindent two more

9973868

chore(Topology): unindent two more

6b22e47

Tweak error message: remove unnecessary repetition of the doc-string

2fac888

fix: avoid false positives with markdown formatting in doc-strings

8682078

grunweg reviewed Feb 19, 2025

View reviewed changes

Comment thread Mathlib/Tactic/Linter/DocString.lean Outdated

Merge branch 'master' into adomani/docstring_linter

a0481ea

adomani commented Feb 20, 2025

View reviewed changes

adomani added 2 commits February 21, 2025 09:28

lint with position for start

fa0f476

lint only initial and terminal spaces, trailing commas

1430269

Add DTExpr.isSpecific doc-string

0cb99e5

grunweg reviewed Feb 27, 2025

View reviewed changes

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 27, 2025

adomani and others added 4 commits February 28, 2025 18:18

add comma test

2cb5901

Michael's suggestions

38f135d

Apply suggestions from code review

247c38f

Co-authored-by: grunweg <[email protected]>

Merge branch 'adomani/docstring_linter' of github.com:leanprover-comm…

3c0cf83

…unity/mathlib4 into adomani/docstring_linter

adomani commented Feb 28, 2025

View reviewed changes

adomani removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 28, 2025

grunweg reviewed Feb 28, 2025

View reviewed changes

Comment thread Mathlib/Tactic/Linter.lean Outdated

Comment thread Mathlib/Tactic/Linter/DocString.lean Outdated

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 28, 2025

adomani added 2 commits February 28, 2025 20:15

remove import in Linter.leam

80d4223

rename variable to endRange

ca47def

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 7, 2025

adomani added 3 commits March 7, 2025 10:46

Merge remote-tracking branch 'origin/master' into adomani/docstring_l…

ee8c367

…inter

final adjustments

00b3530

Merge remote-tracking branch 'origin/master' into adomani/docstring_l…

5b88905

…inter

ghost added the ready-to-merge This PR has been sent to bors. label Mar 7, 2025

mathlib-bors bot changed the title ~~feat: the doc-string linter~~ [Merged by Bors] - feat: the doc-string linter Mar 7, 2025

mathlib-bors bot closed this Mar 7, 2025

mathlib-bors bot deleted the adomani/docstring_linter branch March 7, 2025 14:33

Conversation

adomani commented Feb 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5b889058df

Import changes for modified files

Declarations diff

Uh oh!

adomani commented Feb 19, 2025

Uh oh!

Uh oh!

Uh oh!

adomani commented Feb 19, 2025

Uh oh!

adomani Feb 20, 2025

Choose a reason for hiding this comment

Uh oh!

grunweg 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!

grunweg commented Feb 27, 2025

Uh oh!

adomani left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

adomani commented Feb 28, 2025

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Feb 28, 2025

Uh oh!

PatrickMassot commented Mar 7, 2025

Uh oh!

mathlib-bors bot commented Mar 7, 2025

Uh oh!

adomani commented Mar 7, 2025

Uh oh!

mathlib-bors bot commented Mar 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

adomani commented Feb 19, 2025 •

edited

Loading

github-actions bot commented Feb 19, 2025 •

edited

Loading