feat(tactic/lint): add unprintable tactic linter (#11725)

This linter will banish the recurring issue of tactics for which `param_desc` fails, leaving a nasty error message in hovers.

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

src/ring_theory/witt_vector/init_tail.lean

@@ -45,7 +45,7 @@ setup_tactic_parser
 /--
 `init_ring` is an auxiliary tactic that discharges goals factoring `init` over ring operations.
 -/
-meta def init_ring (assert : parse (tk "using" >> parser.pexpr)?) : tactic unit := do
+meta def init_ring (assert : parse (tk "using" *> parser.pexpr)?) : tactic unit := do
 `[rw ext_iff,
   intros i,
   simp only [init, select, coeff_mk],

src/tactic/interactive.lean

@@ -576,7 +576,7 @@ meta def h_generalize (rev : parse (tk "!")?)
      (h : parse ident_?)
      (_ : parse (tk ":"))
      (arg : parse h_generalize_arg_p)
-     (eqs_h : parse ( (tk "with" >> pure <$> ident_) <|> pure [])) :
+     (eqs_h : parse ( (tk "with" *> pure <$> ident_) <|> pure [])) :
   tactic unit :=
 do let (e,n) := arg,
    let h' := if h = `_ then none else h,
@@ -774,10 +774,7 @@ add_tactic_doc
   inherit_description_from := `tactic.interactive.change' }
 
 private meta def opt_dir_with : parser (option (bool × name)) :=
-(do tk "with",
-   arrow ← (tk "<-")?,
-   h ← ident,
-   return (arrow.is_some, h)) <|> return none
+(tk "with" *> ((λ arrow h, (option.is_some arrow, h)) <$> (tk "<-")? <*> ident))?
 
 /--
 `set a := t with h` is a variant of `let a := t`. It adds the hypothesis `h : a = t` to
@@ -801,7 +798,7 @@ h : y = 3
 end
 ```
 -/
-meta def set (h_simp : parse (tk "!")?) (a : parse ident) (tp : parse ((tk ":") >> texpr)?)
+meta def set (h_simp : parse (tk "!")?) (a : parse ident) (tp : parse ((tk ":") *> texpr)?)
   (_ : parse (tk ":=")) (pv : parse texpr)
   (rev_name : parse opt_dir_with) :=
 do tp ← i_to_expr $ tp.get_or_else pexpr.mk_placeholder,
@@ -945,7 +942,7 @@ end
 ```
 
 -/
-meta def extract_goal (print_use : parse $ tt <$ tk "!" <|> pure ff)
+meta def extract_goal (print_use : parse $ (tk "!" *> pure tt) <|> pure ff)
   (n : parse ident?) (vs : parse (tk "with" *> ident*)?)
   : tactic unit :=
 do tgt ← target,

src/tactic/itauto.lean

@@ -660,7 +660,7 @@ find among the atomic propositions, and `itauto! *` will case on all proposition
 *Warning:* This can blow up the proof search, so it should be used sparingly.
 -/
 meta def itauto (classical : parse (tk "!")?)
-  : parse (some <$> pexpr_list <|> none <$ tk "*")? → tactic unit
+  : parse (some <$> pexpr_list <|> tk "*" *> pure none)? → tactic unit
 | none := tactic.itauto false classical.is_some []
 | (some none) := tactic.itauto true classical.is_some []
 | (some (some ls)) := ls.mmap i_to_expr >>= tactic.itauto false classical.is_some

src/tactic/linear_combination.lean

@@ -324,16 +324,8 @@ was given a `pexpr ` of ``(1) along with the identifier.
 * Output: a `lean.parser (name × pexpr)`
 -/
 meta def parse_name_pexpr_pair : lean.parser (name × pexpr) :=
-(do
-  tk "(",
-  id ← ident,
-  tk ",",
-  coeff ← parser.pexpr 0,
-  tk ")",
-  pure (id, coeff)) <|>
-(do
-  id ← ident,
-  pure (id, ``(1)))
+(tk "(" *> prod.mk <$> ident <*> (tk "," *> parser.pexpr 0 <* tk ")")) <|>
+((λ id, (id, ``(1))) <$> ident)
 
 /--
 `linear_combination` attempts to prove the target by creating and applying a

src/tactic/lint/default.lean

@@ -53,6 +53,7 @@ The following linters are run by default:
 20. `check_univs` checks that there are no bad `max u v` universe levels.
 21. `syn_taut` checks that declarations are not syntactic tautologies.
 22. `check_reducibility` checks whether non-instances with a class as type are reducible.
+23. `unprintable_interactive` checks that interactive tactics have parser documentation.
 
 Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
 This is not run by default.

src/tactic/lint/misc.lean

@@ -448,3 +448,36 @@ meta def linter.unused_haves_suffices : linter :=
 "`proof_of_goal`, in addition to being ineffectual, they may make unnecessary assumptions in " ++
 "proofs appear as if they are used. ",
   is_fast := ff }
+
+/-!
+## Linter for unprintable interactive tactics
+-/
+
+/--
+Ensures that every interactive tactic has arguments for which `interactive.param_desc` succeeds.
+This is used to generate the parser documentation that appears in hovers on interactive tactics.
+-/
+meta def unprintable_interactive (d : declaration) : tactic (option string) :=
+match d.to_name with
+| name.mk_string _ (name.mk_string "interactive" (name.mk_string _ name.anonymous)) := do
+  (ds, _) ← mk_local_pis d.type,
+  ds ← ds.mfilter $ λ d, bnot <$> succeeds (interactive.param_desc d.local_type),
+  ff ← return ds.empty | return none,
+  ds ← ds.mmap (pp ∘ to_binder),
+  return $ some $ ds.to_string_aux tt
+| _ := return none
+end
+
+/-- A linter for checking that interactive tactics have parser documentation. -/
+@[linter]
+meta def linter.unprintable_interactive : linter :=
+{ test := unprintable_interactive,
+  auto_decls := tt,
+  no_errors_found := "No tactics are unprintable.",
+  errors_found := "THE FOLLOWING TACTICS ARE UNPRINTABLE. " ++
+"This means that an interactive tactic is using `parse p` where `p` does not have " ++
+"an associated description. You can fix this by wrapping `p` as `with_desc \"p\" p`, " ++
+"and provide the description there, or you can stick to \"approved\" tactic combinators " ++
+"like `?` `*>` `<*` `<*>` `<|>` and `<$>` (but not `>>=` or `do` blocks) " ++
+"that automatically generate a description.",
+  is_fast := tt }

