PR !4#19322: test: rebuild modifying lint

Stream: triage

[Random Issue Bot]

Today I chose PR #19322 for discussion!

test: rebuild modifying lint
Created by @damiano (@adomani) on 2024-11-21
Labels: merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

[Damiano Testa]

Closed as no longer relevant: the docPrime linter is no longer active.

[Ruben Van de Velde]

Why not though?

[Damiano Testa]

I can look into reinstating the docPrime linter.

[Damiano Testa]

I had disabled it because it was too annoying for... I don't remember what!

[Damiano Testa]

It is certainly true that it was, on purpose, very hard to silence, unless you actually wrote a doc-string. There was some missing interaction between the lean files and the relevant nolints file that had caused some headaches.

[Damiano Testa]

Maybe this was the issue: projects downstream of mathlib were getting the linter warnings on mathlib files?

[Violeta Hernández]

I think the issue is not everyone wanted it.