feat: more infrastructure for tactic documentation (#4490)

This is the groundwork for a tactic index in generated documentation, as
there was in Lean 3. There are a few challenges to getting this to work
well in Lean 4:
* There's no natural notion of *tactic identity* - a tactic may be
specified by multiple syntax rules (e.g. the pattern-matching version of
`intro` is specified apart from the default version, but both are the
same from a user perspective)
* There's no natural notion of *tactic name* - here, we take the
pragmatic choice of using the first keyword atom in the tactic's syntax
specification, but this may need to be overridable someday.
* Tactics are extensible, but we don't want to allow arbitrary imports
to clobber existing tactic docstrings, which could become unpredictable
in practice.

For tactic identity, this PR introduces the notion of a *tactic
alternative*, which is a `syntax` specification that is really "the same
as" an existing tactic, but needs to be separate for technical reasons.
This provides a notion of tactic identity, which we can use as the basis
of a tactic index in generated documentation. Alternative forms of
tactics are specified using a new `@[tactic_alt IDENT]` attribute,
applied to the new tactic syntax. It is an error to declare a tactic
syntax rule to be an alternative of another one that is itself an
alternative. Documentation hovers now take alternatives into account,
and display the docs for the canonical name.

*Tactic tags*, created with the `register_tactic_tag` command, specify
tags that may be applied to tactics. This is intended to be used by
doc-gen and Verso. Tags may be applied using the `@[tactic_tag TAG1 TAG2
...]` attribute on a canonical tactic parser, which may be used in any
module to facilitate downstream projects introducing tags that apply to
pre-existing tactics. Tags may not be removed, but it's fine to
redundantly add them. The collection of tags, and the tactics to which
they're applied, can be seen using the `#print tactic tags` command.

*Extension documentation* provides a structured way to document
extensions to tactics. The resulting documentation is gathered into a
bulleted list at the bottom of the tactic's docstring. Extensions are
added using the `tactic_extension TAC` command. This can be used when
adding new interpretations of a tactic via `macro_rules`, when extending
some table or search index used by the tactic, or in any other way. It
is a command to facilitate its flexible use with various extension
mechanisms.

src/Lean/BuiltinDocAttr.lean

@@ -5,12 +5,12 @@ Authors: Mario Carneiro
 -/
 prelude
 import Lean.Compiler.InitAttr
-import Lean.DocString
+import Lean.DocString.Extension
 
 namespace Lean
 
 def declareBuiltinDocStringAndRanges (declName : Name) : AttrM Unit := do
-  if let some doc ← findDocString? (← getEnv) declName (includeBuiltin := false) then
+  if let some doc ← findSimpleDocString? (← getEnv) declName (includeBuiltin := false) then
     declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
   if let some declRanges ← findDeclarationRanges? declName then
     declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])

src/Lean/DocString.lean

@@ -4,58 +4,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.DeclarationRange
-import Lean.MonadEnv
-import Init.Data.String.Extra
+import Lean.DocString.Extension
+import Lean.Parser.Tactic.Doc
+
+set_option linter.missingDocs true
+
+-- This module contains the main query interface for docstrings, which assembles user-visible
+-- docstrings.
+-- The module `Lean.DocString.Extension` contains the underlying data.
 
 namespace Lean
+open Lean.Parser.Tactic.Doc
 
-private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
-private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
+/--
+Finds the docstring for a name, taking tactic alternate forms and documentation extensions into
+account.
 
-def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
-  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
-
-def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
-  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
-    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
-  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
-
-def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
-  match docString? with
-  | some docString => addDocString declName docString
-  | none => return ()
-
-def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
-  if let some docStr := docStringExt.find? env declName then
-    return some docStr
-  else if includeBuiltin then
-    return (← builtinDocStrings.get).find? declName
-  else
-    return none
-
-structure ModuleDoc where
-  doc : String
-  declarationRange : DeclarationRange
-
-private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
-  addImportedFn := fun _ => {}
-  addEntryFn    := fun s e => s.push e
-  toArrayFn     := fun es => es.toArray
-}
-
-def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
-  moduleDocExt.addEntry env doc
-
-def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
-  moduleDocExt.getState env
-
-def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
-  env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
-
-def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
-  match stx.raw[1] with
-  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
-  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
-
-end Lean
+Use `Lean.findSimpleDocString?` to look up the raw docstring without resolving alternate forms or
+including extensions.
+-/
+def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) := do
+  let declName := alternativeOfTactic env declName |>.getD declName
+  let exts := getTacticExtensionString env declName
+  return (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts)