src/tactic/monotonicity/interactive.lean

@@ -609,7 +609,7 @@ meta def assert_or_rule : lean.parser (pexpr ⊕ pexpr) :=
 (tk ":=" *> inl <$> texpr <|> (tk ":" *> inr <$> texpr))
 
 meta def arity : lean.parser rep_arity :=
-rep_arity.many <$ tk "*" <|>
+tk "*" *> pure rep_arity.many <|>
 rep_arity.exactly <$> (tk "^" *> small_nat) <|>
 pure rep_arity.one
 

src/tactic/push_neg.lean

@@ -167,7 +167,7 @@ lemma imp_of_not_imp_not (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) :=
 
 /-- Matches either an identifier "h" or a pair of identifiers "h with k" -/
 meta def name_with_opt : lean.parser (name × option name) :=
-prod.mk <$> ident <*> (some <$> (tk "with" >> ident) <|> return none)
+prod.mk <$> ident <*> (some <$> (tk "with" *> ident) <|> return none)
 
 /--
 Transforms the goal into its contrapositive.

src/tactic/squeeze.lean

@@ -40,17 +40,18 @@ open list
 
 /-- parse structure instance of the shape `{ field1 := value1, .. , field2 := value2 }` -/
 meta def struct_inst : lean.parser pexpr :=
-do tk "{",
-   ls ← sep_by (skip_info (tk ","))
-     ( sum.inl <$> (tk ".." *> texpr) <|>
-       sum.inr <$> (prod.mk <$> ident <* tk ":=" <*> texpr)),
-   tk "}",
-   let (srcs,fields) := partition_map id ls,
-   let (names,values) := unzip fields,
-   pure $ pexpr.mk_structure_instance
-     { field_names := names,
-       field_values := values,
-       sources := srcs }
+with_desc "cfg" $ do
+  tk "{",
+  ls ← sep_by (skip_info (tk ","))
+    ( sum.inl <$> (tk ".." *> texpr) <|>
+      sum.inr <$> (prod.mk <$> ident <* tk ":=" <*> texpr)),
+  tk "}",
+  let (srcs,fields) := partition_map id ls,
+  let (names,values) := unzip fields,
+  pure $ pexpr.mk_structure_instance
+    { field_names := names,
+      field_values := values,
+      sources := srcs }
 
 /-- pretty print structure instance -/
 meta def struct.to_tactic_format (e : pexpr) : tactic format :=