feat(tactic/lint): support @[nolint unused_arguments]

[gebner]

We have so many linters now and @[nolint] disables all of them. This PR adds parameters to the nolint attribute so that you can selectively disable some lints only:

@[nolint def_lemma] -- TODO: This should be a theorem but Lean fails to synthesize the placeholder
def div_def (a) {b : ordinal} (h : b ≠ 0) :

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[bryangingechen]

Could you update docs/commands.md?

[jcommelin]

Should it even be the default that nolint disables nothing, and the linters that are to be disabled MUST be listed explicitly?

[urkud]

Should it even be the default that nolint disables nothing, and the linters that are to be disabled MUST be listed explicitly?

This behavior is not the "least surprising". If we want to force users to specify disabled linters explicitly, then @[nolint] with no parameters should fail.

[gebner]

I think I introduced a performance issue when refactoring the linting code. The linters now take 30 minutes instead of 12. I'm debugging it now.

Could you update docs/commands.md?

Done.

[...] the linters that are to be disabled MUST be listed explicitly?
[...] then @[nolint] with no parameters should fail.

I agree. The only reason it did not fail was because of the nolints.txt file, which added nolint without specifying the linter. I have now updated the mk_nolints.lean file, and I'll then make @[nolints] an error.

[gebner]

I think I introduced a performance issue when refactoring the linting code.

The performance issue was due to using user attributes with parameters. I'm using the obvious fix now:

/--
Computes the declaration name used to store the nolint attribute data.

Retrieving the parameters for user attributes is *extremely* slow.
Hence we store the parameters of the nolint attribute as declarations
in the environment.  E.g. for `@[nolint foo] def bar := _` we add the
following declaration:

meta def bar._nolint.foo : unit := ()
-/
private meta def mk_nolint_decl_name (decl : name) (linter : name) : name :=
(decl ++ nolint_infix) ++ linter

As requested, @[nolint] is now an error. You always need to specify the linters you want to disable. I've also refactored the mk_nolint.lean script; the nolints.txt file is now grouped by filename. Maybe this makes it more attractive for people to just pick a file and fix all the linting errors there?

-- data/dfinsupp.lean
apply_nolint decidable_zero_symm doc_blame
apply_nolint dfinsupp doc_blame
apply_nolint dfinsupp.decidable_eq unused_arguments
apply_nolint dfinsupp.erase doc_blame
apply_nolint dfinsupp.lmk doc_blame
apply_nolint dfinsupp.lsingle doc_blame
apply_nolint dfinsupp.map_range_def unused_arguments
apply_nolint dfinsupp.map_range_single unused_arguments
apply_nolint dfinsupp.mk doc_blame
apply_nolint dfinsupp.pre doc_blame has_inhabited_instance
apply_nolint dfinsupp.single doc_blame
apply_nolint dfinsupp.subtype_domain_sum unused_arguments
apply_nolint dfinsupp.sum_apply unused_arguments
apply_nolint dfinsupp.support doc_blame
apply_nolint dfinsupp.to_has_scalar doc_blame
apply_nolint dfinsupp.to_module doc_blame
apply_nolint dfinsupp.zip_with doc_blame
apply_nolint dfinsupp.zip_with_def unused_arguments

-- data/dlist/basic.lean
apply_nolint dlist.join doc_blame

[robertylewis]

@[nolint doc_blame] is saying this def is permanently allowed to not have a doc string. Could you either add a doc string, or add it to nolints.txt (temporary permission to not have a doc string)? Same for map below. The examples in ordinal are a little different since morally they're lemmas, not defs.

I'd suggest a doc string but honestly I'm not sure what this is for.

[gebner]

Good point! I've added a docstring for const, but the rest of the file is a bit of a mystery to me as well. I've got no idea what add_const is for.

[PatrickMassot]

Maybe @cipher1024 could help here.