src/Lean/DocString/Extension.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.DeclarationRange
+import Lean.MonadEnv
+import Init.Data.String.Extra
+
+-- This module contains the underlying data for docstrings, with as few imports as possible, so that
+-- docstrings can be saved in as much of the compiler as possible.
+-- The module `Lean.DocString` contains the query interface, which needs to look at additional data
+-- to construct user-visible docstrings.
+
+namespace Lean
+
+private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
+private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
+
+def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
+  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
+
+def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
+  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
+    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
+
+def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
+  match docString? with
+  | some docString => addDocString declName docString
+  | none => return ()
+
+/--
+Finds a docstring without performing any alias resolution or enrichment with extra metadata.
+
+Docstrings to be shown to a user should be looked up with `Lean.findDocString?` instead.
+-/
+def findSimpleDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
+  if let some docStr := docStringExt.find? env declName then
+    return some docStr
+  else if includeBuiltin then
+    return (← builtinDocStrings.get).find? declName
+  else
+    return none
+
+structure ModuleDoc where
+  doc : String
+  declarationRange : DeclarationRange
+
+private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
+  addImportedFn := fun _ => {}
+  addEntryFn    := fun s e => s.push e
+  toArrayFn     := fun es => es.toArray
+}
+
+def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
+  moduleDocExt.addEntry env doc
+
+def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
+  moduleDocExt.getState env
+
+def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
+  env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
+
+def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
+  match stx.raw[1] with
+  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
+  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"

src/Lean/Elab.lean

@@ -50,3 +50,4 @@ import Lean.Elab.ParseImportsFast
 import Lean.Elab.GuardMsgs
 import Lean.Elab.CheckTactic
 import Lean.Elab.MatchExpr
+import Lean.Elab.Tactic.Doc

src/Lean/Elab/InheritDoc.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 prelude
 import Lean.Elab.InfoTree.Main
-import Lean.DocString
+import Lean.DocString.Extension
 
 namespace Lean
 
@@ -21,9 +21,9 @@ builtin_initialize
         let some id := id?
           | throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
         let declName ← Elab.realizeGlobalConstNoOverloadWithInfo id
-        if (← findDocString? (← getEnv) decl).isSome then
+        if (← findSimpleDocString? (← getEnv) decl).isSome then
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
-        let some doc ← findDocString? (← getEnv) declName
+        let some doc ← findSimpleDocString? (← getEnv) declName
           | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"
         addDocString decl doc
       | _  => throwError "invalid `[inherit_doc]` attribute"

