Lean4
/-- `getDeprecatedSyntax t` returns all usages of deprecated syntax in the input syntax `t`. -/
partial def getDeprecatedSyntax : Syntax → Array (SyntaxNodeKind × Syntax × MessageData)
| stx@(.node _ kind args) =>
let rargs := args.flatMap getDeprecatedSyntax
match kind with
| ``Lean.Parser.Tactic.refine' =>
rargs.push
(kind, stx,
"The `refine'` tactic is discouraged: \
please strongly consider using `refine` or `apply` instead.")
| `Mathlib.Tactic.cases' =>
rargs.push
(kind, stx,
"The `cases'` tactic is discouraged: \
please strongly consider using `obtain`, `rcases` or `cases` instead.")
| `Mathlib.Tactic.induction' =>
rargs.push
(kind, stx,
"The `induction'` tactic is discouraged: \
please strongly consider using `induction` instead.")
| ``Lean.Parser.Tactic.tacticAdmit =>
rargs.push
(kind, stx,
"The `admit` tactic is discouraged: \
please strongly consider using the synonymous `sorry` instead.")
| ``Lean.Parser.Tactic.decide =>
if isDecideNative stx then
rargs.push
(kind, stx,
"Using `decide +native` is not allowed in mathlib: \
because it trusts the entire Lean compiler (not just the Lean kernel), \
it could quite possibly be used to prove false.")
else rargs
| ``Lean.Parser.Tactic.nativeDecide =>
rargs.push
(kind, stx,
"Using `native_decide` is not allowed in mathlib: \
because it trusts the entire Lean compiler (not just the Lean kernel), \
it could quite possibly be used to prove false.")
| ``Lean.Parser.Command.in =>
match getSetOptionMaxHeartbeatsComment stx with
| none => rargs
| some (opt, n, trailing) =>
-- Since we are now seeing the currently outermost `maxHeartbeats` option,
-- we remove all subsequent potential flags and only decide whether to lint or not
-- based on whether the current option has a comment.
let rargs := rargs.filter (·.1 != `MaxHeartbeats)
if trailing.toString.trimLeft.isEmpty then
rargs.push
(`MaxHeartbeats, stx,
s! "Please, add a comment explaining the need for modifying the maxHeartbeat limit, \
as in\nset_option {opt } {n} in\n-- reason for change\n...")
else rargs
| _ => rargs
| _ => default
