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

Author: robertylewis

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'
 

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 γ }

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 }

src/meta/rb_map.lean

@@ -2,42 +2,62 @@
 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)
 
 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

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

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')
 

src/tactic/doc_blame.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
 
 /--