import linter failure

Stream: mathlib4

[Peter Nelson]

#13960 is failing the unused imports linter, which is flagging a redundant import that isn't actually redundant. The file is importing Data.Set.Subset in order to use the down-arrow notation for coercion preimage of sets. But (probably because I'm not using any theorems from that file) it's being flagged as a warning - see
https://github.com/leanprover-community/mathlib4/actions/runs/9586738790/job/26435306567?pr=13960

[Damiano Testa]

So, then "lake exe shake --update to ignore" is the way to go!

[Peter Nelson]

I can do that, but shouldn't the linter be fixed so this doesn't happen?

[Yaël Dillies]

It's really quite hard to improve the linter here

[Peter Nelson]

So much that it isn’t worth doing?

[Peter Nelson]

I've just encountered this problem again with a different PR that imports Data.Set.Subset for the notation. I suspect that a good number of imports of this file will have the same issue. By the time the linter makes the suggestion, it adds up to an hour or so of extra waiting to sort out the PR.

Would it be possible for the lake exe shake to include global exceptions for usual suspects like Data.Set.Subset? Could it in some cases try building with the suggested change to see if things break before issuing the suggestion? I don't know how technically feasible this last suggestion is.

[Ruben Van de Velde]

I think there's a part of noshake.json for that, yeah

[Peter Nelson]

Did I do this right? #14196

[Ruben Van de Velde]

I think so