inherit_doc on projections

Stream: mathlib4

[Eric Wieser]

Can we add a linter to protect against the documentation mess at docs#CategoryTheory.Limits.Bicone ? The docs tell me the same thing 5 times

[Eric Wieser]

The culprit is

attribute [inherit_doc Bicone] Bicone.pt Bicone.π Bicone.ι Bicone.ι_π

which I think is a sloppy attempt to silence the doc linter

[Damiano Testa]

Well, the attempt was successful...

[Eric Wieser]

Well, not really since the linter was globally disabled at the time it was written anyway...

[Damiano Testa]

Is the proposal that the linter would prevent assigning the same docs to a field of a structure?

[Eric Wieser]

Yes, that seems like something that is never the right thing to do

[Damiano Testa]

The linter could be called docs.WellFounded.

[Damiano Testa]

The empty string counts as a doc-string:

import Std

/---/
def IamDocumented : Nat := 0

#lint
/-
-- Found 0 errors in 1 declarations (plus 2 automatically generated ones) in the current file with 12 linters


-- All linting checks passed!
-/

Should this be disallowed? My idea of doc-string is that there will be something to read and there is not much reading to do with the empty string.

[Kevin Buzzard]

Reid always argued that an empty docstring was better than a docstring written just to shut a linter up by someone who didn't know or care about the material

[Damiano Testa]

I wonder if every time that we hover over an empty doc-strings, Chat-GPT could make a new attempt at describing the object, until we are happy with the outcome.

[Eric Wieser]

Kevin Buzzard said:

Reid always argued that an empty docstring was better than a docstring written just to shut a linter up by someone who didn't know or care about the material

This situation should never happen; if the linter is complaining about a missing docstring, it is because the definition was added by the very person who should be writing the docstring! And if they don't know about the material, they shouldn't be the one to PR it...

[Kevin Buzzard]

This was not at all the case during the port though; people ported "the next file on the list" regardless of whether they knew the material, and fields of structures did not have to be docstringed in Lean 3.

[Eric Wieser]

They didn't in lean4 either, for most of the port

[Eric Wieser]

People got confused by #lint which was much stricter than CI and told people to do things we didn't actually want them to do