fix: make the allowed unused tactics extensible (#14557)

This PR allows to change the tactics that the unused tactic linter ignores.

The main use-case is allowing `done` at the end of proofs, which is very useful for teaching purposes.  See for instance [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Disable.20.60linter.2EunusedTactic.60.20warning.20for.20.60done.60).

Author: adomani

Mathlib/Tactic/Linter/UnusedTactic.lean

@@ -66,31 +66,48 @@ namespace UnusedTactic
 /-- The monad for collecting the ranges of the syntaxes that do not modify any goal. -/
 abbrev M := StateRefT (HashMap String.Range Syntax) IO
 
-/-- `Parser`s allowed to not change the tactic state. -/
-def allowed : HashSet SyntaxNodeKind := HashSet.empty
-  |>.insert `Mathlib.Tactic.Says.says
-  |>.insert `Batteries.Tactic.«tacticOn_goal-_=>_»
-  -- attempt to speed up, by ignoring more tactics
-  |>.insert `by
-  |>.insert `null
-  |>.insert `«]»
-  |>.insert ``Lean.Parser.Term.byTactic
-  |>.insert ``Lean.Parser.Tactic.tacticSeq
-  |>.insert ``Lean.Parser.Tactic.tacticSeq1Indented
-  |>.insert ``Lean.Parser.Tactic.tacticTry_
-
-  -- the following `SyntaxNodeKind`s play a role in silencing `test`s
-  |>.insert ``Lean.Parser.Tactic.guardHyp
-  |>.insert ``Lean.Parser.Tactic.guardTarget
-  |>.insert ``Lean.Parser.Tactic.failIfSuccess
-  |>.insert `Mathlib.Tactic.successIfFailWithMsg
-  |>.insert `Mathlib.Tactic.failIfNoProgress
-  |>.insert `Mathlib.Tactic.ExtractGoal.extractGoal
-  |>.insert `Mathlib.Tactic.Propose.propose'
-  |>.insert `Lean.Parser.Tactic.traceState
-  |>.insert `Mathlib.Tactic.tacticMatch_target_
-  |>.insert `change?
-  |>.insert `«tactic#adaptation_note_»
+/-- `Parser`s allowed to not change the tactic state.
+This can be increased dynamically, using `#allow_unused_tactic`.
+-/
+initialize allowedRef : IO.Ref (HashSet SyntaxNodeKind) ←
+  IO.mkRef <| HashSet.empty
+    |>.insert `Mathlib.Tactic.Says.says
+    |>.insert `Batteries.Tactic.«tacticOn_goal-_=>_»
+    -- attempt to speed up, by ignoring more tactics
+    |>.insert `by
+    |>.insert `null
+    |>.insert `«]»
+    |>.insert ``Lean.Parser.Term.byTactic
+    |>.insert ``Lean.Parser.Tactic.tacticSeq
+    |>.insert ``Lean.Parser.Tactic.tacticSeq1Indented
+    |>.insert ``Lean.Parser.Tactic.tacticTry_
+    -- the following `SyntaxNodeKind`s play a role in silencing `test`s
+    |>.insert ``Lean.Parser.Tactic.guardHyp
+    |>.insert ``Lean.Parser.Tactic.guardTarget
+    |>.insert ``Lean.Parser.Tactic.failIfSuccess
+    |>.insert `Mathlib.Tactic.successIfFailWithMsg
+    |>.insert `Mathlib.Tactic.failIfNoProgress
+    |>.insert `Mathlib.Tactic.ExtractGoal.extractGoal
+    |>.insert `Mathlib.Tactic.Propose.propose'
+    |>.insert `Lean.Parser.Tactic.traceState
+    |>.insert `Mathlib.Tactic.tacticMatch_target_
+    |>.insert `change?
+    |>.insert `«tactic#adaptation_note_»
+
+/-- `#allow_unused_tactic` takes an input a space-separated list of identifiers.
+These identifiers are then allowed by the unused tactic linter:
+even if these tactics do not modify goals, there will be no warning emitted.
+Note: for this to work, these identifiers should be the `SyntaxNodeKind` of each tactic.
+
+For instance, you can allow the `done` and `skip` tactics using
+```lean
+#allow_unused_tactic Lean.Parser.Tactic.done Lean.Parser.Tactic.skip
+```
+Notice that you should use the `SyntaxNodeKind` of the tactic.
+-/
+elab "#allow_unused_tactic " ids:ident* : command => do
+  let ids := ← Command.liftCoreM do ids.mapM realizeGlobalConstNoOverload
+  allowedRef.modify (·.insertMany ids)
 
 /--
 A list of blacklisted syntax kinds, which are expected to have subterms that contain
@@ -161,7 +178,7 @@ partial def eraseUsedTactics : InfoTree → M Unit
       let stx := i.stx
       let kind := stx.getKind
       if let some r := stx.getRange? true then
-        if allowed.contains kind
+        if (← allowedRef.get).contains kind
         -- if the tactic is allowed to not change the goals
         then modify (·.erase r)
         else

test/UnusedTactic.lean

@@ -15,10 +15,27 @@ set_option linter.unusedTactic false
 /--
 warning: 'congr' tactic does nothing
 note: this linter can be disabled with `set_option linter.unusedTactic false`
+---
+warning: 'done' tactic does nothing
+note: this linter can be disabled with `set_option linter.unusedTactic false`
 -/
 #guard_msgs in
 set_option linter.unusedTactic true in
 -- the linter notices that `congr` is unused
 example : True := by
   congr
   constructor
+  done
+
+section allowing_more_unused_tactics
+--  test that allowing more unused tactics has the desired effect of silencing the linter
+#allow_unused_tactic Lean.Parser.Tactic.done Lean.Parser.Tactic.skip
+
+#guard_msgs in
+set_option linter.unusedTactic true in
+example : True := by
+  skip
+  constructor
+  done
+
+end allowing_more_unused_tactics