feat: validate that tactic doc features are used on tactics

src/Lean/Elab/Tactic/Doc.lean

@@ -37,7 +37,9 @@ private def asStrLit? : Syntax → Option StrLit
       | throwErrorAt cmd "Malformed documentation comment ({docComment})"
     let tacName ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo tac
     if let some tgt' := aliasOfTactic (← getEnv) tacName then
-        throwError "'{tacName}' is an alias of '{tgt'}'"
+        throwErrorAt tac "'{tacName}' is an alias of '{tgt'}'"
+    if !(isTactic (← getEnv) tacName) then throwErrorAt tac "'{tacName}' is not a tactic"
+
     modifyEnv (tacticDocExtExt.addEntry · (tacName, docComment.getDocString))
     pure ()
   | _ => throwError "Malformed tactic extension command"
@@ -113,7 +115,7 @@ Displays all available tactic tags, with documentation.
 @[builtin_command_elab printTacTags] def elabPrintTacTags : CommandElab := fun _stx => do
   let all :=
     tacticTagExt.toEnvExtension.getState (← getEnv)
-      |>.importedEntries |>.push (tacticTagExt.getState (← getEnv))
+      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (tacticTagExt.getState (← getEnv)))
   let mut mapping : NameMap NameSet := {}
   for arr in all do
     for (tac, tag) in arr do
@@ -163,7 +165,7 @@ def allTacticDocs : MetaM (Array TacticDoc) := do
   let env ← getEnv
   let all :=
     tacticTagExt.toEnvExtension.getState (← getEnv)
-      |>.importedEntries |>.push (tacticTagExt.getState (← getEnv))
+      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (tacticTagExt.getState (← getEnv)))
   let mut tacTags : NameMap NameSet := {}
   for arr in all do
     for (tac, tag) in arr do

src/Lean/Parser/Tactic/Doc.lean

@@ -7,11 +7,22 @@ prelude
 import Lean.Attributes
 import Lean.DocString
 import Lean.Elab.InfoTree.Main
+import Lean.Parser.Extension
 
 set_option linter.missingDocs true
 
 namespace Lean.Parser.Tactic.Doc
 
+open Lean.Parser (registerParserAttributeHook)
+
+/-- Check whether a name is a tactic syntax kind -/
+def isTactic (env : Environment) (kind : Name) : Bool := Id.run do
+  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
+    | return false
+  for (tac, _) in tactics.kinds do
+    if kind == tac then return true
+  return false
+
 /--
 Stores a collection of tactic aliases, to track which new syntax rules represent new forms of
 existing tactics.
@@ -60,10 +71,15 @@ builtin_initialize
       unless ((← getEnv).getModuleIdxFor? decl).isNone do
         throwError "invalid attribute '{name}', declaration is in an imported module"
       let .node _ _ #[.atom _ "tactic_alias", tgt] := stx
-        | throwError "invalid '{name}' attribute {stx}"
+        | throwError "invalid syntax for '{name}' attribute"
 
       let tgtName ← Lean.Elab.realizeGlobalConstNoOverloadWithInfo tgt
 
+      if !(isTactic (← getEnv) tgtName) then throwErrorAt tgt "'{tgtName}' is not a tactic"
+      -- If this condition is true, then we're in an `attribute` command and can validate here.
+      if (← getEnv).find? decl |>.isSome then
+        if !(isTactic (← getEnv) decl) then throwError "'{decl}' is not a tactic"
+
       if let some tgt' := aliasOfTactic (← getEnv) tgtName then
         throwError "'{tgtName}' is itself an alias of '{tgt'}'"
       modifyEnv fun env => tacticAliasExt.addEntry env (decl, tgtName)
@@ -72,9 +88,15 @@ builtin_initialize
           logWarningAt stx m!"Replacing docstring for '{decl}' with the one from '{tgtName}'"
         addDocString decl docs
     descr := "Register a tactic parser as an alias of an existing tactic, so they can be grouped together in documentation.",
-    applicationTime := .afterTypeChecking
+    -- This runs prior to elaboration because it allows a check for whether the decl is present
+    -- in the environment to determine whether we can see if it's a tactic name. This is useful
+    -- when the attribute is applied after definition, using an `attribute` command (error checking
+    -- for the `@[tactic_alias TAC]` syntax is performed by the parser attribute hook). If this
+    -- attribute ran later, then the decl would already be present.
+    applicationTime := .beforeElaboration
   }
 
+
 /--
 The known tactic tags that allow tactics to be grouped by purpose.
 -/
@@ -137,12 +159,17 @@ some other purpose, consider a new representation.
 The first projection in each pair is the tactic name, and the second is the tag name.
 -/
 builtin_initialize tacticTagExt
-    : PersistentEnvExtension (Name × Name) (Name × Name) (Array (Name × Name)) ←
+    : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap NameSet) ←
   registerPersistentEnvExtension {
     mkInitial := pure {},
-    addImportedFn := fun _ => pure #[],
-    addEntryFn := Array.push,
-    exportEntriesFn := id
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun tags (decl, newTag) => tags.insert decl (tags.findD decl {} |>.insert newTag)
+    exportEntriesFn := fun tags => Id.run do
+      let mut exported := #[]
+      for (decl, dTags) in tags do
+        for t in dTags do
+          exported := exported.push (decl, t)
+      exported
   }
 
 builtin_initialize
@@ -152,10 +179,15 @@ builtin_initialize
     ref := by exact decl_name%,
     add := fun decl stx kind => do
       unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
-      let .node _ `Lean.Parser.Attr.tactic_tag #[_, .node _ _ tags] := stx
+      let .node _ `Lean.Parser.Attr.tactic_tag #[_kw, .node _ _ tags] := stx
         | throwError "invalid '{name}' attribute"