src/Lean/Elab/Tactic/Doc.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+prelude
+import Lean.DocString
+import Lean.Elab.Command
+import Lean.Parser.Tactic.Doc
+import Lean.Parser.Command
+
+namespace Lean.Elab.Tactic.Doc
+open Lean.Parser.Tactic.Doc
+open Lean.Elab.Command
+open Lean.Parser.Command
+
+@[builtin_command_elab «tactic_extension»] def elabTacticExtension : CommandElab
+  | `(«tactic_extension»|tactic_extension%$cmd $_) => do
+    throwErrorAt cmd "Missing documentation comment"
+  | `(«tactic_extension»|$docs:docComment tactic_extension $tac:ident) => do
+    let tacName ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo tac
+
+    if let some tgt' := alternativeOfTactic (← getEnv) tacName then
+        throwErrorAt tac "'{tacName}' is an alternative form of '{tgt'}'"
+    if !(isTactic (← getEnv) tacName) then
+      throwErrorAt tac "'{tacName}' is not a tactic"
+
+    modifyEnv (tacticDocExtExt.addEntry · (tacName, docs.getDocString))
+    pure ()
+  | _ => throwError "Malformed tactic extension command"
+
+@[builtin_command_elab «register_tactic_tag»] def elabRegisterTacticTag : CommandElab
+  | `(«register_tactic_tag»|$[$doc:docComment]? register_tactic_tag $tag:ident $user:str) => do
+    let docstring ← doc.mapM getDocStringText
+    modifyEnv (knownTacticTagExt.addEntry · (tag.getId, user.getString, docstring))
+  | _ => throwError "Malformed 'register_tactic_tag' command"
+
+/--
+Gets the first string token in a parser description. For example, for a declaration like
+`syntax "squish " term " with " term : tactic`, it returns `some "squish "`, and for a declaration
+like `syntax tactic " <;;;> " tactic : tactic`, it returns `some " <;;;> "`.
+
+Returns `none` for syntax declarations that don't contain a string constant.
+-/
+private partial def getFirstTk (e : Expr) : MetaM (Option String) := do
+  match (← Meta.whnf e).getAppFnArgs with
+  | (``ParserDescr.node, #[_, _, p]) => getFirstTk p
+  | (``ParserDescr.trailingNode, #[_, _, _, p]) => getFirstTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getFirstTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getFirstTk p
+  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getFirstTk p
+  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
+  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (some tk)
+  | (``Parser.withAntiquot, #[_, p]) => getFirstTk p
+  | (``Parser.leadingNode, #[_, _, p]) => getFirstTk p
+  | (``HAndThen.hAndThen, #[_, _, _, _, p1, p2]) =>
+    if let some tk ← getFirstTk p1 then pure (some tk)
+    else getFirstTk (.app p2 (.const ``Unit.unit []))
+  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
+  | (``Parser.symbol, #[.lit (.strVal tk)]) => pure (some tk)
+  | _ => pure none
+
+
+/--
+Creates some `MessageData` for a parser name.
+
+If the parser name maps to a description with an
+identifiable leading token, then that token is shown. Otherwise, the underlying name is shown
+without an `@`. The name includes metadata that makes infoview hovers and the like work. This
+only works for global constants, as the local context is not included.
+-/
+private def showParserName (n : Name) : MetaM MessageData := do
+  let env ← getEnv
+  let params :=
+    env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
+  let tok ←
+    if let some descr := env.find? n |>.bind (·.value?) then
+      if let some tk ← getFirstTk descr then
+        pure <| Std.Format.text tk.trim
+      else pure <| format n
+    else pure <| format n
+  pure <| .ofFormatWithInfos {
+    fmt := "'" ++ .tag 0 tok ++ "'",
+    infos :=
+      .fromList [(0, .ofTermInfo {
+        lctx := .empty,
+        expr := .const n params,
+        stx := .ident .none (toString n).toSubstring n [.decl n []],
+        elaborator := `Delab,
+        expectedType? := none
+      })] _
+  }
+
+
+/--
+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.exportEntriesFn (tacticTagExt.getState (← getEnv)))
+  let mut mapping : NameMap NameSet := {}
+  for arr in all do
+    for (tac, tag) in arr do
+      mapping := mapping.insert tag (mapping.findD tag {} |>.insert tac)
+
+  let showDocs : Option String → MessageData
+    | none => .nil
+    | some d => Format.line ++ MessageData.joinSep ((d.splitOn "\n").map toMessageData) Format.line
+
+  let showTactics (tag : Name) : MetaM MessageData := do
+    match mapping.find? tag with
+    | none => pure .nil
+    | some tacs =>
+      if tacs.isEmpty then pure .nil
+      else
+        let tacs := tacs.toArray.qsort (·.toString < ·.toString) |>.toList
+        pure (Format.line ++ MessageData.joinSep (← tacs.mapM showParserName) ", ")
+
+  let tagDescrs ← liftTermElabM <| (← allTagsWithInfo).mapM fun (name, userName, docs) => do
+    pure <| m!"• " ++
+      MessageData.nestD (m!"'{name}'" ++
+        (if name.toString != userName then m!" — \"{userName}\"" else MessageData.nil) ++
+        showDocs docs ++
+        (← showTactics name))
+
+  let tagList : MessageData :=
+    m!"Available tags: {MessageData.nestD (Format.line ++ .joinSep tagDescrs Format.line)}"
+
+  logInfo tagList
+
+/--
+The information needed to display all documentation for a tactic.
+-/
+structure TacticDoc where
+  /-- The name of the canonical parser for the tactic -/
+  internalName : Name
+  /-- The user-facing name to display (typically the first keyword token) -/
+  userName : String
+  /-- The tags that have been applied to the tactic -/
+  tags : NameSet
+  /-- The docstring for the tactic -/
+  docString : Option String
+  /-- Any docstring extensions that have been specified -/
+  extensionDocs : Array String
+
+def allTacticDocs : MetaM (Array TacticDoc) := do
+  let env ← getEnv
+  let all :=
+    tacticTagExt.toEnvExtension.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
+      tacTags := tacTags.insert tac (tacTags.findD tac {} |>.insert tag)
+
+  let mut docs := #[]
+
+  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
+    | return #[]
+  for (tac, _) in tactics.kinds do
+    -- Skip noncanonical tactics
+    if let some _ := alternativeOfTactic env tac then continue
+    let userName : String ←
+      if let some descr := env.find? tac |>.bind (·.value?) then
+        if let some tk ← getFirstTk descr then
+          pure tk.trim
+        else pure tac.toString
+      else pure tac.toString
+
+    docs := docs.push {
+      internalName := tac,
+      userName := userName,
+      tags := tacTags.findD tac {},
+      docString := ← findDocString? env tac,
+      extensionDocs := getTacticExtensions env tac
+    }
+  return docs

