Zulip Chat Archive

Stream: general

Topic: nolint doc


view this post on Zulip Patrick Massot (Oct 20 2019 at 20:03):

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

view this post on Zulip Rob Lewis (Oct 20 2019 at 20:42):

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

view this post on Zulip Patrick Massot (Mar 01 2020 at 09:26):

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.

view this post on Zulip Gabriel Ebner (Mar 01 2020 at 10:08):

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

view this post on Zulip Patrick Massot (Mar 01 2020 at 10:09):

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

view this post on Zulip Rob Lewis (Mar 01 2020 at 10:57):

It's not really a user facing thing.

view this post on Zulip Patrick Massot (Mar 01 2020 at 10:58):

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

view this post on Zulip Rob Lewis (Mar 01 2020 at 10:58):

Contributors can 100% ignore nolints.txt.

view this post on Zulip Rob Lewis (Mar 01 2020 at 10:58):

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

view this post on Zulip Rob Lewis (Mar 01 2020 at 10:59):

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

view this post on Zulip Patrick Massot (Mar 01 2020 at 11:01):

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

view this post on Zulip Rob Lewis (Mar 01 2020 at 11:07):

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.

view this post on Zulip Rob Lewis (Mar 01 2020 at 11:08):

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

view this post on Zulip Rob Lewis (Mar 01 2020 at 11:10):

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.


Last updated: May 06 2021 at 20:13 UTC