Zulip Chat Archive

Stream: general

Topic: linting the core library


Bryan Gin-ge Chen (Apr 29 2020 at 16:47):

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 (Apr 29 2020 at 16:48):

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 (Apr 29 2020 at 16:48):

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

Rob Lewis (Apr 29 2020 at 16:49):

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 (Apr 29 2020 at 16:50):

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 (Apr 29 2020 at 16:53):

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 (Apr 29 2020 at 16:58):

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

Rob Lewis (Apr 29 2020 at 16:59):

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

Gabriel Ebner (Apr 29 2020 at 17:05):

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 (Apr 29 2020 at 17:07):

Alternatively: core CI also checks mathlib...

Rob Lewis (Apr 29 2020 at 17:08):

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 (Apr 29 2020 at 17:09):

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

Johan Commelin (Apr 29 2020 at 17:09):

But I get your point

Rob Lewis (Apr 29 2020 at 18:52):

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

Rob Lewis (Apr 29 2020 at 18:54):

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

Rob Lewis (Apr 29 2020 at 18:55):

(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 (Apr 29 2020 at 19:07):

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 (Apr 29 2020 at 19:30):

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?


Last updated: Dec 20 2023 at 11:08 UTC