runLinter --update

Stream: mathlib4

[Thomas Murrills]

(Other aside: it looks to me like the existing runLinter --update doesn't work as intended? It just writes the declarations that failed to the nolint file. It should presumably only be writing failing declarations already in the nolints file to the nolints file, right?)

[Thomas Murrills]

Thomas Murrills said:

Other aside: it looks to me like the existing runLinter --update doesn't work as intended?

(batteries#1600)

[Bryan Gin-ge Chen]

I can't remember exactly, but I seem to recall that the whole point of these update commands was to allow us to easily add new violations to the nolints file. Maybe I'm missing something though.

[Thomas Murrills]

Hmm, so maybe the docstring is wrong? It says it “removes any declarations that no longer need to be nolinted”.

I can imagine both functionalities would be useful…!

[Bryan Gin-ge Chen]

Ah, now that I read your explanation in batteries#1600 I understand your point. I guess I had never considered that case, but now I can imagine there being cases where we would want one behavior or the other.

[Notification Bot]

4 messages were moved here from #mathlib4 > slow linting step CI? by Bryan Gin-ge Chen.

[Notification Bot]

A message was moved here from #mathlib4 > slow linting step CI? by Bryan Gin-ge Chen.

[Thomas Murrills]

So, should we have two separate flags? Or --update!, even? Happy to make a PR for whatever design we want! :)

[Thomas Murrills]

(Note that I think the current “add new violations” behavior would also need a tweak: currently it erases nolints that pertain to modules which are not currently being linted. Not a problem when we only ever lint the one module, but in general… :upside_down:)

[Bryan Gin-ge Chen]

My guess is that the only regular user of the --update option right now is this workflow that runs weekly, so my instinct would be to just document this and then move on.

However, maybe this is also used when people add new linters. Are we typically using --update to populate the nolints file then too?

[Thomas Murrills]

Hmm, so that workflow effectively just so happens to do a cleanup instead of adding new nolints, because CI ensures there are no new violations, right? :grinning_face_with_smiling_eyes:

[Bryan Gin-ge Chen]

Yep, exactly!

[Thomas Murrills]

Gotcha!