chore: rename tactic aliases to tactic alternatives

src/Lean/Elab/Tactic/Doc.lean

@@ -36,8 +36,8 @@ private def asStrLit? : Syntax → Option StrLit
     let some docComment := asDocComment? docComment
       | throwErrorAt cmd "Malformed documentation comment ({docComment})"
     let tacName ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo tac
-    if let some tgt' := aliasOfTactic (← getEnv) tacName then
-        throwErrorAt tac "'{tacName}' is an alias of '{tgt'}'"
+    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, docComment.getDocString))
@@ -177,7 +177,7 @@ def allTacticDocs : MetaM (Array TacticDoc) := do
     | return #[]
   for (tac, _) in tactics.kinds do
     -- Skip noncanonical tactics
-    if let some _ := aliasOfTactic env tac then continue
+    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

src/Lean/Parser/Attr.lean

@@ -57,8 +57,8 @@ 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_alias := leading_parser
-  "tactic_alias" >> ppSpace >> ident
+@[builtin_attr_parser] def tactic_alt := leading_parser
+  "tactic_alt" >> ppSpace >> ident
 
 /--
 Add one or more tags to a tactic.

src/Lean/Parser/Tactic/Doc.lean

@@ -24,10 +24,10 @@ def isTactic (env : Environment) (kind : Name) : Bool := Id.run do
   return false
 
 /--
-Stores a collection of tactic aliases, to track which new syntax rules represent new forms of
+Stores a collection of *tactic alternatives*, to track which new syntax rules represent new forms of
 existing tactics.
 -/
-builtin_initialize tacticAliasExt
+builtin_initialize tacticAlternativeExt
     : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap Name) ←
   registerPersistentEnvExtension {
     mkInitial := pure {},
@@ -38,39 +38,40 @@ builtin_initialize tacticAliasExt
   }
 
 /--
-If `tac` is registered as the alias of another tactic, then return the canonical name for it.
+If `tac` is registered as the alternative form of another tactic, then return the canonical name for
+it.
 -/
-def aliasOfTactic (env : Environment) (tac : Name) : Option Name :=
+def alternativeOfTactic (env : Environment) (tac : Name) : Option Name :=
   match env.getModuleIdxFor? tac with
   | some modIdx =>
-    match (tacticAliasExt.getModuleEntries env modIdx).binSearch (tac, .anonymous) (Name.quickLt ·.1 ·.1) with
+    match (tacticAlternativeExt.getModuleEntries env modIdx).binSearch (tac, .anonymous) (Name.quickLt ·.1 ·.1) with
     | some (_, val) => some val
     | none => none
-  | none => tacticAliasExt.getState env |>.find? tac
+  | none => tacticAlternativeExt.getState env |>.find? tac
 
 /--
-Find all aliases of a given canonical tactic name.
+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 tacticAliasExt.getState env do
+  for (src, tgt) in tacticAlternativeExt.getState env do
     if tgt == tac then found := found.insert src
-  for arr in tacticAliasExt.toEnvExtension.getState env |>.importedEntries do
+  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_alias
+  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 .node _ _ #[.atom _ "tactic_alias", tgt] := stx
+      let .node _ _ #[.atom _ "tactic_alt", tgt] := stx
         | throwError "invalid syntax for '{name}' attribute"
 
       let tgtName ← Lean.Elab.realizeGlobalConstNoOverloadWithInfo tgt
@@ -80,18 +81,20 @@ builtin_initialize
       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)
+      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 let some docs ← findDocString? (← getEnv) tgtName then
         if (← findDocString? (← getEnv) decl).isSome then
           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.",
