Configuring/modernizing runLinter

Stream: lean4

[Michael Rothgang]

Occasionally, I would like to configure the behaviour of runLinter, such as

• also run lint X (say, the docBlameThm linter)[1]
• only run lint X/omit lint Y (say, if I'm running on all of mathlib; the simpNF linters take a while on my computer)

In addition, the user experience of using runLinter can be improved: no --help output, no documentation what its inputs do. They are all somewhat obvious, but not quite. I remember looking for a way to do the above; it took me a while to figure out this was not possible.
Perhaps I have been spoilt by the Rust ecosystem, but I like my tools telling me right away what they can and cannot do!

The most apparent way to address both is to
(1) rewrite runLinter as a proper CLI app (instead of the ad hoc command line argument parsing it's doing today)
(2) add flags such as

• --print-linters: print the list of all linters it discovered and exit

• --add-linters: also run the following linters, even if they were disabled before
  (my use case: run a linter which is @[env_linter disabled], when I cannot or do not want to edit the project defining the linter)

• --exclude-linters X Y: do not run linters X or Y (say, for performance reasons or because I'm not interested in their output right now)

• --only-linters Z: only run linter Z (say, if I added this anew)

Is there any reasons to not do this? Are the longer-term plans in this area I should be aware of?
I have a prototype for this in a mathlib branch; if this is deemed useful, I'm happy to make a PR to batteries to improve runLinter there.)

[1] I can do so in individual files using the #lint docBlameThm command. I would like to run it on the whole project, however.

[Michael Rothgang]

To un-#xy: my original motivation was regenerating mathlib's nolints.json file locally. I know how to do this, but running all the simp linters takes a while. I can have my computer start this, cook dinner and have the results afterwards, but there ought to be a better way.
Another motivation was re-discovering the docBlameThm linter, which is disabled by default: I currently cannot run it on mathlib without editing core or batteries; this should not be necessary.

[Michael Rothgang]

Mathlib PR #14654 is a proof of concept PR for the UX I can imagine. Comments very welcome.

[Michael Rothgang]

batteries#881 makes first baby steps in this direction, by fixing the getChecks function

[Michael Rothgang]

Thanks for the comments and merging the batteries PR!

[Michael Rothgang]

In light of the discussion about the naming convention, I would like to rename runLinter (to be in kebab-case, for example).

At the same time, runLinter is slightly ambiguous, now that syntax linters exist and at least mathlib is gaining quite a few of them. Since runLinter runs all linters tagged with env_lint, how about renaming to env-lint? (I would perform this rename along with adding a warning to the old script, pointing out the rename. After perhaps a month or two, that warning can be removed.)
CC @Kim Morrison

[Kim Morrison]

I don't think env needs to be in the executable name. I think the plan is that we are going to transition to using lake lint (in fact, if I understand right we can already do this, but I'm on mobile and can't verify). It is meant to work just like @[test_driver] does for lake test.

[Kim Morrison]

The distinction between syntax and environment linters should be prominent in the documentation for both, but people who are just trying to use them don't need to know immediately.

[Kim Morrison]

That said, I guess it's no harm to rename the executable as you suggest, and then immediately hide it behind lake lint.

[Michael Rothgang]

Kim Morrison said:

That said, I guess it's no harm to rename the executable as you suggest, and then immediately hide it behind lake lint.

That would be my preferred solution also!

[Bryan Gin-ge Chen]

Sorry for bumping this old thread with something only tangentially related to the conversation.

Looking at the diff of our most recent mathlib4 automatic update nolints PR, it looks like lake exe runLinter --update writes a nolints.json file without a final newline. It'd be nice to fix that since anyone editing the file manually will most likely add a final newline character so this will just lead to diff noise. (This is of course hardly a huge deal, but I figured I'd post here while it was on my mind.)

Maybe if @Michael Rothgang 's runLinter rewrite is still forthcoming, this can be worked in somehow?

[Damiano Testa]

Bryan, does #17038 look like it might solve the issue? Sorry, I do not have time to test it now.

[Bryan Gin-ge Chen]

Hi Damiano, this is my first time looking at the lean code in that file, but isn't that PR touching code (in Mathlib/Tactic/Linter/TextBased.lean) which writes changes to the .lean file being linted and not the code where the nolints.json file containing exceptions is updated?

I could be wrong but I think the nolints.json file is generated with a missing final newline in scripts/runLinter.lean in batteries.

[Damiano Testa]

You're probably right. Then I think that the missing line break is here:

https://github.com/leanprover-community/batteries/blob/2ce0037d487217469a1efeb9ea8196fe15ab9c46/scripts%2FrunLinter.lean#L18

I remember fixing a similar issue with shake a while back.

[Damiano Testa]

I think that the JSON pretty-fier does not add a final line break to the file.

[Damiano Testa]

I've already switched off the computer for the night, though. If you want to add a .push '\n' yourself, feel free to do so! Otherwise, I'll do it tomorrow.

[Damiano Testa]

This is the analogous line in shake:

https://github.com/leanprover-community/mathlib4/blob/master/Shake%2FMain.lean#L538

[Damiano Testa]

batteries#955

I tested this locally and it seems to work as intended.

I am having some difficulty testing it in CI, though.

[Michael Rothgang]

That PR looks good to me - you got to it before I saw this thread in full :-)

[Bryan Gin-ge Chen]

It looks like the update nolints job is now saving a file ending in a newline: https://github.com/leanprover-community/mathlib4/pull/17245/files

Thanks Damiano! (I've closed #17038 for now.)