linting the core library

Stream: general

[Bryan Gin-ge Chen]

This is a thread to discuss lean#200, which proposes linting the core library. I think it's a good idea. Should we have some guidelines for linting PRs? Also, any ideas for a good CI setup? @Gabriel Ebner

[Rob Lewis]

We definitely should lint core, but it's a little tricky I think. Ideally it would be part of core CI. But do we want to move the linter framework and definitions to core?

[Rob Lewis]

I'm not sure that's a good idea.

[Rob Lewis]

We could expand mathlib CI to also lint core, but then new errors don't show up until the version upgrade PRs to mathlib.

[Rob Lewis]

What do you mean by guidelines for linting PRs? There's nothing of the kind in mathlib afaik, and the graph shows we're doing a reasonable job of cleaning things up anyway.

[Bryan Gin-ge Chen]

Yeah, I guess I'm not sure what such guidelines would look like. Maybe just some suggestions on which linting errors to prioritize?

[Rob Lewis]

I think the easy change is just making mathlib CI also lint core. It's low effort and seems uncontroversial.

[Rob Lewis]

For graphing purposes I'd rather keep the mathlib and core nolints files separate, but that's completely an aesthetic thing...

[Gabriel Ebner]

I've mentioned this in the issue already, but I think it is better to run the linters in mathlib CI instead of core CI. There are some linters where declarations in mathlib can cause linting errors in core, and I'd like to catch these as well.

[Johan Commelin]

Alternatively: core CI also checks mathlib...

[Rob Lewis]

Johan Commelin said:

Alternatively: core CI also checks mathlib...

We want to be able to make non-backward compatible changes in core though.

[Johan Commelin]

We can still manually overrule the complaints of CI, right?

[Johan Commelin]

But I get your point

[Rob Lewis]

https://github.com/leanprover-community/mathlib/tree/lint-core

[Rob Lewis]

Question: is it possible that changes to mathlib will cause linter failures in core? These errors would be very annoying to fix.

[Rob Lewis]

(This should be a successful run. The next commit will move some declarations to another file that will force it to recompile everything.)

[Gabriel Ebner]

Rob Lewis said:

Question: is it possible that changes to mathlib will cause linter failures in core?

Yes. That's precisely why I'd like the linter to be run in mathlib. One concrete example: if you write a simp lemma that is already a simp lemma in core, then the duplicate lemma in core will get an linting error. This kind of error is easy to fix, namely in mathlib.
As a general policy I would suggest that it is OK to add declarations to nolints.txt as long as you open a PR to fix it in core.

[Rob Lewis]

I dunno, it doesn't really feel ergonomic. For one, it's best if people can ignore the nolints files completely just like they can ignore the rest of the CI stuff. It's confusing to tell people that the way to fix their PR is to edit some "read-only" file and make another PR to a different repo, no?