src/Lean/Parser.lean

@@ -12,6 +12,7 @@ import Lean.Parser.Command
 import Lean.Parser.Module
 import Lean.Parser.Syntax
 import Lean.Parser.Do
+import Lean.Parser.Tactic.Doc
 
 namespace Lean
 namespace Parser

src/Lean/Parser/Attr.lean

@@ -50,6 +50,24 @@ def externEntry := leading_parser
 @[builtin_attr_parser] def extern     := leading_parser
   nonReservedSymbol "extern" >> optional (ppSpace >> numLit) >> many (ppSpace >> externEntry)
 
+/--
+Declare this tactic to be an alias or alternative form of an existing tactic.
+
+This has the following effects:
+ * The alias relationship is saved
+ * The docstring is taken from the original tactic, if present
+-/
+@[builtin_attr_parser] def «tactic_alt» := leading_parser
+  "tactic_alt" >> ppSpace >> ident
+
+/--
+Add one or more tags to a tactic.
+
+Tags should be applied to the canonical names for tactics.
+-/
+@[builtin_attr_parser] def «tactic_tag» := leading_parser
+  "tactic_tag" >> many1 (ppSpace >> ident)
+
 end Attr
 
 end Lean.Parser

src/Lean/Parser/Command.lean

@@ -447,6 +447,11 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
   "#print " >> nonReservedSymbol "axioms " >> ident
 @[builtin_command_parser] def printEqns      := leading_parser
   "#print " >> (nonReservedSymbol "equations " <|> nonReservedSymbol "eqns ") >> ident
+/--
+Displays all available tactic tags, with documentation.
+-/
+@[builtin_command_parser] def printTacTags   := leading_parser
+  "#print " >> nonReservedSymbol "tactic " >> nonReservedSymbol "tags"
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
@@ -669,6 +674,26 @@ Documentation can only be added to declarations in the same module.
 @[builtin_command_parser] def addDocString := leading_parser
   docComment >> "add_decl_doc " >> ident
 
+/--
+Register a tactic tag, saving its user-facing name and docstring.
+
+Tactic tags can be used by documentation generation tools to classify related tactics.
+-/
+@[builtin_command_parser] def «register_tactic_tag» := leading_parser
+  optional (docComment >> ppLine) >>
+  "register_tactic_tag " >> ident >> strLit
+
+/--
+Add more documentation as an extension of the documentation for a given tactic.
+
+The extended documentation is placed in the command's docstring. It is shown as part of a bulleted
+list, so it should be brief.
+-/
+@[builtin_command_parser] def «tactic_extension» := leading_parser
+  optional (docComment >> ppLine) >>
+  "tactic_extension " >> ident
+
+
 /--
   This is an auxiliary command for generation constructor injectivity theorems for
   inductive types defined at `Prelude.lean`.

src/Lean/Parser/Tactic.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Parser.Term
+import Lean.Parser.Tactic.Doc
 
 namespace Lean
 namespace Parser

src/Lean/Parser/Tactic/Doc.lean