+    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_alias TAC]` syntax is performed by the parser attribute hook). If this
+    -- 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
   }
@@ -185,8 +188,8 @@ builtin_initialize
         if !(isTactic (← getEnv) decl) then
           throwErrorAt stx "'{decl}' is not a tactic"
 
-      if let some tgt' := aliasOfTactic (← getEnv) decl then
-        throwErrorAt stx "'{decl}' is an alias of '{tgt'}'"
+      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
@@ -209,7 +212,7 @@ builtin_initialize
               m!"(expected {suggestions})"
 
           throwErrorAt t (m!"unknown tag '{tagName}' " ++ extra)
-    descr := "Register a tactic parser as an alias of an existing tactic, so they can be " ++
+    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
@@ -267,12 +270,13 @@ where
 -- 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
+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 aliasOfTactic (← getEnv) declName |>.isSome then
+    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

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -26,7 +26,7 @@ open Lsp
 open RequestM
 open Snapshots
 
-open Lean.Parser.Tactic.Doc (aliasOfTactic getTacticExtensionString)
+open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
 
 def handleCompletion (p : CompletionParams)
     : RequestM (RequestTask CompletionList) := do
@@ -89,8 +89,8 @@ def handleHover (p : HoverParams)
       let stxDoc? ← match stack? with
         | some stack => stack.findSomeM? fun (stx, _) => do
           let .node _ kind _ := stx | pure none
-          -- If the tactic is an alias, get the docs for the canonical version
-          let kind := aliasOfTactic snap.env kind |>.getD kind
+          -- If the tactic is an alternative form, get the docs for the canonical version
+          let kind := alternativeOfTactic snap.env kind |>.getD kind
           let exts := getTacticExtensionString snap.env kind
           let docStr := (← findDocString? snap.env kind).map (· ++ exts)
           return docStr.map (·, stx.getRange?.get!)

src/Lean/Server/InfoUtils.lean

@@ -10,7 +10,7 @@ import Lean.Parser.Tactic.Doc
 
 namespace Lean.Elab
 
-open Lean.Parser.Tactic.Doc (aliasOfTactic getTacticExtensionString)
+open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
 
 /-- Elaborator information with elaborator context.
 
@@ -262,11 +262,11 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
   return none
 where
   /--
-  Find the docstring for a name, resolving tactic aliases and additionally adding tactic extension
-  documentation
+  Find the docstring for a name, resolving tactic alternatives and additionally adding tactic
+  extension documentation
   -/
   docsWithTacExt? env n := do
-    let n := aliasOfTactic env n |>.getD n
+    let n := alternativeOfTactic env n |>.getD n
     return (← findDocString? env n).map (· ++ getTacticExtensionString env n)
 
 /-- Construct a hover popup, if any, from an info node in a context.-/

tests/lean/interactive/hoverTacticExt.lean

@@ -8,7 +8,7 @@ Tests that docstring hovers are computed correctly for tactic extensions
 /-- Another `trivial` tactic -/
 syntax (name := my_trivial) "my_trivial" : tactic
 
-@[tactic_alias my_trivial]
+@[tactic_alt my_trivial]
 syntax (name := very_trivial) "very_trivial" : tactic
 macro_rules
 | `(tactic|very_trivial) => `(tactic|my_trivial)
@@ -55,7 +55,7 @@ example : True := by
   my_trivial
       --^ textDocument/hover
 
--- This tests that aliases are resolved
+-- This tests that alts are resolved
 example : True := by
   very_trivial
       --^ textDocument/hover

tests/lean/run/tacticDoc.lean

@@ -22,7 +22,7 @@ register_tactic_tag ctrl "control flow"
 @[tactic_tag finishing extensible]
 syntax (name := my_trivial) "my_trivial" : tactic
 
-@[tactic_alias my_trivial]
+@[tactic_alt my_trivial]
 syntax (name := very_trivial) "very_trivial" : tactic
 
 /-- It tries Lean's `trivial` -/
@@ -38,35 +38,35 @@ 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.
+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 aliases -/
+/-! These tests check that non-tactics can't be alternative forms of tactics -/
 
 /-- error: 'nonTacticTm' is not a tactic -/
 #guard_msgs in
-@[tactic_alias my_trivial]
+@[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_alias my_trivial] nonTacticTm'
+attribute [tactic_alt my_trivial] nonTacticTm'
 
-/-! These tests check that non-tactics can't be aliased -/
+/-! These tests check that non-tactics can't have tactic alternatives -/
 
 /-- error: 'nonTacticTm' is not a tactic -/
 #guard_msgs in
-@[tactic_alias nonTacticTm]
+@[tactic_alt 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'
+attribute [tactic_alt nonTacticTm] itsATactic'
 
 
 /-! These tests check that non-tactics can't receive tags -/
@@ -99,7 +99,7 @@ syntax "someTactic" : tactic
 /-- Some docs that don't belong here -/
 tactic_extension nonTacticTm'
 
-/-- error: 'very_trivial' is an alias of 'my_trivial' -/
+/-- error: 'very_trivial' is an alternative form of 'my_trivial' -/
 #guard_msgs in
 /-- Some docs that don't belong here -/
 tactic_extension very_trivial