refactor(tactic/lint): split into multiple files (#2299)

The `lint.lean` file is getting too long for me to comfortably navigate.  This PR splits the file up into several parts:
 * `tactic.lint.basic` defining the `linter` structure and the `@[linter]` and `@[nolint]` attributes
 * `tactic.lint.frontend` defined the functions to run the linters and the various `#lint` commands
 * The linters are split into three separate files, the simp linters, the type class linters, and the rest.
 * `tactic.lint` imports all of the files above so `import tactic.lint` still works as before

src/tactic/lint/basic.lean

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
+-/
+import tactic.core
+
+/-!
+# Basic linter types and attributes
+
+This file defines the basic types and attributes used by the linting
+framework.  A linter essentially consists of a function
+`declaration → tactic (option string)`, this function together with some
+metadata is stored in the `linter` structure. We define two attributes:
+
+ * `@[linter]` applies to a declaration of type `linter` and adds it to the default linter set.
+
+ * `@[nolint linter_name]` omits the tagged declaration from being checked by
+   the linter with name `linter_name`.
+-/
+
+open tactic
+setup_tactic_parser
+
+-- Manual constant subexpression elimination for performance.
+private meta def linter_ns := `linter
+private meta def nolint_infix := `_nolint
+
+/--
+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:
+
+```lean
+meta def bar._nolint.foo : unit := ()
+```
+-/
+private meta def mk_nolint_decl_name (decl : name) (linter : name) : name :=
+(decl ++ nolint_infix) ++ linter
+
+/-- Defines the user attribute `nolint` for skipping `#lint` -/
+@[user_attribute]
+meta def nolint_attr : user_attribute _ (list name) :=
+{ name := "nolint",
+  descr := "Do not report this declaration in any of the tests of `#lint`",
+  after_set := some $ λ n _ _, (do
+    ls@(_::_) ← nolint_attr.get_param n
+      | fail "you need to specify at least one linter to disable",
+    ls.mmap' $ λ l, do
+      get_decl (linter_ns ++ l) <|> fail ("unknown linter: " ++ to_string l),
+      try $ add_decl $ declaration.defn (mk_nolint_decl_name n l) []
+        `(unit) `(unit.star) (default _) ff),
+  parser := ident* }
+
+add_tactic_doc
+{ name                     := "nolint",
+  category                 := doc_category.attr,
+  decl_names               := [`nolint_attr],
+  tags                     := ["linting"] }
+
+/-- `should_be_linted linter decl` returns true if `decl` should be checked
+using `linter`, i.e., if there is no `nolint` attribute. -/
+meta def should_be_linted (linter : name) (decl : name) : tactic bool := do
+e ← get_env,
+pure $ ¬ e.contains (mk_nolint_decl_name decl linter)
+
+/--
+A linting test for the `#lint` command.
+
+`test` defines a test to perform on every declaration. It should never fail. Returning `none`
+signifies a passing test. Returning `some msg` reports a failing test with error `msg`.
+
+`no_errors_found` is the message printed when all tests are negative, and `errors_found` is printed
+when at least one test is positive.
+
+If `is_fast` is false, this test will be omitted from `#lint-`.
+
+If `auto_decls` is true, this test will also be executed on automatically generated declarations.
+-/
+meta structure linter :=
+(test : declaration → tactic (option string))
+(no_errors_found : string)
+(errors_found : string)
+(is_fast : bool := tt)
+(auto_decls : bool := ff)
+
+/-- Takes a list of names that resolve to declarations of type `linter`,
+and produces a list of linters. -/
+meta def get_linters (l : list name) : tactic (list (name × linter)) :=
+l.mmap (λ n, prod.mk n.last <$> (mk_const n >>= eval_expr linter)
+  <|> fail format!"invalid linter: {n}")
+
+/-- Defines the user attribute `linter` for adding a linter to the default set.
+Linters should be defined in the `linter` namespace.
+A linter `linter.my_new_linter` is referred to as `my_new_linter` (without the `linter` namespace)
+when used in `#lint`.
+-/
+@[user_attribute]
+meta def linter_attr : user_attribute unit unit :=
+{ name := "linter",
+  descr := "Use this declaration as a linting test in #lint",
+  after_set := some $ λ nm _ _,
+                mk_const nm >>= infer_type >>= unify `(linter) }
+
+add_tactic_doc
+{ name                     := "linter",
+  category                 := doc_category.attr,
+  decl_names               := [`linter_attr],
+  tags                     := ["linting"] }

src/tactic/lint/default.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
+-/
+
+import tactic.lint.frontend
+  tactic.lint.simp
+  tactic.lint.type_classes
+  tactic.lint.misc
+
+open tactic
+
+add_tactic_doc
+{ name                     := "linting commands",
+  category                 := doc_category.cmd,
+  decl_names               := [`lint_cmd, `lint_mathlib_cmd, `lint_all_cmd, `list_linters],
+  tags                     := ["linting"],
+  description              :=
+"User commands to spot common mistakes in the code
+
+* `#lint`: check all declarations in the current file
+* `#lint_mathlib`: check all declarations in mathlib (so excluding core or other projects,
+  and also excluding the current file)
+* `#lint_all`: check all declarations in the environment (the current file and all
+  imported files)
+
+The following linters are run by default:
+1. `unused_arguments` checks for unused arguments in declarations.
+2. `def_lemma` checks whether a declaration is incorrectly marked as a def/lemma.
+3. `dup_namespce` checks whether a namespace is duplicated in the name of a declaration.
+4. `ge_or_gt` checks whether ≥/> is used in the declaration.
+5. `instance_priority` checks that instances that always apply have priority below default.
+6. `doc_blame` checks for missing doc strings on definitions and constants.
+7.  `has_inhabited_instance` checks whether every type has an associated `inhabited` instance.
+8.  `impossible_instance` checks for instances that can never fire.
+9.  `incorrect_type_class_argument` checks for arguments in [square brackets] that are not classes.
+10. `dangerous_instance` checks for instances that generate type-class problems with metavariables.
+11. `fails_quickly` tests that type-class inference ends (relatively) quickly when applied to variables.
+12. `has_coe_variable` tests that there are no instances of type `has_coe α t` for a variable `α`.
+13. `inhabited_nonempty` checks for `inhabited` instance arguments that should be changed to `nonempty`.
+14. `simp_nf` checks that the left-hand side of simp lemmas is in simp-normal form.
+15. `simp_var_head` checks that there are no variables as head symbol of left-hand sides of simp lemmas.
+16. `simp_comm` checks that no commutativity lemmas (such as `add_comm`) are marked simp.
+
+Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
+This is not run by default.
+
+The command `#list_linters` prints a list of the names of all available linters.
+
+You can append a `*` to any command (e.g. `#lint_mathlib*`) to omit the slow tests (4).
+
+You can append a `-` to any command (e.g. `#lint_mathlib-`) to run a silent lint
+that suppresses the output of passing checks.
+A silent lint will fail if any test fails.
+
+You can append a sequence of linter names to any command to run extra tests, in addition to the
+default ones. e.g. `#lint doc_blame_thm` will run all default tests and `doc_blame_thm`.
+
+You can append `only name1 name2 ...` to any command to run a subset of linters, e.g.
+`#lint only unused_arguments`
+
+You can add custom linters by defining a term of type `linter` in the `linter` namespace.
+A linter defined with the name `linter.my_new_check` can be run with `#lint my_new_check`
+or `lint only my_new_check`.
+If you add the attribute `@[linter]` to `linter.my_new_check` it will run by default.
+
+Adding the attribute `@[nolint doc_blame unused_arguments]` to a declaration
+omits it from only the specified linter checks." }
+
+/-- The default linters used in mathlib CI. -/
+meta def mathlib_linters : list name := by do
+ls ← get_checks tt [] ff,
+let ls := ls.map (λ ⟨n, _⟩, `linter ++ n),
+exact (reflect ls)