From 173e70a0c4cbbf525bb8fde62105084ad27f4572 Mon Sep 17 00:00:00 2001
From: Rob Lewis <Rob.y.lewis@gmail.com>
Date: Sat, 19 Oct 2019 21:57:42 +0200
Subject: [PATCH] feat(tactic/lint): rename and refactor sanity_check (#1556)

* chore(*): rename sanity_check to lint

* rename sanity_check files to lint

* refactor(tactic/lint): use attributes to add new linters

* feat(tactic/lint): restrict which linters are run

* doc(tactic/lint): document

* doc(tactic/lint): document list_linters

* chore(tactic/doc_blame): turn doc_blame into a linter

* remove doc_blame import

* fix(test/lint)

* feat(meta/rb_map): add name_set.insert_list

* feat(tactic/lint): better control over which linters are run

* ignore instances in doc_blame

* update lint documentation

* minor refactor

* correct docs

* correct command doc strings

* doc rb_map.lean

* consistently use key/value

* fix command doc strings
---
 docs/tactics.md                       |  49 ++--
 src/category/functor.lean             |   6 +-
 src/measure_theory/l1_space.lean      |   2 +-
 src/meta/rb_map.lean                  |  56 +++-
 src/tactic/basic.lean                 |   3 +-
 src/tactic/core.lean                  |   2 +-
 src/tactic/doc_blame.lean             |  33 ---
 src/tactic/interactive.lean           |   4 +-
 src/tactic/lint.lean                  | 384 ++++++++++++++++++++++++++
 src/tactic/sanity_check.lean          | 265 ------------------
 test/{sanity_check.lean => lint.lean} |  17 +-
 11 files changed, 477 insertions(+), 344 deletions(-)
 delete mode 100644 src/tactic/doc_blame.lean
 create mode 100644 src/tactic/lint.lean
 delete mode 100644 src/tactic/sanity_check.lean
 rename test/{sanity_check.lean => lint.lean} (84%)

diff --git a/docs/tactics.md b/docs/tactics.md
index 985dcee4d6ef1..8d7b9b1956413 100644
--- a/docs/tactics.md
+++ b/docs/tactics.md
@@ -1137,30 +1137,39 @@ Here too, the `reassoc` attribute can be used instead. It works well when combin
 ```lean
 attribute [simp, reassoc] some_class.bar
 ```
-### sanity_check
+### lint
 User commands to spot common mistakes in the code
 
-* `#sanity_check`: check all declarations in the current file
-* `#sanity_check_mathlib`: check all declarations in mathlib (so excluding core or other projects,
+* `#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)
-* `#sanity_check_all`: check all declarations in the environment (the current file and all
+* `#lint_all`: check all declarations in the environment (the current file and all
   imported files)
 
-Currently this will check for
+Five 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. `illegal_constant` checks whether ≥/> is used in the declaration
+5. `doc_blame` checks for missing doc strings on definitions and constants.
 
-1. unused arguments in declarations,
-2. whether a declaration is incorrectly marked as a def/lemma,
-3. whether a namespace is duplicated in the name of a declaration
-4. whether ≥/> is used in the declaration
+A sixth linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
+This is not run by default.
 
-You can append a `-` to any command (e.g. `#sanity_check_mathlib-`) to omit the slow tests (4).
+The command `#list_linters` prints a list of the names of all available linters.
 
-You can customize the performed checks like this:
-```lean
-meta def my_check (d : declaration) : tactic (option string) :=
-return $ if d.to_name = `foo then some "gotcha!" else none
-run_cmd sanity_check tt [(my_check, "found nothing", "found something")] >>= trace
-```
+You can append a `-` to any command (e.g. `#lint_mathlib-`) to omit the slow tests (4).
+
+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.
 
 ### lift
 
@@ -1195,12 +1204,12 @@ Lift an expression to another type.
 
 ### import_private
 
-`import_private foo from bar` finds a private declaration `foo` in the same file as `bar` and creates a 
-local notation to refer to it. 
-    
+`import_private foo from bar` finds a private declaration `foo` in the same file as `bar` and creates a
+local notation to refer to it.
+
 `import_private foo`, looks for `foo` in all (imported) files.
 
-When possible, make `foo` non-private rather than using this feature. 
+When possible, make `foo` non-private rather than using this feature.
 
 ### default_dec_tac'
 
diff --git a/src/category/functor.lean b/src/category/functor.lean
index 42e1cc09508de..c3f703c91e615 100644
--- a/src/category/functor.lean
+++ b/src/category/functor.lean
@@ -5,7 +5,7 @@ Author: Simon Hudon
 
 Standard identity and composition functors
 -/
-import tactic.ext tactic.sanity_check category.basic
+import tactic.ext tactic.lint category.basic
 
 universe variables u v w
 
@@ -42,7 +42,7 @@ def id.mk {α : Sort u} : α → id α := id
 
 namespace functor
 
-@[sanity_skip] def const (α : Type*) (β : Type*) := α
+@[nolint] def const (α : Type*) (β : Type*) := α
 
 @[pattern] def const.mk {α β} (x : α) : const α β := x
 
@@ -54,7 +54,7 @@ namespace const
 
 protected lemma ext {α β} {x y : const α β} (h : x.run = y.run) : x = y := h
 
-@[sanity_skip] protected def map {γ α β} (f : α → β) (x : const γ β) : const γ α := x
+@[nolint] protected def map {γ α β} (f : α → β) (x : const γ β) : const γ α := x
 
 instance {γ} : functor (const γ) :=
 { map := @const.map γ }
diff --git a/src/measure_theory/l1_space.lean b/src/measure_theory/l1_space.lean
index e19feab1a237f..87a267b293bfd 100644
--- a/src/measure_theory/l1_space.lean
+++ b/src/measure_theory/l1_space.lean
@@ -45,7 +45,7 @@ assume hfi hgi,
     ... < ⊤ : add_lt_top.2 ⟨hfi, hgi⟩
 
 -- We don't need `f` to be measurable here, but it's easier to have a uniform API
-@[sanity_skip]
+@[nolint]
 lemma lintegral_nnnorm_neg {f : α → γ} (hf : measurable f) :
   (∫⁻ (a : α), ↑(nnnorm ((-f) a))) = ∫⁻ (a : α), ↑(nnnorm ((f) a)) :=
 lintegral_congr_ae $ by { filter_upwards [], simp }
diff --git a/src/meta/rb_map.lean b/src/meta/rb_map.lean
index 91844e0138d12..8d3095e8e5110 100644
--- a/src/meta/rb_map.lean
+++ b/src/meta/rb_map.lean
@@ -2,22 +2,32 @@
 Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Robert Y. Lewis
-
-Additional operations on native rb_maps and rb_sets.
 -/
 import data.option.defs
 
+/-!
+# rb_map
+
+This file defines additional operations on native rb_maps and rb_sets.
+These structures are defined in core in `init.meta.rb_map`. They are meta objects,
+and are generally the most efficient dictionary structures to use for pure metaprogramming right now.
+-/
+
 namespace native
 namespace rb_set
 
+/-- `filter s P` returns the subset of elements of `s` satisfying `P`. -/
 meta def filter {key} (s : rb_set key) (P : key → bool) : rb_set key :=
 s.fold s (λ a m, if P a then m else m.erase a)
 
+/-- `mfilter s P` returns the subset of elements of `s` satisfying `P`,
+where the check `P` is monadic. -/
 meta def mfilter {m} [monad m] {key} (s : rb_set key) (P : key → m bool) : m (rb_set key) :=
 s.fold (pure s) (λ a m,
   do x ← m,
      mcond (P a) (pure x) (pure $ x.erase a))
 
+/-- `union s t` returns an rb_set containing every element that appears in either `s` or `t`. -/
 meta def union {key} (s t : rb_set key) : rb_set key :=
 s.fold t (λ a t, t.insert a)
 
@@ -25,19 +35,29 @@ end rb_set
 
 namespace rb_map
 
-meta def find_def {α β} (x : β) (m : rb_map α β) (k : α) :=
-(m.find k).get_or_else x
+/-- `find_def default m k` returns the value corresponding to `k` in `m`, if it exists.
+Otherwise it returns `default`. -/
+meta def find_def {key value} (default : value) (m : rb_map key value) (k : key) :=
+(m.find k).get_or_else default
 
-meta def insert_cons {α β} [has_lt α] (k : α) (x : β) (m : rb_map α (list β)) : rb_map α (list β) :=
+/-- `insert_cons k x m` adds `x` to the list corresponding to key `k`. -/
+meta def insert_cons {key value} [has_lt key] (k : key) (x : value) (m : rb_map key (list value)) :
+  rb_map key (list value) :=
 m.insert k (x :: m.find_def [] k)
 
-meta def ifind {α β} [inhabited β] (m : rb_map α β) (a : α) : β :=
-(m.find a).iget
+/-- `ifind m key` returns the value corresponding to `key` in `m`, if it exists.
+Otherwise it returns the default value of `value`. -/
+meta def ifind {key value} [inhabited value] (m : rb_map key value) (k : key) : value :=
+(m.find k).iget
 
-meta def zfind {α β} [has_zero β] (m : rb_map α β) (a : α) : β :=
-(m.find a).get_or_else 0
+/-- `zfind m key` returns the value corresponding to `key` in `m`, if it exists.
+Otherwise it returns 0. -/
+meta def zfind {key value} [has_zero value] (m : rb_map key value) (k : key) : value :=
+(m.find k).get_or_else 0
 
-meta def add {α β} [has_add β] [has_zero β] [decidable_eq β] (m1 m2 : rb_map α β) : rb_map α β :=
+/-- Returns the pointwise sum of `m1` and `m2`, treating nonexistent values as 0. -/
+meta def add {key value} [has_add value] [has_zero value] [decidable_eq value]
+  (m1 m2 : rb_map key value) : rb_map key value :=
 m1.fold m2
   (λ n v m,
    let nv := v + m2.zfind n in
@@ -46,15 +66,19 @@ m1.fold m2
 variables {m : Type → Type*} [monad m]
 open function
 
+/-- `mfilter P s` filters `s` by the monadic predicate `P` on keys and values. -/
 meta def mfilter {key val} [has_lt key] [decidable_rel ((<) : key → key → Prop)]
   (P : key → val → m bool) (s : rb_map key val) : m (rb_map.{0 0} key val) :=
 rb_map.of_list <$> s.to_list.mfilter (uncurry P)
 
+/-- `mmap f s` maps the monadic function `f` over values in `s`. -/
 meta def mmap {key val val'} [has_lt key] [decidable_rel ((<) : key → key → Prop)]
   (f : val → m val') (s : rb_map key val) : m (rb_map.{0 0} key val') :=
 rb_map.of_list <$> s.to_list.mmap (λ ⟨a,b⟩, prod.mk a <$> f b)
 
-meta def scale {α β} [has_lt α] [decidable_rel ((<) : α → α → Prop)] [has_mul β] (b : β) (m : rb_map α β) : rb_map α β :=
+/-- `scale b m` multiplies every value in `m` by `b`. -/
+meta def scale {key value} [has_lt key] [decidable_rel ((<) : key → key → Prop)] [has_mul value]
+  (b : value) (m : rb_map key value) : rb_map key value :=
 m.map ((*) b)
 
 section
@@ -85,21 +109,31 @@ end rb_lmap
 end native
 
 namespace name_set
+
+/-- `filter P s` returns the subset of elements of `s` satisfying `P`. -/
 meta def filter (P : name → bool) (s : name_set) : name_set :=
 s.fold s (λ a m, if P a then m else m.erase a)
 
+/-- `mfilter P s` returns the subset of elements of `s` satisfying `P`,
+where the check `P` is monadic. -/
 meta def mfilter {m} [monad m] (P : name → m bool) (s : name_set) : m name_set :=
 s.fold (pure s) (λ a m,
   do x ← m,
      mcond (P a) (pure x) (pure $ x.erase a))
 
+/-- `mmap f s` maps the monadic function `f` over values in `s`. -/
 meta def mmap {m} [monad m] (f : name → m name) (s : name_set) : m name_set :=
 s.fold (pure mk_name_set) (λ a m,
   do x ← m,
      b ← f a,
      (pure $ x.insert b))
 
+/-- `union s t` returns an rb_set containing every element that appears in either `s` or `t`. -/
 meta def union (s t : name_set) : name_set :=
 s.fold t (λ a t, t.insert a)
 
+/-- `insert_list s l` inserts every element of `l` into `s`. -/
+meta def insert_list (s : name_set) (l : list name) : name_set :=
+l.foldr (λ n s', s'.insert n) s
+
 end name_set
diff --git a/src/tactic/basic.lean b/src/tactic/basic.lean
index 99fa3ca4dd87e..1bcb0a50825f6 100644
--- a/src/tactic/basic.lean
+++ b/src/tactic/basic.lean
@@ -3,7 +3,6 @@ import
   tactic.cache
   tactic.converter.interactive
   tactic.core
-  tactic.doc_blame
   tactic.ext
   tactic.generalize_proofs
   tactic.interactive
@@ -16,7 +15,7 @@ import
   tactic.replacer
   tactic.restate_axiom
   tactic.rewrite
-  tactic.sanity_check
+  tactic.lint
   tactic.simpa
   tactic.simps
   tactic.split_ifs
diff --git a/src/tactic/core.lean b/src/tactic/core.lean
index eecf131ae7c91..aea4a06491d7d 100644
--- a/src/tactic/core.lean
+++ b/src/tactic/core.lean
@@ -106,7 +106,7 @@ do nm ← mk_fresh_name,
    return $ `user__ ++ nm.pop_prefix.sanitize_name ++ `user__
 
 
-/-- Checks whether n' has attribute n. -/
+/-- `has_attribute n n'` checks whether n' has attribute n. -/
 meta def has_attribute' : name → name → tactic bool | n n' :=
 succeeds (has_attribute n n')
 
diff --git a/src/tactic/doc_blame.lean b/src/tactic/doc_blame.lean
deleted file mode 100644
index 29ae1fb1ad701..0000000000000
--- a/src/tactic/doc_blame.lean
+++ /dev/null
@@ -1,33 +0,0 @@
-/-
-Copyright (c) 2019 Patrick Massot. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Patrick Massot, Robert Y. Lewis
--/
-import tactic.core
-open tactic declaration environment
-
-/-- Print the declaration name if it's a definition without a docstring -/
-meta def print_item (use_thms : bool) : declaration → tactic unit
-| (defn n _ _ _ _ _) := doc_string n >> skip <|> trace n
-| (cnst n _ _ _) := doc_string n >> skip <|> trace n
-| (thm n _ _ _) := when use_thms (doc_string n >> skip <|> trace n)
-| _ := skip
-
-/-- Print all definitions in the current file without a docstring -/
-meta def print_docstring_orphans (use_thms : bool) : tactic unit :=
-do curr_env ← get_env,
-   let local_decls : list declaration := curr_env.fold [] $ λ x t,
-     if environment.in_current_file' curr_env (to_name x) &&
-        not (to_name x).is_internal &&
-        not (is_auto_generated curr_env x) then x::t
-     else t,
-   local_decls.mmap' (print_item use_thms)
-
-setup_tactic_parser
-
-reserve prefix `#doc_blame`:max
-
-@[user_command]
-meta def doc_cmd (_ : decl_meta_info) (_ : parse $ tk "#doc_blame") : lean.parser unit :=
-do use_thms ← (tk "!") >> return tt <|> return ff,
-   print_docstring_orphans use_thms
diff --git a/src/tactic/interactive.lean b/src/tactic/interactive.lean
index 7266bbcce6d72..e37babc9c6d4e 100644
--- a/src/tactic/interactive.lean
+++ b/src/tactic/interactive.lean
@@ -4,7 +4,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Simon Hudon, Sebastien Gouezel, Scott Morrison
 -/
-import tactic.sanity_check
+import tactic.lint
 
 open lean
 open lean.parser
@@ -132,7 +132,7 @@ private meta def generalize_arg_p_aux : pexpr → parser (pexpr × name)
 private meta def generalize_arg_p : parser (pexpr × name) :=
 with_desc "expr = id" $ parser.pexpr 0 >>= generalize_arg_p_aux
 
-@[sanity_skip] lemma {u} generalize_a_aux {α : Sort u}
+@[nolint] lemma {u} generalize_a_aux {α : Sort u}
   (h : ∀ x : Sort u, (α → x) → x) : α := h α id
 
 /--
diff --git a/src/tactic/lint.lean b/src/tactic/lint.lean
new file mode 100644
index 0000000000000..432f575a8dbfc
--- /dev/null
+++ b/src/tactic/lint.lean
@@ -0,0 +1,384 @@
+/-
+Copyright (c) 2019 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
+-/
+import tactic.core
+/-!
+# lint command
+This file defines the following 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)
+
+Five 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. `illegal_constant` checks whether ≥/> is used in the declaration
+5. `doc_blame` checks for missing doc strings on definitions and constants.
+
+A sixth 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 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.
+
+## Tags
+sanity check, lint, cleanup, command, tactic
+-/
+
+universe variable u
+open expr tactic native
+
+reserve notation `#lint`
+reserve notation `#lint_mathlib`
+reserve notation `#lint_all`
+reserve notation `#list_linters`
+
+run_cmd tactic.skip -- apparently doc strings can't come directly after `reserve notation`
+
+/-- Defines the user attribute `nolint` for skipping `#lint` -/
+@[user_attribute]
+meta def nolint_attr : user_attribute :=
+{ name := "nolint",
+  descr := "Do not report this declaration in any of the tests of `#lint`" }
+
+attribute [nolint] imp_intro
+  classical.dec classical.dec_pred classical.dec_rel classical.dec_eq
+
+/--
+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-`.
+-/
+meta structure linter :=
+(test : declaration → tactic (option string))
+(no_errors_found : string)
+(errors_found : string)
+(is_fast : bool := tt)
+
+/-- 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 linter) :=
+l.mmap (λ n, 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) }
+
+setup_tactic_parser
+universe variable v
+
+/-- Find all declarations in `l` where tac returns `some x` and list them. -/
+meta def fold_over_with_cond {α} (l : list declaration) (tac : declaration → tactic (option α)) :
+  tactic (list (declaration × α)) :=
+l.mmap_filter $ λ d, option.map (λ x, (d, x)) <$> tac d
+
+/-- Find all declarations in `l` where tac returns `some x` and sort the resulting list by file name. -/
+meta def fold_over_with_cond_sorted {α} (l : list declaration)
+  (tac : declaration → tactic (option α)) : tactic (list (string × list (declaration × α))) := do
+  e ← get_env,
+  ds ← fold_over_with_cond l tac,
+  let ds₂ := rb_lmap.of_list (ds.map (λ x, ((e.decl_olean x.1.to_name).iget, x))),
+  return $ ds₂.to_list
+
+/-- Make the output of `fold_over_with_cond` printable, in the following form:
+      #print <name> <open multiline comment> <elt of α> <close multiline comment> -/
+meta def print_decls {α} [has_to_format α] (ds : list (declaration × α)) : format :=
+ds.foldl
+  (λ f x, f ++ "\n" ++ to_fmt "#print " ++ to_fmt x.1.to_name ++ " /- " ++ to_fmt x.2 ++ " -/")
+  format.nil
+
+/-- Make the output of `fold_over_with_cond_sorted` printable, with the file path + name inserted.-/
+meta def print_decls_sorted {α} [has_to_format α] (ds : list (string × list (declaration × α))) :
+  format :=
+ds.foldl
+  (λ f x, f ++ "\n\n" ++ to_fmt "-- " ++ to_fmt x.1 ++ print_decls x.2)
+  format.nil
+
+/-- Same as `print_decls_sorted`, but removing the first `n` characters from the string.
+  Useful for omitting the mathlib directory from the output. -/
+meta def print_decls_sorted_mathlib {α} [has_to_format α] (n : ℕ)
+  (ds : list (string × list (declaration × α))) : format :=
+ds.foldl
+  (λ f x, f ++ "\n\n" ++ to_fmt "-- " ++ to_fmt (x.1.popn n) ++ print_decls x.2)
+  format.nil
+
+/-- Auxilliary definition for `check_unused_arguments` -/
+meta def check_unused_arguments_aux : list ℕ → ℕ → ℕ → expr → list ℕ | l n n_max e :=
+if n > n_max then l else
+if ¬ is_lambda e ∧ ¬ is_pi e then l else
+  let b := e.binding_body in
+  let l' := if b.has_var_idx 0 then l else n :: l in check_unused_arguments_aux l' (n+1) n_max b
+
+/-- Check which arguments of a declaration are not used.
+  Prints a list of natural numbers corresponding to which arguments are not used (e.g.
+    this outputs [1, 4] if the first and fourth arguments are unused).
+  Checks both the type and the value of `d` for whether the argument is used
+  (in rare cases an argument is used in the type but not in the value).
+  We return [] if the declaration was automatically generated.
+  We print arguments that are larger than the arity of the type of the declaration
+  (without unfolding definitions). -/
+meta def check_unused_arguments (d : declaration) : option (list ℕ) :=
+let l := check_unused_arguments_aux [] 1 d.type.pi_arity d.value in
+if l = [] then none else
+let l2 := check_unused_arguments_aux [] 1 d.type.pi_arity d.type in
+(l.filter $ λ n, n ∈ l2).reverse
+
+/-- Check for unused arguments, and print them with their position, variable name, type and whether
+  the argument is a duplicate.
+  See also `check_unused_arguments`.
+  This tactic additionally filters out all unused arguments of type `parse _` -/
+meta def unused_arguments (d : declaration) : tactic (option string) := do
+  let ns := check_unused_arguments d,
+  if ¬ ns.is_some then return none else do
+  let ns := ns.iget,
+  (ds, _) ← get_pi_binders d.type,
+  let ns := ns.map (λ n, (n, (ds.nth $ n - 1).iget)),
+  let ns := ns.filter (λ x, x.2.type.get_app_fn ≠ const `interactive.parse []),
+  if ns = [] then return none else do
+  ds' ← ds.mmap pp,
+  ns ← ns.mmap (λ ⟨n, b⟩, (λ s, to_fmt "argument " ++ to_fmt n ++ ": " ++ s ++
+    (if ds.countp (λ b', b.type = b'.type) ≥ 2 then " (duplicate)" else "")) <$> pp b),
+  return $ some $ ns.to_string_aux tt
+
+/-- A linter object for checking for unused arguments. This is in the default linter set. -/
+@[linter] meta def linter.unused_arguments : linter :=
+{ test := unused_arguments,
+  no_errors_found := "No unused arguments",
+  errors_found := "UNUSED ARGUMENTS" }
+
+/-- Checks whether the correct declaration constructor (definition or theorem) by comparing it
+  to its sort. Instances will not be printed -/
+meta def incorrect_def_lemma (d : declaration) : tactic (option string) := do
+  e ← get_env,
+  expr.sort n ← infer_type d.type,
+  let is_def : Prop := d.is_definition,
+  if d.is_constant ∨ d.is_axiom ∨ (is_def ↔ (n ≠ level.zero))
+    then return none
+    else is_instance d.to_name >>= λ b, return $
+    if b then none
+    else if (d.is_definition : bool) then "is a def, should be a lemma/theorem"
+    else "is a lemma/theorem, should be a def"
+
+/-- A linter for checking whether the correct declaration constructor (definition or theorem)
+has been used. -/
+@[linter] meta def linter.def_lemma : linter :=
+{ test := incorrect_def_lemma,
+  no_errors_found := "All declarations correctly marked as def/lemma",
+  errors_found := "INCORRECT DEF/LEMMA" }
+
+/-- Checks whether a declaration has a namespace twice consecutively in its name -/
+meta def dup_namespace (d : declaration) : tactic (option string) :=
+is_instance d.to_name >>= λ is_inst,
+return $ let nm := d.to_name.components in if nm.chain' (≠) ∨ is_inst then none
+  else let s := (nm.find $ λ n, nm.count n ≥ 2).iget.to_string in
+  some $ "The namespace `" ++ s ++ "` is duplicated in the name"
+
+/-- A linter for checking whether a declaration has a namespace twice consecutively in its name. -/
+@[linter] meta def linter.dup_namespace : linter :=
+{ test := dup_namespace,
+  no_errors_found := "No declarations have a duplicate namespace",
+  errors_found := "DUPLICATED NAMESPACES IN NAME" }
+
+/-- Checks whether a `>`/`≥` is used in the statement of `d`. -/
+-- TODO: the commented out code also checks for classicality in statements, but needs fixing
+-- TODO: this probably needs to also check whether the argument is a variable or @eq <var> _ _
+-- meta def illegal_constants_in_statement (d : declaration) : tactic (option string) :=
+-- return $ if d.type.contains_constant (λ n, (n.get_prefix = `classical ∧
+--   n.last ∈ ["prop_decidable", "dec", "dec_rel", "dec_eq"]) ∨ n ∈ [`gt, `ge])
+-- then
+--   let illegal1 := [`classical.prop_decidable, `classical.dec, `classical.dec_rel, `classical.dec_eq],
+--       illegal2 := [`gt, `ge],
+--       occur1 := illegal1.filter (λ n, d.type.contains_constant (eq n)),
+--       occur2 := illegal2.filter (λ n, d.type.contains_constant (eq n)) in
+--   some $ sformat!"the type contains the following declarations: {occur1 ++ occur2}." ++
+--     (if occur1 = [] then "" else " Add decidability type-class arguments instead.") ++
+--     (if occur2 = [] then "" else " Use ≤/< instead.")
+-- else none
+meta def illegal_constants_in_statement (d : declaration) : tactic (option string) :=
+return $ let illegal := [`gt, `ge] in if d.type.contains_constant (λ n, n ∈ illegal)
+  then some "the type contains ≥/>. Use ≤/< instead."
+  else none
+
+/-- A linter for checking whether illegal constants (≥, >) appear in a declaration's type. -/
+@[linter] meta def linter.illegal_constants : linter :=
+{ test := illegal_constants_in_statement,
+  no_errors_found := "No illegal constants in declarations",
+  errors_found := "ILLEGAL CONSTANTS IN DECLARATIONS",
+  is_fast := ff }
+
+/-- Reports definitions and constants that are missing doc strings -/
+meta def doc_blame_report_defn : declaration → tactic (option string)
+| (declaration.defn n _ _ _ _ _) := doc_string n >> return none <|> return "def missing doc string"
+| (declaration.cnst n _ _ _) := doc_string n >> return none <|> return "constant missing doc string"
+| _ := return none
+
+/-- Reports definitions and constants that are missing doc strings -/
+meta def doc_blame_report_thm : declaration → tactic (option string)
+| (declaration.thm n _ _ _) := doc_string n >> return none <|> return "theorem missing doc string"
+| _ := return none
+
+/-- A linter for checking definition doc strings -/
+@[linter] meta def linter.doc_blame : linter :=
+{ test := λ d, mcond (bnot <$> has_attribute' `instance d.to_name) (doc_blame_report_defn d) (return none),
+  no_errors_found := "No definitions are missing documentation.",
+  errors_found := "DEFINITIONS ARE MISSING DOCUMENTATION STRINGS" }
+
+/-- A linter for checking theorem doc strings. This is not in the default linter set. -/
+meta def linter.doc_blame_thm : linter :=
+{ test := doc_blame_report_thm,
+  no_errors_found := "No theorems are missing documentation.",
+  errors_found := "THEOREMS ARE MISSING DOCUMENTATION STRINGS",
+  is_fast := ff }
+
+/-- `get_checks slow extra use_only` produces a list of linters.
+`extras` is a list of names that should resolve to declarations with type `linter`.
+If `use_only` is true, it only uses the linters in `extra`.
+Otherwise, it uses all linters in the environment tagged with `@[linter]`.
+If `slow` is false, it filters the linter list to only use fast tests. -/
+meta def get_checks (slow : bool) (extra : list name) (use_only : bool) :
+  tactic (list linter) :=
+do linter_list ← if use_only then return extra else list.append extra <$> attribute.get_instances `linter,
+   linter_list ← get_linters linter_list.erase_dup,
+   return $ if slow then linter_list else linter_list.filter (λ l, l.is_fast)
+
+/-- The common denominator of `#lint[|mathlib|all]`.
+  The different commands have different configurations for `l`, `printer` and `where_desc`.
+  If `slow` is false, doesn't do the checks that take a lot of time.
+  By setting `checks` you can customize which checks are performed. -/
+meta def lint_aux (l : list declaration)
+  (printer : (declaration → tactic (option string)) → tactic format)
+  (where_desc : string) (slow : bool) (checks : list linter) : tactic format := do
+  let s : format := "/- Note: This command is still in development. -/\n",
+  let s := s ++ format!"/- Checking {l.length} declarations {where_desc} -/\n\n",
+  s ← checks.mfoldl (λ s ⟨tac, ok_string, warning_string, _⟩, show tactic format, from do
+    f ← printer tac,
+    return $ s ++ if f.is_nil then format!"/- OK: {ok_string}. -/\n"
+  else format!"/- {warning_string}: -/" ++ f ++ "\n\n") s,
+  return $ if slow then s else s ++ "/- (slow tests skipped) -/\n"
+
+/-- Return the message printed by `#lint`. -/
+meta def lint (slow : bool := tt) (extra : list name := [])
+  (use_only : bool := ff) : tactic format := do
+  checks ← get_checks slow extra use_only,
+  e ← get_env,
+  l ← e.mfilter (λ d,
+    if e.in_current_file' d.to_name ∧ ¬ d.to_name.is_internal ∧ ¬ d.is_auto_generated e
+    then bnot <$> has_attribute' `nolint d.to_name else return ff),
+  lint_aux l (λ t, print_decls <$> fold_over_with_cond l t)
+    "in the current file" slow checks
+
+/-- Return the message printed by `#lint_mathlib`. -/
+meta def lint_mathlib (slow : bool := tt) (extra : list name := [])
+  (use_only : bool := ff) : tactic format := do
+  checks ← get_checks slow extra use_only,
+  e ← get_env,
+  ml ← get_mathlib_dir,
+  /- note: we don't separate out some of these tests in `lint_aux` because that causes a
+    performance hit. That is also the reason for the current formulation using if then else. -/
+  l ← e.mfilter (λ d,
+    if e.is_prefix_of_file ml d.to_name ∧ ¬ d.to_name.is_internal ∧ ¬ d.is_auto_generated e
+    then bnot <$> has_attribute' `nolint d.to_name else return ff),
+  let ml' := ml.length,
+  lint_aux l (λ t, print_decls_sorted_mathlib ml' <$> fold_over_with_cond_sorted l t)
+    "in mathlib (only in imported files)" slow checks
+
+/-- Return the message printed by `#lint_all`. -/
+meta def lint_all (slow : bool := tt) (extra : list name := [])
+  (use_only : bool := ff) : tactic format := do
+  checks ← get_checks slow extra use_only,
+  e ← get_env,
+  l ← e.mfilter (λ d, if ¬ d.to_name.is_internal ∧ ¬ d.is_auto_generated e
+    then bnot <$> has_attribute' `nolint d.to_name else return ff),
+  lint_aux l (λ t, print_decls_sorted <$> fold_over_with_cond_sorted l t)
+    "in all imported files (including this one)" slow checks
+
+/-- Parses an optional `only`, followed by a sequence of zero or more identifiers.
+Prepends `linter.` to each of these identifiers. -/
+private meta def parse_lint_additions : parser (bool × list name) :=
+prod.mk <$> only_flag <*> (list.map (name.append `linter) <$> ident_*)
+
+/-- The common denominator of `lint_cmd`, `lint_mathlib_cmd`, `lint_all_cmd` -/
+private meta def lint_cmd_aux (scope : bool → list name → bool → tactic format) : parser unit :=
+do b ← optional (tk "-"),
+   (use_only, extra) ← parse_lint_additions,
+   s ← scope b.is_none extra use_only,
+   trace s
+
+/-- The command `#lint` at the bottom of a file will warn you about some common mistakes
+in that file. Usage: `#lint`, `#lint linter_1 linter_2`, `#lint only linter_1 linter_2`.
+Use the command `#list_linters` to see all available linters. -/
+@[user_command] meta def lint_cmd (_ : parse $ tk "#lint") : parser unit :=
+lint_cmd_aux @lint
+
+/-- The command `#lint_mathlib` checks all of mathlib for certain mistakes.
+Usage: `#lint_mathlib`, `#lint_mathlib linter_1 linter_2`, `#lint_mathlib only linter_1 linter_2`.
+Use the command `#list_linters` to see all available linters. -/
+@[user_command] meta def lint_mathlib_cmd (_ : parse $ tk "#lint_mathlib") : parser unit :=
+lint_cmd_aux @lint_mathlib
+
+/-- The command `#lint_all` checks all imported files for certain mistakes.
+Usage: `#lint_all`, `#lint_all linter_1 linter_2`, `#lint_all only linter_1 linter_2`.
+Use the command `#list_linters` to see all available linters. -/
+@[user_command] meta def lint_all_cmd (_ : parse $ tk "#lint_all") : parser unit :=
+lint_cmd_aux @lint_all
+
+/-- The command `#list_linters` prints a list of all available linters. -/
+@[user_command] meta def list_linters (_ : parse $ tk "#list_linters") : parser unit :=
+do env ← get_env,
+let ns := env.decl_filter_map $ λ dcl,
+    if (dcl.to_name.get_prefix = `linter) && (dcl.type = `(linter)) then some dcl.to_name else none,
+   trace "Available linters:\n  linters marked with (*) are in the default lint set\n",
+   ns.mmap' $ λ n, do
+     b ← has_attribute' `linter n,
+     trace $ n.pop_prefix.to_string ++ if b then " (*)" else ""
+
+/-- Use `lint` as a hole command. Note: In a large file, there might be some delay between
+  choosing the option and the information appearing -/
+@[hole_command] meta def lint_hole_cmd : hole_command :=
+{ name := "Lint",
+  descr := "Lint: Find common mistakes in current file.",
+  action := λ es, do s ← lint, return [(s.to_string,"")] }
+
+-- set_option profiler true
+-- run_cmd lint
+-- run_cmd lint_mathlib
+-- run_cmd lint_all
+-- #lint
+-- #lint only unused_arguments dup_namespace
+-- #lint_mathlib
+-- #lint_all
+-- #lint-
+-- #lint_mathlib-
+-- #lint_all-
+-- #list_linters
diff --git a/src/tactic/sanity_check.lean b/src/tactic/sanity_check.lean
deleted file mode 100644
index 5c846ffc606d3..0000000000000
--- a/src/tactic/sanity_check.lean
+++ /dev/null
@@ -1,265 +0,0 @@
-/-
-Copyright (c) 2019 Floris van Doorn. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn
--/
-import tactic.core
-/-!
-  # sanity_check command
-  This file defines the following user commands to spot common mistakes in the code.
-  * `#sanity_check`: check all declarations in the current file
-  * `#sanity_check_mathlib`: check all declarations in mathlib (so excluding core or other projects,
-    and also excluding the current file)
-  * `#sanity_check_all`: check all declarations in the environment (the current file and all
-    imported files)
-
-  Currently this will check for
-  1. unused arguments in declarations,
-  2. whether a declaration is incorrectly marked as a def/lemma,
-  3. whether a namespace is duplicated in the name of a declaration
-  4. whether ≥/> is used in the declaration
-
-  You can append a `-` to any command (e.g. `#sanity_check_mathlib-`) to omit the slow tests (4).
-
-  You can customize the performed checks like this:
-  ```
-  meta def my_check (d : declaration) : tactic (option string) :=
-  return $ if d.to_name = `foo then some "gotcha!" else none
-  run_cmd sanity_check tt [(my_check, "found nothing", "found something")] >>= trace
-  ```
-
-  ## Tags
-  sanity check, sanity_check, cleanup, command, tactic
--/
-
-universe variable u
-open expr tactic native
-
-reserve notation `#sanity_check`
-reserve notation `#sanity_check_mathlib`
-reserve notation `#sanity_check_all`
-
-@[user_attribute]
-meta def sanity_skip_attr : user_attribute :=
-{ name := "sanity_skip",
-  descr := "Do not report this declaration in any of the tests of `#sanity_check`" }
-
-attribute [sanity_skip] imp_intro
-  classical.dec classical.dec_pred classical.dec_rel classical.dec_eq
-
-setup_tactic_parser
-universe variable v
-
-/-- Find all declarations in `l` where tac returns `some x` and list them. -/
-meta def fold_over_with_cond {α} (l : list declaration) (tac : declaration → tactic (option α)) :
-  tactic (list (declaration × α)) :=
-l.mmap_filter $ λ d, option.map (λ x, (d, x)) <$> tac d
-
-/-- Find all declarations in `l` where tac returns `some x` and sort the resulting list by file name. -/
-meta def fold_over_with_cond_sorted {α} (l : list declaration)
-  (tac : declaration → tactic (option α)) : tactic (list (string × list (declaration × α))) := do
-  e ← get_env,
-  ds ← fold_over_with_cond l tac,
-  let ds₂ := rb_lmap.of_list (ds.map (λ x, ((e.decl_olean x.1.to_name).iget, x))),
-  return $ ds₂.to_list
-
-/-- Make the output of `fold_over_with_cond` printable, in the following form:
-      #print <name> <open multiline comment> <elt of α> <close multiline comment> -/
-meta def print_decls {α} [has_to_format α] (ds : list (declaration × α)) : format :=
-ds.foldl
-  (λ f x, f ++ "\n" ++ to_fmt "#print " ++ to_fmt x.1.to_name ++ " /- " ++ to_fmt x.2 ++ " -/")
-  format.nil
-
-/-- Make the output of `fold_over_with_cond_sorted` printable, with the file path + name inserted.-/
-meta def print_decls_sorted {α} [has_to_format α] (ds : list (string × list (declaration × α))) :
-  format :=
-ds.foldl
-  (λ f x, f ++ "\n\n" ++ to_fmt "-- " ++ to_fmt x.1 ++ print_decls x.2)
-  format.nil
-
-/-- Same as `print_decls_sorted`, but removing the first `n` characters from the string.
-  Useful for omitting the mathlib directory from the output. -/
-meta def print_decls_sorted_mathlib {α} [has_to_format α] (n : ℕ)
-  (ds : list (string × list (declaration × α))) : format :=
-ds.foldl
-  (λ f x, f ++ "\n\n" ++ to_fmt "-- " ++ to_fmt (x.1.popn n) ++ print_decls x.2)
-  format.nil
-
-/-- Auxilliary definition for `check_unused_arguments` -/
-meta def check_unused_arguments_aux : list ℕ → ℕ → ℕ → expr → list ℕ | l n n_max e :=
-if n > n_max then l else
-if ¬ is_lambda e ∧ ¬ is_pi e then l else
-  let b := e.binding_body in
-  let l' := if b.has_var_idx 0 then l else n :: l in check_unused_arguments_aux l' (n+1) n_max b
-
-/-- Check which arguments of a declaration are not used.
-  Prints a list of natural numbers corresponding to which arguments are not used (e.g.
-    this outputs [1, 4] if the first and fourth arguments are unused).
-  Checks both the type and the value of `d` for whether the argument is used
-  (in rare cases an argument is used in the type but not in the value).
-  We return [] if the declaration was automatically generated.
-  We print arguments that are larger than the arity of the type of the declaration
-  (without unfolding definitions). -/
-meta def check_unused_arguments (d : declaration) : option (list ℕ) :=
-let l := check_unused_arguments_aux [] 1 d.type.pi_arity d.value in
-if l = [] then none else
-let l2 := check_unused_arguments_aux [] 1 d.type.pi_arity d.type in
-(l.filter $ λ n, n ∈ l2).reverse
-
-/- Check for unused arguments, and print them with their position, variable name, type and whether
-  the argument is a duplicate.
-  See also `check_unused_arguments`.
-  This tactic additionally filters out all unused arguments of type `parse _` -/
-meta def unused_arguments (d : declaration) : tactic (option string) := do
-  let ns := check_unused_arguments d,
-  if ¬ ns.is_some then return none else do
-  let ns := ns.iget,
-  (ds, _) ← get_pi_binders d.type,
-  let ns := ns.map (λ n, (n, (ds.nth $ n - 1).iget)),
-  let ns := ns.filter (λ x, x.2.type.get_app_fn ≠ const `interactive.parse []),
-  if ns = [] then return none else do
-  ds' ← ds.mmap pp,
-  ns ← ns.mmap (λ ⟨n, b⟩, (λ s, to_fmt "argument " ++ to_fmt n ++ ": " ++ s ++
-    (if ds.countp (λ b', b.type = b'.type) ≥ 2 then " (duplicate)" else "")) <$> pp b),
-  return $ some $ ns.to_string_aux tt
-
-/-- Checks whether the correct declaration constructor (definition of theorem) by comparing it
-  to its sort. Instances will not be printed -/
-meta def incorrect_def_lemma (d : declaration) : tactic (option string) := do
-  e ← get_env,
-  expr.sort n ← infer_type d.type,
-  let is_def : Prop := d.is_definition,
-  if d.is_constant ∨ d.is_axiom ∨ (is_def ↔ (n ≠ level.zero))
-    then return none
-    else is_instance d.to_name >>= λ b, return $
-    if b then none
-    else if (d.is_definition : bool) then "is a def, should be a lemma/theorem"
-    else "is a lemma/theorem, should be a def"
-
-/-- Checks whether a declaration has a namespace twice consecutively in its name -/
-meta def dup_namespace (d : declaration) : tactic (option string) :=
-is_instance d.to_name >>= λ is_inst,
-return $ let nm := d.to_name.components in if nm.chain' (≠) ∨ is_inst then none
-  else let s := (nm.find $ λ n, nm.count n ≥ 2).iget.to_string in
-  some $ "The namespace `" ++ s ++ "` is duplicated in the name"
-
-/-- Checks whether a `>`/`≥` is used in the statement of `d`. -/
--- TODO: the commented out code also checks for classicality in statements, but needs fixing
--- TODO: this probably needs to also check whether the argument is a variable or @eq <var> _ _
--- meta def illegal_constants_in_statement (d : declaration) : tactic (option string) :=
--- return $ if d.type.contains_constant (λ n, (n.get_prefix = `classical ∧
---   n.last ∈ ["prop_decidable", "dec", "dec_rel", "dec_eq"]) ∨ n ∈ [`gt, `ge])
--- then
---   let illegal1 := [`classical.prop_decidable, `classical.dec, `classical.dec_rel, `classical.dec_eq],
---       illegal2 := [`gt, `ge],
---       occur1 := illegal1.filter (λ n, d.type.contains_constant (eq n)),
---       occur2 := illegal2.filter (λ n, d.type.contains_constant (eq n)) in
---   some $ sformat!"the type contains the following declarations: {occur1 ++ occur2}." ++
---     (if occur1 = [] then "" else " Add decidability type-class arguments instead.") ++
---     (if occur2 = [] then "" else " Use ≤/< instead.")
--- else none
-meta def illegal_constants_in_statement (d : declaration) : tactic (option string) :=
-return $ let illegal := [`gt, `ge] in if d.type.contains_constant (λ n, n ∈ illegal)
-  then some "the type contains ≥/>. Use ≤/< instead."
-  else none
-
-/- The quick checks of `#sanity_check` -/
-meta def quick_checks : list ((declaration → tactic (option string)) × string × string) :=
-[ (unused_arguments, "No unused arguments", "UNUSED ARGUMENTS"),
-  (incorrect_def_lemma, "All declarations correctly marked as def/lemma", "INCORRECT DEF/LEMMA"),
-  (dup_namespace, "No declarations have a duplicate namespace", "DUPLICATED NAMESPACES IN NAME")]
-
-/- The slow checks of `#sanity_check`. They are not executed with `#sanity_check-` -/
-meta def slow_checks : list ((declaration → tactic (option string)) × string × string) :=
-[ (illegal_constants_in_statement, "No illegal constants in declarations",
-    "ILLEGAL CONSTANTS IN DECLARATIONS")]
-
-/- The default checks of `#sanity_check`. Depends on whether `slow` is true -/
-meta def default_checks (slow : bool := tt) :
-  list ((declaration → tactic (option string)) × string × string) :=
-quick_checks ++ if slow then slow_checks else []
-
-/-- The common denominator of `#sanity_check[|mathlib|all]`.
-  The different commands have different configurations for `l`, `printer` and `where_desc`.
-  If `slow` is false, doesn't do the checks that take a lot of time.
-  By setting `checks` you can customize which checks are performed. -/
-meta def sanity_check_aux (l : list declaration)
-  (printer : (declaration → tactic (option string)) → tactic format)
-  (where_desc : string) (slow : bool)
-  (checks : list ((declaration → tactic (option string)) × string × string)) : tactic format := do
-  let s : format := "/- Note: This command is still in development. -/\n",
-  let s := s ++ format!"/- Checking {l.length} declarations {where_desc} -/\n\n",
-  s ← checks.mfoldl (λ s ⟨tac, ok_string, warning_string⟩, show tactic format, from do
-    f ← printer tac,
-    return $ s ++ if f.is_nil then format!"/- OK: {ok_string}. -/\n"
-  else format!"/- {warning_string}: -/" ++ f ++ "\n\n") s,
-  return $ if slow then s else s ++ "/- (slow tests skipped) -/\n"
-
-/-- Return the message printed by `#sanity_check`. -/
-meta def sanity_check (slow : bool := tt)
-  (checks : list ((declaration → tactic (option string)) × string × string) :=
-    default_checks slow) : tactic format := do
-  e ← get_env,
-  l ← e.mfilter (λ d,
-    if e.in_current_file' d.to_name ∧ ¬ d.to_name.is_internal ∧ ¬ d.is_auto_generated e
-    then bnot <$> has_attribute' `sanity_skip d.to_name else return ff),
-  sanity_check_aux l (λ t, print_decls <$> fold_over_with_cond l t)
-    "in the current file" slow checks
-
-/-- Return the message printed by `#sanity_check_mathlib`. -/
-meta def sanity_check_mathlib (slow : bool := tt)
-  (checks : list ((declaration → tactic (option string)) × string × string) :=
-    default_checks slow) : tactic format := do
-  e ← get_env,
-  ml ← get_mathlib_dir,
-  /- note: we don't separate out some of these tests in `sanity_check_aux` because that causes a
-    performance hit. That is also the reason for the current formulation using if then else. -/
-  l ← e.mfilter (λ d,
-    if e.is_prefix_of_file ml d.to_name ∧ ¬ d.to_name.is_internal ∧ ¬ d.is_auto_generated e
-    then bnot <$> has_attribute' `sanity_skip d.to_name else return ff),
-  let ml' := ml.length,
-  sanity_check_aux l (λ t, print_decls_sorted_mathlib ml' <$> fold_over_with_cond_sorted l t)
-    "in mathlib (only in imported files)" slow checks
-
-/-- Return the message printed by `#sanity_check_all`. -/
-meta def sanity_check_all (slow : bool := tt)
-  (checks : list ((declaration → tactic (option string)) × string × string) :=
-    default_checks slow) : tactic format := do
-  e ← get_env,
-  l ← e.mfilter (λ d, if ¬ d.to_name.is_internal ∧ ¬ d.is_auto_generated e
-    then bnot <$> has_attribute' `sanity_skip d.to_name else return ff),
-  sanity_check_aux l (λ t, print_decls_sorted <$> fold_over_with_cond_sorted l t)
-    "in all imported files (including this one)" slow checks
-
-/-- The command `#sanity_check` at the bottom of a file will warn you about some common mistakes
-  in that file. -/
-@[user_command] meta def sanity_check_cmd (_ : parse $ tk "#sanity_check") : parser unit :=
-do b ← optional (tk "-"), s ← sanity_check b.is_none, trace s
-
-/-- The command `#sanity_check_mathlib` checks all of mathlib for certain mistakes. -/
-@[user_command] meta def sanity_check_mathlib_cmd (_ : parse $ tk "#sanity_check_mathlib") :
-  parser unit :=
-do b ← optional (tk "-"), s ← sanity_check_mathlib b.is_none, trace s
-
-/-- The command `#sanity_check_mathlib` checks all of mathlib for certain mistakes. -/
-@[user_command] meta def sanity_check_all_cmd (_ : parse $ tk "#sanity_check_all") :
-  parser unit :=
-do b ← optional (tk "-"), s ← sanity_check_all b.is_none, trace s
-
-/-- Use sanity check as a hole command. Note: In a large file, there might be some delay between
-  choosing the option and the information appearing -/
-@[hole_command] meta def sanity_check_hole_cmd : hole_command :=
-{ name := "Sanity Check",
-  descr := "Sanity check: Find common mistakes in current file.",
-  action := λ es, do s ← sanity_check, return [(s.to_string,"")] }
-
--- set_option profiler true
--- run_cmd sanity_check
--- run_cmd sanity_check_mathlib
--- run_cmd sanity_check_all
--- #sanity_check
--- #sanity_check_mathlib
--- #sanity_check_all
--- #sanity_check-
--- #sanity_check_mathlib-
--- #sanity_check_all-
diff --git a/test/sanity_check.lean b/test/lint.lean
similarity index 84%
rename from test/sanity_check.lean
rename to test/lint.lean
index 764364636c5ad..37cee14063e2a 100644
--- a/test/sanity_check.lean
+++ b/test/lint.lean
@@ -1,4 +1,4 @@
-import tactic.sanity_check
+import tactic.lint
 
 def foo1 (n m : ℕ) : ℕ := n + 1
 def foo2 (n m : ℕ) : m = m := by refl
@@ -35,18 +35,23 @@ run_cmd do
   guard $ l4.length = 1,
   guard $ ∃(x ∈ l4), (x : declaration × _).1.to_name = `foo.foo,
   -- guard $ ∃(x ∈ l4), (x : declaration × _).1.to_name = `foo4,
-  s ← sanity_check ff,
+  s ← lint ff,
   guard $ "/- (slow tests skipped) -/\n".is_suffix_of s.to_string,
-  s2 ← sanity_check tt,
+  s2 ← lint tt,
   guard $ s.to_string ≠ s2.to_string,
   skip
 
-/- check customizability and sanity_skip -/
-@[sanity_skip] def bar.foo : (if 3 = 3 then 1 else 2) = 1 := if_pos (by refl)
+/- check customizability and nolint -/
+@[nolint] def bar.foo : (if 3 = 3 then 1 else 2) = 1 := if_pos (by refl)
 
 meta def dummy_check (d : declaration) : tactic (option string) :=
 return $ if d.to_name.last = "foo" then some "gotcha!" else none
 
+meta def linter.dummy_linter : linter :=
+{ test := dummy_check,
+  no_errors_found := "found nothing",
+  errors_found := "found something" }
+
 run_cmd do
-  s ← sanity_check tt [(dummy_check, "found nothing", "found something")],
+  s ← lint tt [`linter.dummy_linter] tt,
   guard $ "/- found something: -/\n#print foo.foo /- gotcha! -/\n\n".is_suffix_of s.to_string