+      if (← getEnv).find? decl |>.isSome then
+        if !(isTactic (← getEnv) decl) then
+          throwErrorAt stx "'{decl}' is not a tactic"
+
       if let some tgt' := aliasOfTactic (← getEnv) decl then
-        throwError "'{decl}' is an alias of '{tgt'}'"
+        throwErrorAt stx "'{decl}' is an alias of '{tgt'}'"
+
       for t in tags do
         let tagName := t.getId
         if let some _ ← tagInfo tagName then
@@ -179,7 +211,12 @@ builtin_initialize
           throwErrorAt t (m!"unknown tag '{tagName}' " ++ extra)
     descr := "Register a tactic parser as an alias of an existing tactic, so they can be " ++
       "grouped together in documentation.",
-    applicationTime := .afterTypeChecking
+    -- This runs prior to elaboration because it allows a check for whether the decl is present
+    -- in the environment to determine whether we can see if it's a tactic name. This is useful
+    -- when the attribute is applied after definition, using an `attribute` command (error checking
+    -- for the `@[tactic_tag ...]` syntax is performed by the parser attribute hook). If this
+    -- attribute ran later, then the decl would already be present.
+    applicationTime := .beforeElaboration
   }
 
 /--
@@ -223,3 +260,25 @@ where
     | [] => ""
     | [l] => " * " ++ l ++ "\n\n"
     | l::ls => " * " ++ l ++ "\n" ++ String.join (ls.map indentLine) ++ "\n\n"
+
+
+-- Note: this error handler doesn't prevent all cases of non-tactics being added to the data
+-- structure. But the module will throw errors during elaboration, and there doesn't seem to be
+-- another way to implement this, because the category parser extension attribute runs *after* the
+-- attributes specified before a `syntax` command.
+/--
+Validate that a tactic alias is actually a tactic and that syntax tagged as tactics are tactics
+-/
+def tacticDocsOnTactics : ParserAttributeHook where
+  postAdd (catName declName : Name) (_builtIn : Bool) := do
+    if catName == `tactic then return
+    if aliasOfTactic (← getEnv) declName |>.isSome then
+      throwError m!"'{declName}' is not a tactic"
+    -- It's sufficient to look in the state (and not the imported entries) because this validation
+    -- only needs to check tags added in the current module
+    if let some tags := tacticTagExt.getState (← getEnv) |>.find? declName then
+      if !tags.isEmpty then
+        throwError m!"'{declName}' is not a tactic"
+
+builtin_initialize
+  registerParserAttributeHook tacticDocsOnTactics

tests/lean/run/tacticDoc.lean

@@ -35,10 +35,75 @@ attribute [tactic_tag finishing] Lean.Parser.Tactic.omega
 
 attribute [tactic_tag ctrl] Lean.Parser.Tactic.«tactic_<;>_»
 
+/-!
+# Error Handling
+
+Test error handling. Non-tactics are not eligible to be the target of aliases, to be aliases, or to
+receive tags or doc extensions.
+-/
+
+/-! These tests check that non-tactics can't be aliases -/
+
+/-- error: 'nonTacticTm' is not a tactic -/
+#guard_msgs in
+@[tactic_alias my_trivial]
+syntax (name := nonTacticTm) "nonTactic" : term
+
+syntax (name := nonTacticTm') "nonTactic'" : term
+
+/-- error: 'nonTacticTm'' is not a tactic -/
+#guard_msgs in
+attribute [tactic_alias my_trivial] nonTacticTm'
+
+/-! These tests check that non-tactics can't be aliased -/
+
+/-- error: 'nonTacticTm' is not a tactic -/
+#guard_msgs in
+@[tactic_alias nonTacticTm]
+syntax (name := itsATactic) "yepATactic" : tactic
+
+syntax (name := itsATactic') "yepATactic'" : tactic
+
+/-- error: 'nonTacticTm' is not a tactic -/
+#guard_msgs in
+attribute [tactic_alias nonTacticTm] itsATactic'
+
+
+/-! These tests check that non-tactics can't receive tags -/
+
+/-- error: 'tm' is not a tactic -/
+#guard_msgs in
+@[tactic_tag finishing]
+syntax (name := tm) "someTerm" : term
+
+
+/-- error: 'tm' is not a tactic -/
+#guard_msgs in
+attribute [tactic_tag ctrl] tm
+
+/-! These tests check that only known tags may be applied -/
+
 /-- error: unknown tag 'bogus' (expected one of 'ctrl', 'extensible', 'finishing') -/
 #guard_msgs in
 attribute [tactic_tag bogus] my_trivial
 
+/-- error: unknown tag 'bogus' (expected one of 'ctrl', 'extensible', 'finishing') -/
+#guard_msgs in
+@[tactic_tag bogus]
+syntax "someTactic" : tactic
+
+/-! Check that only canonical tactics may receive doc extensions -/
+
+/-- error: 'nonTacticTm'' is not a tactic -/
+#guard_msgs in
+/-- Some docs that don't belong here -/
+tactic_extension nonTacticTm'
+
+/-- error: 'very_trivial' is an alias of 'my_trivial' -/
+#guard_msgs in
+/-- Some docs that don't belong here -/
+tactic_extension very_trivial
+
 /--
 info: Available tags: ⏎
   • 'ctrl' — "control flow"
@@ -49,7 +114,7 @@ info: Available tags: ⏎
     'my_trivial'
   • 'finishing'
     Finishing tactics that are intended to completely close a goal ⏎
-    'omega', 'my_trivial'
+    'omega', 'my_trivial', 'someTerm'
 -/
 #guard_msgs in
 #print tactic tags