@@ -0,0 +1,290 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+prelude
+import Lean.Attributes
+import Lean.DocString.Extension
+import Lean.Elab.InfoTree.Main
+import Lean.Parser.Attr
+import Lean.Parser.Extension
+
+set_option linter.missingDocs true
+
+namespace Lean.Parser.Tactic.Doc
+
+open Lean.Parser (registerParserAttributeHook)
+open Lean.Parser.Attr
+
+/-- 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 alternatives*, to track which new syntax rules represent new forms of
+existing tactics.
+-/
+builtin_initialize tacticAlternativeExt
+    : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap Name) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun as (src, tgt) => as.insert src tgt,
+    exportEntriesFn := fun es =>
+      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/--
+If `tac` is registered as the alternative form of another tactic, then return the canonical name for
+it.
+-/
+def alternativeOfTactic (env : Environment) (tac : Name) : Option Name :=
+  match env.getModuleIdxFor? tac with
+  | some modIdx =>
+    match (tacticAlternativeExt.getModuleEntries env modIdx).binSearch (tac, .anonymous) (Name.quickLt ·.1 ·.1) with
+    | some (_, val) => some val
+    | none => none
+  | none => tacticAlternativeExt.getState env |>.find? tac
+
+/--
+Find all alternatives for a given canonical tactic name.
+-/
+def aliases [Monad m] [MonadEnv m] (tac : Name) : m NameSet := do
+  let env ← getEnv
+  let mut found := {}
+  for (src, tgt) in tacticAlternativeExt.getState env do
+    if tgt == tac then found := found.insert src
+  for arr in tacticAlternativeExt.toEnvExtension.getState env |>.importedEntries do
+    for (src, tgt) in arr do
+      if tgt == tac then found := found.insert src
+  pure found
+
+builtin_initialize
+  let name := `tactic_alt
+  registerBuiltinAttribute {
+    name := name,
+    ref := by exact decl_name%,
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
+      unless ((← getEnv).getModuleIdxFor? decl).isNone do
+        throwError "invalid attribute '{name}', declaration is in an imported module"
+      let `(«tactic_alt»|tactic_alt $tgt) := 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' := alternativeOfTactic (← getEnv) tgtName then
+        throwError "'{tgtName}' is itself an alternative for '{tgt'}'"
+      modifyEnv fun env => tacticAlternativeExt.addEntry env (decl, tgtName)
+      if (← findSimpleDocString? (← getEnv) decl).isSome then
+        logWarningAt stx m!"Docstring for '{decl}' will be ignored because it is an alternative"
+
+    descr :=
+      "Register a tactic parser as an alternative form of an existing tactic, so they " ++
+      "can be grouped together in documentation.",
+    -- 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_alt 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.
+-/
+builtin_initialize knownTacticTagExt
+    : PersistentEnvExtension
+        (Name × String × Option String)
+        (Name × String × Option String)
+        (NameMap (String × Option String)) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun as (src, tgt) => as.insert src tgt,
+    exportEntriesFn := fun es =>
+      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/--
+Get the user-facing name and docstring for a tactic tag.
+-/
+def tagInfo [Monad m] [MonadEnv m] (tag : Name) : m (Option (String × Option String)) := do
+  let env ← getEnv
+  match env.getModuleIdxFor? tag with
+  | some modIdx =>
+    match (knownTacticTagExt.getModuleEntries env modIdx).binSearch (tag, default) (Name.quickLt ·.1 ·.1) with
+    | some (_, val) => pure (some val)
+    | none => pure none
+  | none => pure (knownTacticTagExt.getState env |>.find? tag)
+
+/-- Enumerate the tactic tags that are available -/
+def allTags [Monad m] [MonadEnv m] : m (List Name) := do
+  let env ← getEnv
+  let mut found : NameSet := {}
+  for (tag, _) in knownTacticTagExt.getState env do
+    found := found.insert tag
+  for arr in knownTacticTagExt.toEnvExtension.getState env |>.importedEntries do
+    for (tag, _) in arr do
+      found := found.insert tag
+  pure (found.toArray.qsort (·.toString < ·.toString) |>.toList)
+
+/-- Enumerate the tactic tags that are available, with their user-facing name and docstring -/
+def allTagsWithInfo [Monad m] [MonadEnv m] : m (List (Name × String × Option String)) := do
+  let env ← getEnv
+  let mut found : NameMap (String × Option String) := {}
+  for (tag, info) in knownTacticTagExt.getState env do
+    found := found.insert tag info
+  for arr in knownTacticTagExt.toEnvExtension.getState env |>.importedEntries do
+    for (tag, info) in arr do
+      found := found.insert tag info
+  let arr := found.fold (init := #[]) (fun arr k v => arr.push (k, v))
+  pure (arr.qsort (·.1.toString < ·.1.toString) |>.toList)
+
+/--
+The mapping between tags and tactics. Tags may be applied in any module, not just the defining
+module for the tactic.
+
+Because this is expected to be augmented regularly, but queried rarely (only when generating
+documentation indices), it is just stored as flat unsorted arrays of pairs. Before it is used for
+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) (NameMap NameSet) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    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
+  let name := `tactic_tag
+  registerBuiltinAttribute {
+    name := name,
+    ref := by exact decl_name%,
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
+      let `(«tactic_tag»|tactic_tag $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' := alternativeOfTactic (← getEnv) decl then
+        throwErrorAt stx "'{decl}' is an alternative form of '{tgt'}'"
+
+      for t in tags do
+        let tagName := t.getId
+        if let some _ ← tagInfo tagName then
+          modifyEnv (tacticTagExt.addEntry · (decl, tagName))
+        else
+          let all ← allTags
+          let extra : MessageData :=
+              let count := all.length
+              let name := (m!"'{·}'")
+              let suggestions :=
+                if count == 0 then m!"(no tags defined)"
+                else if count == 1 then
+                  MessageData.joinSep (all.map name) ", "
+                else if count < 10 then
+                  m!"one of " ++ MessageData.joinSep (all.map name) ", "
+                else
+                  m!"one of " ++
+                  MessageData.joinSep (all.take 10 |>.map name) ", " ++ ", ..."
+              m!"(expected {suggestions})"
+
+          throwErrorAt t (m!"unknown tag '{tagName}' " ++ extra)
+    descr := "Register a tactic parser as an alternative of an existing tactic, so they can be " ++
+      "grouped together in documentation.",
+    -- 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
+  }
+
+/--
+Extensions to tactic documentation.
+
+This provides a structured way to indicate that an extensible tactic has been extended (for
+instance, new cases tried by `trivial`).
+-/
+builtin_initialize tacticDocExtExt
+    : PersistentEnvExtension (Name × Array String) (Name × String) (NameMap (Array String)) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun es (x, ext) => es.insert x (es.findD x #[] |>.push ext),
+    exportEntriesFn := fun es =>
+      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/-- Gets the extensions declared for the documentation for the given canonical tactic name -/
+def getTacticExtensions (env : Environment) (tactic : Name) : Array String := Id.run do
+  let mut extensions := #[]
+  -- Extensions may be declared in any module, so they must all be searched
+  for modArr in tacticDocExtExt.toEnvExtension.getState env |>.importedEntries do
+    if let some (_, strs) := modArr.binSearch (tactic, #[]) (Name.quickLt ·.1 ·.1) then
+      extensions := extensions ++ strs
+  if let some strs := tacticDocExtExt.getState env |>.find? tactic then
+    extensions := extensions ++ strs
+  pure extensions
+
+/-- Gets the rendered extensions for the given canonical tactic name -/
+def getTacticExtensionString (env : Environment) (tactic : Name) : String := Id.run do
+  let exts := getTacticExtensions env tactic
+  if exts.size == 0 then ""
+  else "\n\nExtensions:\n\n" ++ String.join (exts.toList.map bullet) |>.trimRight
+where
+  indentLine (str: String) : String :=
+    (if str.all (·.isWhitespace) then str else "   " ++ str) ++ "\n"
+  bullet (str : String) : String :=
+    let lines := str.splitOn "\n"
+    match lines with
+    | [] => ""
+    | [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.
+/--
+Validates that a tactic alternative 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 alternativeOfTactic (← 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

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -10,6 +10,8 @@ import Lean.DeclarationRange
 import Lean.Data.Json
 import Lean.Data.Lsp
 
+import Lean.Parser.Tactic.Doc
+
 import Lean.Server.FileWorker.Utils
 import Lean.Server.Requests
 import Lean.Server.Completion
@@ -24,6 +26,8 @@ open Lsp
 open RequestM
 open Snapshots
 
+open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
+
 def handleCompletion (p : CompletionParams)
     : RequestM (RequestTask CompletionList) := do
   let doc ← readDoc
@@ -85,7 +89,8 @@ def handleHover (p : HoverParams)
       let stxDoc? ← match stack? with
         | some stack => stack.findSomeM? fun (stx, _) => do
           let .node _ kind _ := stx | pure none
-          return (← findDocString? snap.env kind).map (·, stx.getRange?.get!)
+          let docStr ← findDocString? snap.env kind
+          return docStr.map (·, stx.getRange?.get!)
         | none => pure none
 
       -- now try info tree

src/Lean/Server/InfoUtils.lean

@@ -5,10 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
 prelude
+import Lean.DocString
 import Lean.PrettyPrinter
+import Lean.Parser.Tactic.Doc
 
 namespace Lean.Elab
 
+open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
+
 /-- Elaborator information with elaborator context.
 
 It can be thought of as a "thunked" elaboration computation that allows us
@@ -244,7 +248,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
   match i with
   | .ofTermInfo ti =>
     if let some n := ti.expr.constName? then
-      return ← findDocString? env n
+      return (← findDocString? env n)
   | .ofFieldInfo fi => return ← findDocString? env fi.projName
   | .ofOptionInfo oi =>
     if let some doc ← findDocString? env oi.declName then
@@ -258,6 +262,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
   return none
 
+
 /-- Construct a hover popup, if any, from an info node in a context.-/
 def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option FormatWithInfos) := do
   ci.runMetaM i.lctx do

src/lake/Lake/Load/Lean/Eval.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 import Lake.DSL.Attributes
 import Lake.Config.Workspace
+import Lean.DocString
 
 /-! # Lean Configuration Evaluator
 

src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);

tests/lean/interactive/hoverTacticExt.lean

@@ -0,0 +1,61 @@
+
+
+
+/-!
+Tests that docstring hovers are computed correctly for tactic extensions
+-/
+
+/-- Another `trivial` tactic -/
+syntax (name := my_trivial) "my_trivial" : tactic
+
+@[tactic_alt my_trivial]
+syntax (name := very_trivial) "very_trivial" : tactic
+macro_rules
+| `(tactic|very_trivial) => `(tactic|my_trivial)
+
+/-- It tries Lean's `trivial` -/
+tactic_extension my_trivial
+               --^ textDocument/hover
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|trivial)
+             --^ textDocument/hover
+
+/-- It tries `simp_all` -/
+tactic_extension my_trivial
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|simp_all; done)
+
+
+example : True := by
+  my_trivial
+      --^ textDocument/hover
+
+/-- It tries `constructor` -/
+tactic_extension my_trivial
+               --^ textDocument/hover
+-- On the preceding line, it was not yet extended.
+-- Here, it is:
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|constructor; done)
+           --^ textDocument/hover
+
+/--
+It tries some useful things:
+ * `omega`
+ * `simp_arith [*]`
+-/
+tactic_extension my_trivial
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|omega)
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|simp_arith [*]; done)
+
+-- This tests that nested lists work
+example : True := by
+  my_trivial
+      --^ textDocument/hover
+
+-- This tests that alts are resolved
+example : True := by
+  very_trivial
+      --^ textDocument/hover

