feat: recommended_spelling command

src/Lean/DocString.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.DocString.Extension
 import Lean.Parser.Tactic.Doc
+import Lean.Parser.Term.Doc
 
 set_option linter.missingDocs true
 
@@ -15,6 +16,7 @@ set_option linter.missingDocs true
 
 namespace Lean
 open Lean.Parser.Tactic.Doc
+open Lean.Parser.Term.Doc
 
 /--
 Finds the docstring for a name, taking tactic alternate forms and documentation extensions into
@@ -26,4 +28,5 @@ 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)
+  let spellings := getRecommendedSpellingString env declName
+  return (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts ++ spellings)

src/Lean/Elab.lean

@@ -54,3 +54,4 @@ import Lean.Elab.CheckTactic
 import Lean.Elab.MatchExpr
 import Lean.Elab.Tactic.Doc
 import Lean.Elab.Time
+import Lean.Elab.RecommendedSpelling

src/Lean/Elab/RecommendedSpelling.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Lean.Parser.Term.Doc
+import Lean.Parser.Command
+import Lean.Elab.Command
+
+namespace Lean.Elab.Term.Doc
+open Lean.Parser.Term.Doc
+open Lean.Elab.Command
+open Lean.Parser.Command
+
+@[builtin_command_elab «recommended_spelling»] def elabRecommendedSpelling : CommandElab
+  | `(«recommended_spelling»|$[$docs:docComment]? recommended_spelling $spelling:str for $«notation»:str in [$[$decls:ident],*]) => do
+    let declNames ← liftTermElabM <| decls.mapM (fun decl => realizeGlobalConstNoOverloadWithInfo decl)
+    let recommendedSpelling : RecommendedSpelling := {
+      «notation» := «notation».getString
+      recommendedSpelling := spelling.getString
+      additionalInformation? := docs.map (·.getDocString)
+    }
+    modifyEnv (addRecommendedSpelling · recommendedSpelling declNames)
+  | _ => throwError "Malformed recommended spelling command"
+
+/-- Returns an array containing all recommended spellings. -/
+def allRecommendedSpellings : MetaM (Array RecommendedSpelling) := do
+  let all := recommendedSpellingExt.toEnvExtension.getState (← getEnv)
+      |>.importedEntries
+      |>.push (recommendedSpellingExt.exportEntriesFn (recommendedSpellingExt.getState (← getEnv)))
+  return all.flatMap id
+
+end Lean.Elab.Term.Doc

src/Lean/Parser/Command.lean

@@ -736,7 +736,7 @@ Documentation can only be added to declarations in the same module.
   docComment >> "add_decl_doc " >> ident
 
 /--
-Register a tactic tag, saving its user-facing name and docstring.
+Registers a tactic tag, saving its user-facing name and docstring.
 
 Tactic tags can be used by documentation generation tools to classify related tactics.
 -/
@@ -745,7 +745,7 @@ Tactic tags can be used by documentation generation tools to classify related ta
   "register_tactic_tag " >> ident >> strLit
 
 /--
-Add more documentation as an extension of the documentation for a given tactic.
+Adds 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.
@@ -754,6 +754,47 @@ list, so it should be brief.
   optional (docComment >> ppLine) >>
   "tactic_extension " >> ident
 
+/--
+Documents a recommended spelling for a notation in identifiers.
+
+Theorems should generally be systematically named after their statement, rather than creatively.
+Non-identifier notations should be referred to consistently by their recommended spelling.
+
+```
+/-- some additional info -/
+recommended_spelling "and" for "∧" in [And, «term_∧_»]
+```
+
+will do the following:
+* Adds the sentence "The recommended spelling of `∧` in identifiers is `and` (some additional info)."
+  to the end of the docstring for `And` and for `∧`. If the additional info is more than a single
+  line, it will be placed below the sentence instead of in parentheses.
+* Registers this information in an environment extension, so that it will later be possible to
+  generate a table with all recommended spellings.
+
+You can add attach the recommended spelling to as many declarations as you want. It is recommended
+to attach the recommended spelling to all relevant parsers as well as the declaration the parsers
+refer to (if such a declaration exists). Note that the `inherit_doc` attribute does *not* copy
+recommended spellings, so even though the parser for `∧` uses `@[inherit_doc And]`, we have to
+attach the recommended spelling to both `And` and `«term_∧_»`.
+
+The `syntax`, `macro`, `elab` and `notation` commands accept a `(name := parserName)` option to
+assign a name to the created parser so that you do not have to guess the automatically generated
+name. The `synax`, `macro` and `elab` commands can be hovered to see the name of the parser.
+
+For complex notations which enclose identifiers, the convention is to use example identifiers rather
+than other placeholders. This is an example following the convention:
+```
+recommended_spelling "singleton" for "[a]" in [List.cons, «term[_]»]
+```
+Using `[·]` or `[⋯]` or `[…]` instead of `[a]` would be against the convention. When attaching a
+recommended spelling to a notation whose docstring already has an example, try to reuse the
+identifier names chosen in the docstring for consistency.
+-/
+@[builtin_command_parser] def «recommended_spelling» := leading_parser
+  optional (docComment >> ppLine) >>
+  "recommended_spelling " >> strLit >> " for " >> strLit >> " in " >>
+    "[" >> sepBy1 ident ", " >> "]"
 
 /--
   This is an auxiliary command for generation constructor injectivity theorems for

src/Lean/Parser/Term.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich, Mario Carneiro
 prelude
 import Lean.Parser.Attr
 import Lean.Parser.Level
+import Lean.Parser.Term.Doc
 
 namespace Lean
 namespace Parser

src/Lean/Parser/Term/Doc.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Lean.Parser.Extension
+
+/-! Environment extension to register preferred spellings of notations in identifiers. -/
+
+set_option linter.missingDocs true
+
+namespace Lean.Parser.Term.Doc
+
+/-- Information about how to spell a certain notation for an identifier in declaration names. -/
+structure RecommendedSpelling where
+  /-- The notation in question. -/
+  «notation» : String
+  /-- The recommended spelling of the notation in identifiers. -/
+  recommendedSpelling : String
+  /-- Additional information. -/
+  additionalInformation? : Option String
+
+/--
+Recommended spellings for notations, stored in a way so that the recommended spellings for a given
+declaration are easily accessible.
+-/
+builtin_initialize recommendedSpellingByNameExt
+    : PersistentEnvExtension (Name × Array RecommendedSpelling) (RecommendedSpelling × Array Name)
+        (NameMap (Array RecommendedSpelling)) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun es (rec, xs) => xs.foldl (init := es) fun es x => es.insert x (es.findD x #[] |>.push rec),
+    exportEntriesFn := fun es =>
+      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/-- Recommended spellings for notations, stored in such a way that it is easy to generate a table
+containing every recommended spelling exactly once. -/
+builtin_initialize recommendedSpellingExt
+    : PersistentEnvExtension RecommendedSpelling RecommendedSpelling (Array RecommendedSpelling) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := Array.push,
+    exportEntriesFn := id
+  }
+
+/-- Adds a recommended spelling to the environment. -/
+def addRecommendedSpelling (env : Environment) (rec : RecommendedSpelling) (names : Array Name) : Environment :=
+  let env := recommendedSpellingExt.addEntry env rec
+  recommendedSpellingByNameExt.addEntry env (rec, names)
+
+/-- Returns the recommended spellings associated with the given declaration name. -/
+def getRecommendedSpellingsForName (env : Environment) (declName : Name) :
+    Array RecommendedSpelling := Id.run do
+  let mut spellings := #[]
+  for modArr in recommendedSpellingByNameExt.toEnvExtension.getState env |>.importedEntries do
+    if let some (_, strs) := modArr.binSearch (declName, #[]) (Name.quickLt ·.1 ·.1) then
+      spellings := spellings ++ strs
+  if let some strs := recommendedSpellingByNameExt.getState env |>.find? declName then
+    spellings := spellings ++ strs
+  return spellings
+
+/-- Renders the recommended spellings for the given declaration into a string for appending to
+the docstring. -/
+def getRecommendedSpellingString (env : Environment) (declName : Name) : String := Id.run do
+  let spellings := getRecommendedSpellingsForName env declName
+  if spellings.size == 0 then ""
+  else "\n\nConventions for notations in identifiers:\n\n" ++ String.join (spellings.toList.map bullet) |>.trimRight
+where
+  indentLine (str : String) : String :=
+    (if str.all (·.isWhitespace) then str else "   " ++ str) ++ "\n"
+  bullet (spelling : RecommendedSpelling) : String :=
+    let firstLine := s!" * The recommended spelling of `{spelling.«notation»}` in identifiers is `{spelling.recommendedSpelling}`"
+    let additionalInfoLines := spelling.additionalInformation?.map (·.splitOn "\n")
+    match additionalInfoLines with
+    | none | some [] => firstLine ++ ".\n\n"
+    | some [l] => firstLine ++ s!" ({l.trimRight}).\n\n"
+    | some ls => firstLine ++ ".\n\n" ++ String.join (ls.map indentLine) ++ "\n\n"
+
+end Lean.Parser.Term.Doc

tests/lean/run/recommendedSpelling.lean

@@ -0,0 +1,64 @@
+import Lean
+
+/-!
+Test the `recommended_spelling` command.
+
+TODO: once we use this command in Init, we can test that recommended spellings from imported
+modules are reported correctly.
+-/
+
+/--
+Conjuction
+
+Second line
+-/
+inductive MyAnd (P Q : Prop) : Prop where
+  | intro : P → Q → MyAnd P Q
+
+@[inherit_doc] infixr:35 " ☃ " => MyAnd
+@[inherit_doc] infixr:35 " ☋ " => MyAnd
+
+recommended_spelling "snowmand" for "☃" in [MyAnd, «term_☃_»]
+/-- the preferred notation is `∧`.
+
+more stuff
+
+even more stuff
+
+hello
+
+-/
+recommended_spelling "orbitalAnd" for "☋" in [MyAnd, «term_☋_»]
+/--      Docstring      -/
+recommended_spelling "and" for "something" in [«term_☃_», «term_☋_»]
+
+def findDocString? (n : Lean.Name) : Lean.MetaM (Option String) := do
+  Lean.findDocString? (← Lean.getEnv) n
+
+/--
+info: some
+  "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `☃` in identifiers is `snowmand`.\n\n * The recommended spelling of `☋` in identifiers is `orbitalAnd`.\n\n   the preferred notation is `∧`.\n\n   more stuff\n\n   even more stuff\n\n   hello"
+-/
+#guard_msgs in
+#eval findDocString? `MyAnd
+
+/--
+info: some
+  "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `☃` in identifiers is `snowmand`.\n\n * The recommended spelling of `something` in identifiers is `and` (Docstring)."
+-/
+#guard_msgs in
+#eval findDocString? `«term_☃_»
+
+/--
+info: some
+  "Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `☋` in identifiers is `orbitalAnd`.\n\n   the preferred notation is `∧`.\n\n   more stuff\n\n   even more stuff\n\n   hello\n\n\n\n\n * The recommended spelling of `something` in identifiers is `and` (Docstring)."
+-/
+#guard_msgs in
+#eval findDocString? `«term_☋_»
+
+/-- info: 1 -/
+#guard_msgs in
+#eval do
+  return (← Lean.Elab.Term.Doc.allRecommendedSpellings)
+    |>.map Lean.Parser.Term.Doc.RecommendedSpelling.«notation»
+    |>.count "☋"