[Merged by Bors] - feat: separate linter error message for empty doc-strings#27895
Closed
grunweg wants to merge 3 commits intoleanprover-community:masterfrom
Closed
[Merged by Bors] - feat: separate linter error message for empty doc-strings#27895grunweg wants to merge 3 commits intoleanprover-community:masterfrom
grunweg wants to merge 3 commits intoleanprover-community:masterfrom
Conversation
PR summary 3d31f1f2b1Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 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 No changes to technical debt.You can run this locally as
|
3 tasks
adomani
approved these changes
Aug 14, 2025
Contributor
adomani
left a comment
There was a problem hiding this comment.
This looks straightforward, thanks!
I have just two questions.
- Did you
bench!it? I can't see how it would have a noticeable effect, but it is still good to test. - Out of curiosity, did this catch anything besides the ever-present exceptions? What would happen if you linted for doc-strings whose trimmed length is at most 1?
Contributor
Author
|
!bench |
Contributor
Author
|
Thanks for the review. I didn't benchmark this yet (good idea!); let's see what happens. |
Contributor
Author
|
As you see from the diff, this linter didn't find anything else. I could test for doc-strings whose trimmed length is at most 1 (i.e., also catch a doc-string |
Contributor
|
I don't think that there will be one-letter doc-strings and, if they existed, I do not think that they are useful! However, I do wonder about what is the minimum length of a "useful" doc-string. |
Contributor
Author
|
💡 So, I could certain lint for doc-strings with fewer than e.g. 20 trimmed characters, just to see what this finds. |
Contributor
|
Take a look at this: $ git grep '/-- *[^ ]* *-/'
Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean: /-- generators -/
Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean: /-- relations -/
Mathlib/CategoryTheory/Monoidal/Functor.lean: /-- tensorator -/
Mathlib/Order/Filter/AtTopBot/Group.lean:/-- $\lim_{x\to+\infty}|x|_m=+\infty$ -/
Mathlib/Order/Filter/AtTopBot/Group.lean:@[to_additive /-- $\lim_{x\to+\infty}|x|=+\infty$ -/]
Mathlib/Order/Filter/AtTopBot/Group.lean:/-- $\lim_{x\to\infty^{-1}|x|_m=+\infty$ -/
Mathlib/Order/Filter/AtTopBot/Group.lean:@[to_additive /-- $\lim_{x\to-\infty}|x|=+\infty$ -/]
Mathlib/Tactic/AdaptationNote.lean: logError "Adaptation notes must be followed by a /-- comment -/"
Mathlib/Tactic/DepRewrite.lean: /-- Configuration. -/
Mathlib/Tactic/FunProp/Decl.lean:/-- -/
Mathlib/Tactic/FunProp/Mor.lean: /-- -/
Mathlib/Tactic/FunProp/Theorems.lean: /-- priority -/
Mathlib/Tactic/FunProp/Theorems.lean:/-- -/
Mathlib/Tactic/FunProp/Theorems.lean:/-- -/
Mathlib/Tactic/FunProp/Theorems.lean:/-- -/
Mathlib/Tactic/FunProp/Types.lean: /-- priority -/
Mathlib/Tactic/FunProp/Types.lean: /-- -/
Mathlib/Tactic/ToAdditive/Frontend.lean: docstring syntax instead (e.g. `@[to_additive /-- example -/]`)"
Mathlib/Topology/ContinuousMap/Defs.lean: /-- Continuity -/
MathlibTest/CommandStart.lean:/-- A -/
MathlibTest/CommandStart.lean: /-- A -/
MathlibTest/UnusedTactic.lean: #adaptation_note /-- hi -/
MathlibTest/linarith.lean:/-- https://github.com/leanprover-community/mathlib4/issues/8875 -/
MathlibTest/linarith.lean:/-- https://github.com/leanprover-community/mathlib4/issues/2717 -/
MathlibTest/linarith.lean:/-- https://github.com/leanprover-community/mathlib4/issues/8875 -/
MathlibTest/linarith.lean:/-- https://github.com/leanprover-community/mathlib4/issues/2717 -/
MathlibTest/toAdditive.lean:Use docstring syntax instead (e.g. `@[to_additive /-- example -/]`)this is not the same as having at most 20 characters, but it is still somewhat interesting. |
Contributor
Author
|
Indeed! Most of these could and should be expanded a bit - but I'm not sure if always linting them is useful. |
Collaborator
|
Here are the benchmark results for commit 4c91053. Benchmark Metric Change
==========================================================
+ build linting -5.1%
+ ~Mathlib.Topology.Separation.Basic instructions -22.5% |
2 files, Instructions +7.0⬝10⁹
5 files, Instructions +6.0⬝10⁹
4 files, Instructions +5.0⬝10⁹
13 files, Instructions +4.0⬝10⁹
55 files, Instructions +3.0⬝10⁹
84 files, Instructions +2.0⬝10⁹
434 files, Instructions +1.0⬝10⁹
402 files, Instructions -2.0⬝10⁹
68 files, Instructions -3.0⬝10⁹
62 files, Instructions -4.0⬝10⁹
10 files, Instructions -5.0⬝10⁹
2 files, Instructions -6.0⬝10⁹
4 files, Instructions -7.0⬝10⁹
|
Contributor
Author
|
These benchmark results look like a lot of noise, and probably no really bad effect. What do you think? |
Contributor
|
Thanks! bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Aug 14, 2025
While functionally empty doc-strings are already linted for today, this provides a clearer error message. Unlike the `docString` linter, this linter is enabled by default.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
Julian
added a commit
to Aaron1011/mathlib4
that referenced
this pull request
Aug 16, 2025
* origin/master: (508 commits) feat(Logic/Basic): forall_and_index (leanprover-community#27737) feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021) feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000) chore: more elementary Motzkin polynomial proof (leanprover-community#28482) feat: e-seminormed monoid (leanprover-community#27385) feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171) fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513) chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504) feat(RingTheory): invertible modules and Picard group (leanprover-community#25337) chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498) feat: add bilinear maps for vector/matrix products (leanprover-community#28130) feat(Counterexamples): topologists' sine curve (leanprover-community#25833) feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453) chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436) feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285) feat: make `ring` work for semifields (leanprover-community#28494) feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295) chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270) refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450) feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120) feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667) chore(*): address a few timeout-related porting notes (leanprover-community#28483) feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238) feat(Shrink): `IsCancelMul` instance (leanprover-community#28407) chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485) feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087) chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554) feat(RingTheory): faithfully flat ring maps (leanprover-community#24530) chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656) chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459) feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816) feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213) chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402) feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030) chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454) chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962) feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582) feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039) feat: tactic analysis framework (leanprover-community#26683) chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424) feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413) chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231) chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202) feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885) chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660) feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255) chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438) chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431) feat: separate linter error message for empty doc-strings (leanprover-community#27895) feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497) ...
Paul-Lez
pushed a commit
to Paul-Lez/mathlib4
that referenced
this pull request
Aug 23, 2025
…-community#27895) While functionally empty doc-strings are already linted for today, this provides a clearer error message. Unlike the `docString` linter, this linter is enabled by default.
pechersky
pushed a commit
to pechersky/mathlib4
that referenced
this pull request
Aug 25, 2025
…-community#27895) While functionally empty doc-strings are already linted for today, this provides a clearer error message. Unlike the `docString` linter, this linter is enabled by default.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
While functionally empty doc-strings are already linted for today, this provides a clearer error message.
Unlike the
docStringlinter, this linter is enabled by default.