linting in CI

Stream: general

[Rob Lewis]

#1634 proposes adding a full linting check to the CI for mathlib pull requests. Right now we have linters that check for missing doc strings, bad instance priorities, illegal constants in types, and some other things. Putting this in a CI check will give contributors faster feedback and remove some burden from PR reviewers.

Since mathlib still fails some of these checks spectacularly, we can't run the test over the whole library yet. We can get around it by generating a list of failing declarations and whitelisting them right before we run the check. It's a little inelegant, but I'm not sure of a better way to do this without making all of mathlib compliant. (Obviously I'd like to get there eventually. It's a long road.)

Any more thoughts or feedback here?

[Johan Commelin]

I'm in favour of your proposal (unless it blows up the time that Travis spends on checking a PR).

[Rob Lewis]

I'm in favour of your proposal (unless it blows up the time that Travis spends on checking a PR).

It doesn't. Should add at most a few minutes.

[Mario Carneiro]

In the metamath set.mm repo we do something similar. There is a list of theorems whose use is "discouraged", meaning that you are allowed to reference them but there is an extra "I know what I'm doing" step. To accomplish this, we autogenerate a list of all theorems referencing discouraged theorems and check it in, and the CI regenerates the file and requires that it match. This means that if you want to get CI to pass, you have to also update the discouraged file, and this update shows in the git history.

If we apply this to the mathlib lints, it suggests making a list of all excluded lints and checking it into the repo. Then if you add anything beyond what is in the list you don't pass CI, unless you also update the excluded list, and this gives PR reviewers a place to heckle you.

[Rob Lewis]

That's exactly the proposed setup. nolints.txt is stored in the scripts directory. Adding something noncompliant means you have to either touch that file or use the nolint attribute, both of which should be obvious in a PR.

[Mario Carneiro]

ah, okay it wasn't clear to me that the txt file is actually checked in

[Rob Lewis]

I should have linked #1636 too. It's easy to autogenerate it.

[Rob Lewis]

It has to be checked in, because Travis can't generate the list of "acceptable" failing lints itself. It would have to find the root commit of the PR, build it, and generate the list there. That would basically double the time of the Travis check.

[Mario Carneiro]

even if you could do that, I wouldn't recommend it. It is too brittle, "the last commit" is not very well defined

[Rob Lewis]

(oops, that example isn't right)

[Rob Lewis]

There are situations where good PRs will break the tests. Renaming/refactoring, of course, but also:

Suppose def f {T : Type} [group T] (t : T) := t and theorem g {T : Type} [group T] (t : T) : f t = t := rfl. f will end up on the list because the group instance is unused, but g won't. If someone fixes f, the test will fail because g now has an unused argument.

I think these won't happen accidentally though. It should be obvious to reviewers what's going on.

[Rob Lewis]

#1636 is merged and the whitelist is added. #1634 is updated.

[Rob Lewis]

If anything gets merged to master before #1634, we'll need to update the whitelist once that lands.

[Rob Lewis]

Are we ready to merge #1634?

[Rob Lewis]

nolints.txt will have to be updated first, but that's easy enough.

[Rob Lewis]

I'm thinking it might be better to remove the instance_priority test from linting at first. I started a branch a little while ago to see how hard it would be to pass that test, and it seemed tricky. There were some unexpected errors. It would be safer to investigate that first before adding it to CI.

[Rob Lewis]

#1634 has landed. What this means for you: Travis will complain about your PRs if they add declarations that don't pass our linting tests. This means that all definitions must have doc strings, there should be no unused arguments to declarations, you have to use def and lemma/theorem in the right places, and a few other things.

[Rob Lewis]

If your PR adds something that fails a test, but you think it should be allowed anyway, you can use the @[nolint] attribute, with a comment justifying its use. Reviewers should look for this and question whether it's really necessary.

[Rob Lewis]

PRs that rename a lot of existing declarations could lead to failures. The solution here is to regenerate scripts/nolints.txt using scripts/mk_nolint.lean. We'll see in practice how often this is necessary.

[Sebastien Gouezel]

#1700 has just failed the linting test, and therefore it hasn't been merged. This shows that the set up works fine!