No docstring for structure

Stream: mathlib4

[Yaël Dillies]

I just found out that docs#Ring has no docstring! What happened there? :face_with_raised_eyebrow:

[Martin Dvořák]

I quickly skimmed the Git history of the Mathlib4 repo. It seems that the docstring was never there.

[Yaël Dillies]

What does docs3#ring say?

[Yaël Dillies]

It does have a docstring there. A porting misshap?

[Ruben Van de Velde]

I think Ring was ad-hoc ported really early

[Jireh Loreaux]

Oof, that hurts. I wonder how many docstrings we're missing as a result of that.

[Mario Carneiro]

we have a nolints.json which is supposed to be tracking this, but it seems to have grown a bit out of control during the port and we haven't taken the time to work it down again

[Matthew Ballard]

What happens if you replace with a blank copy?

[Mario Carneiro]

you get a ton of linter warnings that stop the build?

[Mario Carneiro]

It was recently trimmed down to only the ones that are still applicable in #9832

[Mario Carneiro]

so all of the remaining ones should be true positives

[Yaël Dillies]

Glad to know that the linter is doing its job, at least.

[Matthew Ballard]

I took a stab at this #9941 Have at it :)

[Yaël Dillies]

Ah, I just opened #9942 !

[Matthew Ballard]

That’s certainly more thorough