nolint doc

Stream: general

[Patrick Massot]

Am I missing something or the nolint attribute is not documented?

[Rob Lewis]

Hmm, looks like not. I just renamed sanity_skip in the recent PR so I guess there was no doc for that either.

[Patrick Massot]

I just updated https://github.com/leanprover-community/mathlib/pull/2069 to fix two issues reported by the linter. I took the opportunity to fix other issues in filter.basic which were marked in https://github.com/leanprover-community/mathlib/blob/19a9bdc23efc4fa9fcf10d1adfdc3929c5328c0f/scripts/nolints.txt#L2541-L2549. Do I understand correctly that some robot will automatically remove these lines after merging this PR? Is this documented somewhere? I couldn't even find nolints.txt in https://leanprover-community.github.io/mathlib_docs/commands.html#lint or anywhere else.

[Gabriel Ebner]

Do I understand correctly that some robot will automatically remove these lines after merging this PR?

Yes, indeed. Until three weeks ago Rob did this manually, but now it is updated after every commit to master. I don't think there's any documentation except the original PR: https://github.com/leanprover-community/mathlib/pull/1979

[Patrick Massot]

Ok, I'll wait to see it in action and then PR some doc.

[Rob Lewis]

It's not really a user facing thing.

[Patrick Massot]

It's maintainer facing at least. Maybe we should have doc specifically targeting maintainers

[Rob Lewis]

Contributors can 100% ignore nolints.txt.

[Rob Lewis]

Sure, we should write down the details of the CI/merge process somewhere.

[Rob Lewis]

But the nolints.txt stuff only matters if you want to change the CI process.

[Patrick Massot]

Yes, but we do change the CI process from time to times.

[Rob Lewis]

The short summary is, mk_nolints.lean is a script that runs the linters and makes a list of which declarations fails which tests. If you run mk_all.sh with the right flag, it will generate an extra file that adds @[nolint] to each declaration in this list, and import this in lint_mathlib.lean.

[Rob Lewis]

So any declaration that failed a lint test at the time mk_nolints was run is ignored by that test in lint_mathlib.

[Rob Lewis]

We only run mk_nolints on master. So errors that appear in PRs aren't on the list, but errors that already exist in mathlib are. If errors get fixed, they're removed from the list as soon as the master build finishes.