fix(tactic/lint/basic): remove default argument for auto_decl and ena…

…ble more linters (#2580)

Run more linters on automatically-generated declarations.  Quite a few linters should have been run on them, but I forgot about it because the `auto_decls` flag is optional and off by default.  I've made it non-optional so that you don't forget about it when defining a linter.

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20linter.20and.20structure.20fields/near/195810856

src/data/list/forall2.lean

@@ -55,10 +55,10 @@ begin
   { assume h, subst h, exact forall₂_refl _ }
 end
 
-@[simp] lemma forall₂_nil_left_iff {l} : forall₂ r nil l ↔ l = nil :=
+@[simp, priority 900] lemma forall₂_nil_left_iff {l} : forall₂ r nil l ↔ l = nil :=
 ⟨λ H, by cases H; refl, by rintro rfl; exact forall₂.nil⟩
 
-@[simp] lemma forall₂_nil_right_iff {l} : forall₂ r l nil ↔ l = nil :=
+@[simp, priority 900] lemma forall₂_nil_right_iff {l} : forall₂ r l nil ↔ l = nil :=
 ⟨λ H, by cases H; refl, by rintro rfl; exact forall₂.nil⟩
 
 lemma forall₂_cons_left_iff {a l u} : forall₂ r (a::l) u ↔ (∃b u', r a b ∧ forall₂ r l u' ∧ u = b :: u') :=

src/tactic/lint/basic.lean

@@ -85,7 +85,7 @@ meta structure linter :=
 (no_errors_found : string)
 (errors_found : string)
 (is_fast : bool := tt)
-(auto_decls : bool := ff)
+(auto_decls : bool)
 
 /-- Takes a list of names that resolve to declarations of type `linter`,
 and produces a list of linters. -/

src/tactic/lint/misc.lean

@@ -51,6 +51,7 @@ return $ let illegal := [`gt, `ge] in if d.type.pi_codomain.contains_constant (
 /-- A linter for checking whether illegal constants (≥, >) appear in a declaration's type. -/
 @[linter] meta def linter.ge_or_gt : linter :=
 { test := ge_or_gt_in_statement,
+  auto_decls := ff,
   no_errors_found := "Not using ≥/> in declarations",
   errors_found := "USING ≥/> IN DECLARATIONS",
   is_fast := ff }
@@ -80,6 +81,7 @@ return $ let nm := d.to_name.components in if nm.chain' (≠) ∨ is_inst then n
 /-- 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,
+  auto_decls := ff,
   no_errors_found := "No declarations have a duplicate namespace",
   errors_found := "DUPLICATED NAMESPACES IN NAME" }
 
@@ -130,6 +132,7 @@ private meta def unused_arguments (d : declaration) : tactic (option string) :=
 /-- 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,
+  auto_decls := ff,
   no_errors_found := "No unused arguments",
   errors_found := "UNUSED ARGUMENTS" }
 
@@ -156,12 +159,14 @@ private meta def doc_blame_report_thm : declaration → tactic (option string)
 @[linter] meta def linter.doc_blame : linter :=
 { test := λ d, mcond (bnot <$> has_attribute' `instance d.to_name)
     (doc_blame_report_defn d) (return none),
+  auto_decls := ff,
   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,
+  auto_decls := ff,
   no_errors_found := "No theorems are missing documentation.",
   errors_found := "THEOREMS ARE MISSING DOCUMENTATION STRINGS",
   is_fast := ff }
@@ -194,6 +199,7 @@ private meta def incorrect_def_lemma (d : declaration) : tactic (option string)
 has been used. -/
 @[linter] meta def linter.def_lemma : linter :=
 { test := incorrect_def_lemma,
+  auto_decls := ff,
   no_errors_found := "All declarations correctly marked as def/lemma",
   errors_found := "INCORRECT DEF/LEMMA" }
 

src/tactic/lint/simp.lean

@@ -121,6 +121,7 @@ else
 /-- A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire. -/
 @[linter] meta def linter.simp_nf : linter :=
 { test := simp_nf_linter,
+  auto_decls := tt,
   no_errors_found := "All left-hand sides of simp lemmas are in simp-normal form",
   errors_found := "SOME SIMP LEMMAS ARE REDUNDANT.
 That is, their left-hand side is not in simp-normal form.
@@ -173,6 +174,7 @@ and which hence never fire.
 -/
 @[linter] meta def linter.simp_var_head : linter :=
 { test := simp_var_head,
+  auto_decls := tt,
   no_errors_found :=
     "No left-hand sides of a simp lemma has a variable as head symbol",
   errors_found := "LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL.\n" ++
@@ -195,6 +197,7 @@ pure $ "should not be marked simp"
 /-- A linter for commutativity lemmas that are marked simp. -/
 @[linter] meta def linter.simp_comm : linter :=
 { test := simp_comm,
+  auto_decls := tt,
   no_errors_found := "No commutativity lemma is marked simp",
   errors_found := "COMMUTATIVITY LEMMA IS SIMP.\n" ++
     "Some commutativity lemmas are simp lemmas" }

src/tactic/lint/type_classes.lean

@@ -122,6 +122,7 @@ else
 @[linter]
 meta def linter.has_inhabited_instance : linter :=
 { test := has_inhabited_instance,
+  auto_decls := ff,
   no_errors_found := "No types have missing inhabited instances",
   errors_found := "TYPES ARE MISSING INHABITED INSTANCES",
   is_fast := ff }
@@ -139,6 +140,7 @@ private meta def impossible_instance (d : declaration) : tactic (option string)
 /-- A linter object for `impossible_instance`. -/
 @[linter] meta def linter.impossible_instance : linter :=
 { test := impossible_instance,
+  auto_decls := tt,
   no_errors_found := "All instances are applicable",
   errors_found := "IMPOSSIBLE INSTANCES FOUND.
 These instances have an argument that cannot be found during type-class resolution, and therefore can never succeed. Either mark the arguments with square brackets (if it is a class), or don't make it an instance" }
@@ -161,6 +163,7 @@ private meta def incorrect_type_class_argument (d : declaration) : tactic (optio
 /-- A linter object for `incorrect_type_class_argument`. -/
 @[linter] meta def linter.incorrect_type_class_argument : linter :=
 { test := incorrect_type_class_argument,
+  auto_decls := tt,
   no_errors_found := "All declarations have correct type-class arguments",
   errors_found := "INCORRECT TYPE-CLASS ARGUMENTS.
 Some declarations have non-classes between [square brackets]" }
@@ -223,6 +226,7 @@ meta def fails_quickly (max_steps : ℕ) (d : declaration) : tactic (option stri
   As of 5 Mar 2020 the longest trace (for `is_add_hom`) takes 2900-3000 "heartbeats". -/
 @[linter] meta def linter.fails_quickly : linter :=
 { test := fails_quickly 3000,
+  auto_decls := tt,
   no_errors_found := "No type-class searches timed out",
   errors_found := "TYPE CLASS SEARCHES TIMED OUT.
 For the following classes, there is an instance that causes a loop, or an excessively long search.",
@@ -239,6 +243,7 @@ private meta def has_coe_variable (d : declaration) : tactic (option string) :=
 /-- A linter object for `has_coe_variable`. -/
 @[linter] meta def linter.has_coe_variable : linter :=
 { test := has_coe_variable,
+  auto_decls := tt,
   no_errors_found := "No invalid `has_coe` instances",
   errors_found := "INVALID `has_coe` INSTANCES.
 Make the following declarations instances of the class `has_coe_t` instead of `has_coe`." }
@@ -256,6 +261,7 @@ do tt ← is_prop d.type | return none,
 /-- A linter object for `inhabited_nonempty`. -/
 @[linter] meta def linter.inhabited_nonempty : linter :=
 { test := inhabited_nonempty,
+  auto_decls := ff,
   no_errors_found := "No uses of `inhabited` arguments should be replaced with `nonempty`",
   errors_found := "USES OF `inhabited` SHOULD BE REPLACED WITH `nonempty`." }
 
@@ -275,6 +281,7 @@ do tt ← is_prop d.type | return none,
 /-- A linter object for `decidable_classical`. -/
 @[linter] meta def linter.decidable_classical : linter :=
 { test := decidable_classical,
+  auto_decls := ff,
   no_errors_found := "No uses of `decidable` arguments should be replaced with `classical`",
   errors_found := "USES OF `decidable` SHOULD BE REPLACED WITH `classical` IN THE PROOF." }
 
@@ -312,6 +319,7 @@ pure $ format.to_string $
 /-- Linter that checks whether `has_coe_to_fun` instances comply with Note [function coercion]. -/
 @[linter] meta def linter.has_coe_to_fun : linter :=
 { test := has_coe_to_fun_linter,
+  auto_decls := tt,
   no_errors_found := "has_coe_to_fun is used correctly",
   errors_found := "INVALID/MISSING `has_coe_to_fun` instances.
 You should add a `has_coe_to_fun` instance for the following types.

test/lint.lean

@@ -53,6 +53,7 @@ return $ if d.to_name.last = "foo" then some "gotcha!" else none
 
 meta def linter.dummy_linter : linter :=
 { test := dummy_check,
+  auto_decls := ff,
   no_errors_found := "found nothing",
   errors_found := "found something" }