tests/lean/interactive/hoverTacticExt.lean.expected.out

@@ -0,0 +1,56 @@
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 16, "character": 17}}
+{"range":
+ {"start": {"line": 16, "character": 17}, "end": {"line": 16, "character": 27}},
+ "contents":
+ {"value":
+  "```lean\nmy_trivial : Lean.ParserDescr\n```\n***\nAnother `trivial` tactic ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 19, "character": 15}}
+{"range":
+ {"start": {"line": 19, "character": 13}, "end": {"line": 19, "character": 23}},
+ "contents":
+ {"value":
+  "Another `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial`",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 29, "character": 8}}
+{"range":
+ {"start": {"line": 29, "character": 2}, "end": {"line": 29, "character": 12}},
+ "contents":
+ {"value":
+  "Another `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial` \n\n * It tries `simp_all`",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 33, "character": 17}}
+{"range":
+ {"start": {"line": 33, "character": 17}, "end": {"line": 33, "character": 27}},
+ "contents":
+ {"value":
+  "```lean\nmy_trivial : Lean.ParserDescr\n```\n***\nAnother `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial` \n\n * It tries `simp_all`",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 38, "character": 13}}
+{"range":
+ {"start": {"line": 38, "character": 13}, "end": {"line": 38, "character": 23}},
+ "contents":
+ {"value":
+  "Another `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial` \n\n * It tries `simp_all` \n\n * It tries `constructor`",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 54, "character": 8}}
+{"range":
+ {"start": {"line": 54, "character": 2}, "end": {"line": 54, "character": 12}},
+ "contents":
+ {"value":
+  "Another `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial` \n\n * It tries `simp_all` \n\n * It tries `constructor` \n\n * It tries some useful things:\n    * `omega`\n    * `simp_arith [*]`",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 59, "character": 8}}
+{"range":
+ {"start": {"line": 59, "character": 2}, "end": {"line": 59, "character": 14}},
+ "contents":
+ {"value":
+  "Another `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial` \n\n * It tries `simp_all` \n\n * It tries `constructor` \n\n * It tries some useful things:\n    * `omega`\n    * `simp_arith [*]`",
+  "kind": "markdown"}}

tests/lean/run/tacticDoc.lean

@@ -0,0 +1,136 @@
+/-!
+Test the commands and attributes for interacting with tactic documentation.
+
+Note that when the standard library starts shipping with actual tags, then this test will need to be
+adjusted or rewritten, as it depends on the complete set of tags that are transitively accessible.
+We don't expect to modify the default tactics often, and it should be a matter of accepting changes
+from #guard_msgs.
+-/
+
+set_option guard_msgs.diff true
+
+/-- Finishing tactics that are intended to completely close a goal -/
+register_tactic_tag finishing "finishing"
+
+/-- Tactics that are intended to be extensible -/
+register_tactic_tag extensible "extensible"
+
+/-- Tactics that sequence or arrange other tactics -/
+register_tactic_tag ctrl "control flow"
+
+/-- Another `trivial` tactic -/
+@[tactic_tag finishing extensible]
+syntax (name := my_trivial) "my_trivial" : tactic
+
+@[tactic_alt my_trivial]
+syntax (name := very_trivial) "very_trivial" : tactic
+
+/-- It tries Lean's `trivial` -/
+tactic_extension my_trivial
+
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|trivial)
+
+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 alternatives, to be
+alternatives themselves, or to receive tags or doc extensions.
+-/
+
+/-! These tests check that non-tactics can't be alternative forms of tactics -/
+
+/-- error: 'nonTacticTm' is not a tactic -/
+#guard_msgs in
+@[tactic_alt my_trivial]
+syntax (name := nonTacticTm) "nonTactic" : term
+
+syntax (name := nonTacticTm') "nonTactic'" : term
+
+/-- error: 'nonTacticTm'' is not a tactic -/
+#guard_msgs in
+attribute [tactic_alt my_trivial] nonTacticTm'
+
+/-! These tests check that non-tactics can't have tactic alternatives -/
+
+/-- error: 'nonTacticTm' is not a tactic -/
+#guard_msgs in
+@[tactic_alt nonTacticTm]
+syntax (name := itsATactic) "yepATactic" : tactic
+
+syntax (name := itsATactic') "yepATactic'" : tactic
+
+/-- error: 'nonTacticTm' is not a tactic -/
+#guard_msgs in
+attribute [tactic_alt 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 alternative form of 'my_trivial' -/
+#guard_msgs in
+/-- Some docs that don't belong here -/
+tactic_extension very_trivial
+
+/-! Check that warnings are issued if alternatives have their own docstrings -/
+
+/-- warning: Docstring for 'tacticAnother' will be ignored because it is an alternative -/
+#guard_msgs in
+/-- Docs -/
+@[tactic_alt my_trivial]
+syntax "another" : tactic
+
+/-- Docs -/
+syntax (name := yetAnother) "yetAnother" : tactic
+
+/-- warning: Docstring for 'yetAnother' will be ignored because it is an alternative -/
+#guard_msgs in
+attribute [tactic_alt my_trivial] «yetAnother»
+
+/-! # Querying Tactic Docs -/
+/--
+info: Available tags: ⏎
+  • 'ctrl' — "control flow"
+    Tactics that sequence or arrange other tactics ⏎
+    '<;>'
+  • 'extensible'
+    Tactics that are intended to be extensible ⏎
+    'my_trivial'
+  • 'finishing'
+    Finishing tactics that are intended to completely close a goal ⏎
+    'omega', 'my_trivial', 'someTerm'
+-/
+#guard_msgs in
+#print tactic tags