feat: Improve role resolution error diagnostics

doc/UsersGuide/Releases.lean

@@ -6,6 +6,7 @@ Author: Emilio J. Gallego Arias
 
 import VersoManual
 
+import UsersGuide.Releases.«v4_29_0»
 import UsersGuide.Releases.«v4_28_0»
 
 open Verso Genre Manual
@@ -26,4 +27,5 @@ Verso versioning follows Lean's.
 This means that we release a new version for each Lean release, usually once per month.
 In particular, note that Verso doesn't follow the [semantic versioning model](https://semver.org/).
 
+{include 0 UsersGuide.Releases.«v4_29_0»}
 {include 0 UsersGuide.Releases.«v4_28_0»}

doc/UsersGuide/Releases/v4_28_0.lean

@@ -11,7 +11,7 @@ open Verso.Genre
 -- To allow ```` below
 set_option linter.verso.markup.codeBlock false
 
-#doc (Manual) "Verso 4.28.0 (unreleased)" =>
+#doc (Manual) "Verso 4.28.0" =>
 %%%
 tag := "release-v4.28.0"
 file := "v4.28.0"

doc/UsersGuide/Releases/v4_29_0.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Emilio J. Gallego Arias
+-/
+
+import VersoManual
+
+open Verso.Genre
+
+#doc (Manual) "Verso 4.29.0" =>
+%%%
+tag := "release-v4.29.0"
+file := "v4.29.0"
+%%%
+
+* Improve role resolution diagnostics with suggestions and actionable registration errors (@ejgallego, #763)
+* Register legacy inline APIs as roles for compatibility (`today`, `date`, `sectionRef`, `index`, `see`, `seeAlso`) (@ejgallego, #763)

src/tests/Tests.lean

@@ -23,6 +23,7 @@ import Tests.ParserRegression
 import Tests.Paths
 import Tests.PorterStemmer
 import Tests.Refs
+import Tests.RoleResolution
 import Tests.Serialization
 import Tests.TeX
 import Tests.TexUnit

src/tests/Tests/RoleResolution.lean

@@ -0,0 +1,201 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Emilio J. Gallego Arias
+-/
+import Verso
+import VersoManual
+import VersoBlog
+
+namespace Verso.RoleResolutionTest
+set_option guard_msgs.diff true
+
+open Lean
+
+/-
+Role resolution has four relevant outcomes:
+1. role function exists, has type `RoleExpander`, and is registered - good.
+2. role function exists, has a role type, but is not registered - bad.
+3. role function exists, but has the wrong type - bad.
+4. role function does not exist - unresolved role name.
+-/
+
+@[role_expander registered]
+def registered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "registered-role")]
+
+#docs (.none) roleCase1 "Case 1" :=
+:::::::
+{registered}[]
+:::::::
+
+/-- info: #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "registered-role"]] -/
+#guard_msgs in
+#eval roleCase1.toPart.content
+
+def unregistered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "unregistered-role")]
+
+/--
+error: Role function `unregistered` was found but not registered as a role. Register it with `@[role]` or `@[role_expander ...]`.
+-/
+#guard_msgs in
+#docs (.none) roleCase2 "Case 2" :=
+:::::::
+{unregistered}[]
+:::::::
+
+def wrongType : Nat := 7
+
+/--
+error: Function `wrongType` was found but likely not a role.
+-/
+#guard_msgs in
+#docs (.none) roleCase3 "Case 3" :=
+:::::::
+{wrongType}[]
+:::::::
+
+/--
+error: No registered role `registred`.
+
+Hint: Did you mean role `registered`?
+  registe̲red
+-/
+#guard_msgs in
+#docs (.none) roleCase4 "Case 4" :=
+:::::::
+{registred}[]
+:::::::
+
+/--
+error: No registered role `nothereatallzzzz`.
+
+Hint: Closest registered roles:
+  • n̵o̵t̵h̵e̵r̵e̵a̵t̵a̵l̵l̵z̵z̵z̵z̵c̲i̲t̲e̲h̲e̲r̲e̲
+  • n̵o̵t̵h̵e̵r̵e̵a̵t̵a̵l̵l̵z̵z̵z̵z̵a̲n̲c̲h̲o̲r̲N̲a̲m̲e̲
+  • n̵o̵t̵h̵e̵r̵e̵a̵t̵a̵l̵l̵z̵z̵z̵z̵a̲n̲c̲h̲o̲r̲W̲a̲r̲n̲i̲n̲g̲
+  • n̵o̵t̵h̵e̵r̵e̵a̵t̵a̵l̵l̵z̵z̵z̵z̵c̲i̲t̲e̲t̲
+  • n̵o̵t̵h̵e̵r̵e̵a̵t̵a̵l̵l̵z̵z̵z̵z̵h̲t̲m̲l̲S̲p̲a̲n̲
+-/
+#guard_msgs in
+#docs (.none) roleCase5 "Case 5" :=
+:::::::
+{nothereatallzzzz}[]
+:::::::
+
+namespace ManualCases
+open Genre Manual
+
+@[role_expander manualRegistered]
+def manualRegistered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "manual-registered-role")]
+
+#docs (Manual) roleCase1 "Manual Case 1" :=
+:::::::
+{manualRegistered}[]
+:::::::
+
+def manualUnregistered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "manual-unregistered-role")]
+
+/--
+error: Role function `manualUnregistered` was found but not registered as a role. Register it with `@[role]` or `@[role_expander ...]`.
+-/
+#guard_msgs in
+#docs (Manual) roleCase2 "Manual Case 2" :=
+:::::::
+{manualUnregistered}[]
+:::::::
+
+/--
+error: No registered role `manualRegistred`.
+
+Hint: Did you mean role `manualRegistered`?
+  manualRegiste̲red
+-/
+#guard_msgs in
+#docs (Manual) roleCase3 "Manual Case 3" :=
+:::::::
+{manualRegistred}[]
+:::::::
+
+/--
+error: No registered role `manualNowhereNearZzzzz`.
+
+Hint: Closest registered roles:
+  • m̵a̵n̵u̵a̵l̵N̵o̵w̵h̵e̵r̵e̵N̵e̵a̵r̵Z̵z̵z̵z̵z̵m̲a̲n̲u̲a̲l̲R̲e̲g̲i̲s̲t̲e̲r̲e̲d̲
+  • m̵a̵n̵u̵a̵l̵N̵o̵w̵h̵e̵r̵e̵N̵e̵a̵r̵Z̵z̵z̵z̵z̵a̲n̲c̲h̲o̲r̲N̲a̲m̲e̲
+  • m̵a̵n̵u̵a̵l̵N̵o̵w̵h̵e̵r̵e̵N̵e̵a̵r̵Z̵z̵z̵z̵z̵a̲n̲c̲h̲o̲r̲T̲e̲r̲m̲
+  • m̵a̵n̵u̵a̵l̵N̵o̵w̵h̵e̵r̵e̵N̵e̵a̵r̵Z̵z̵z̵z̵z̵a̲n̲c̲h̲o̲r̲W̲a̲r̲n̲i̲n̲g̲
+  • m̵a̵n̵u̵a̵l̵N̵o̵w̵h̵e̵r̵e̵N̵e̵a̵r̵Z̵z̵z̵z̵z̵m̲o̲d̲u̲l̲e̲N̲a̲m̲e̲
+-/
+#guard_msgs in
+#docs (Manual) roleCase4 "Manual Case 4" :=
+:::::::
+{manualNowhereNearZzzzz}[]
+:::::::
+
+end ManualCases
+
+namespace BlogCases
+open Genre Blog
+
+@[role_expander blogRegistered]
+def blogRegistered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "blog-registered-role")]
+
+#docs (Blog.Post) roleCase1 "Blog Case 1" :=
+:::::::
+{blogRegistered}[]
+:::::::
+
+def blogUnregistered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "blog-unregistered-role")]
+
+/--
+error: Role function `blogUnregistered` was found but not registered as a role. Register it with `@[role]` or `@[role_expander ...]`.
+-/
+#guard_msgs in
+#docs (Blog.Post) roleCase2 "Blog Case 2" :=
+:::::::
+{blogUnregistered}[]
+:::::::
+
+/--
+error: No registered role `blogRegistred`.
+
+Hint: Did you mean role `blogRegistered`?
+  blogRegiste̲red
+-/
+#guard_msgs in
+#docs (Blog.Post) roleCase3 "Blog Case 3" :=
+:::::::
+{blogRegistred}[]
+:::::::
+
+/--
+error: No registered role `blogNoCloseMatchZzzzz`.
+
+Hint: Closest registered roles:
+  • b̵l̵o̵g̵N̵o̵C̵l̵o̵s̵e̵M̵a̵t̵c̵h̵Z̵z̵z̵z̵z̵b̲l̲o̲g̲R̲e̲g̲i̲s̲t̲e̲r̲e̲d̲
+  • b̵l̵o̵g̵N̵o̵C̵l̵o̵s̵e̵M̵a̵t̵c̵h̵Z̵z̵z̵z̵z̵l̲e̲a̲n̲C̲o̲m̲m̲a̲n̲d̲
+  • b̵l̵o̵g̵N̵o̵C̵l̵o̵s̵e̵M̵a̵t̵c̵h̵Z̵z̵z̵z̵z̵m̲o̲d̲u̲l̲e̲N̲a̲m̲e̲
+  • b̵l̵o̵g̵N̵o̵C̵l̵o̵s̵e̵M̵a̵t̵c̵h̵Z̵z̵z̵z̵z̵m̲o̲d̲u̲l̲e̲O̲u̲t̲
+  • b̵l̵o̵g̵N̵o̵C̵l̵o̵s̵e̵M̵a̵t̵c̵h̵Z̵z̵z̵z̵z̵m̲o̲d̲u̲l̲e̲W̲a̲r̲n̲i̲n̲g̲
+-/
+#guard_msgs in
+#docs (Blog.Post) roleCase4 "Blog Case 4" :=
+:::::::
+{blogNoCloseMatchZzzzz}[]
+:::::::
+
+end BlogCases
+
+end Verso.RoleResolutionTest

src/verso-manual/VersoManual/Index.lean

@@ -10,6 +10,8 @@ import Std.Data.HashMap
 import Std.Data.HashSet
 
 import Verso.Doc.Elab
+public import Verso.Doc.Elab.Monad
+meta import Verso.Doc.Elab.Monad
 public import VersoManual.Basic
 import VersoManual.Html.SoftHyphenate
 import MultiVerso
@@ -19,7 +21,8 @@ public import Verso.Doc
 open Verso Genre Manual
 open Verso.Multi
 open Verso.Doc.Elab
-open Lean (ToJson FromJson)
+open Verso.ArgParse
+open Lean (ToJson FromJson quote)
 open Std (HashMap HashSet)
 
 namespace Verso.Genre.Manual.Index
@@ -184,6 +187,42 @@ def seeAlso (args : Array (Doc.Inline Manual)) (target : String) (subterm : Opti
   let data : Index.See := {source := .concat args, target := .text target, subTarget := subterm.map .text, also := true, index}
   Doc.Inline.other {Inline.see with data := ToJson.toJson data} #[]
 
+structure IndexArgs where
+  subterm : Option String
+  index : Option String
+
+structure SeeArgs where
+  target : String
+  subterm : Option String
+  index : Option String
+
+instance : FromArgs IndexArgs DocElabM where
+  fromArgs := IndexArgs.mk <$> .named `subterm .string true <*> .named `index .string true
+
+instance : FromArgs SeeArgs DocElabM where
+  fromArgs := SeeArgs.mk <$>
+    .positional `target .string <*>
+    .named `subterm .string true <*>
+    .named `index .string true
+
+@[role index]
+def indexRole : RoleExpanderOf IndexArgs
+  | {subterm, index}, args => do
+    let args ← args.mapM elabInline
+    ``(index #[$args,*] $(quote subterm) $(quote index))
+
+@[role see]
+def seeRole : RoleExpanderOf SeeArgs
+  | {target, subterm, index}, args => do
+    let args ← args.mapM elabInline
+    ``(see #[$args,*] $(quote target) $(quote subterm) $(quote index))
+
+@[role seeAlso]
+def seeAlsoRole : RoleExpanderOf SeeArgs
+  | {target, subterm, index}, args => do
+    let args ← args.mapM elabInline
+    ``(seeAlso #[$args,*] $(quote target) $(quote subterm) $(quote index))
+
 @[inline_extension see]
 def see.descr : InlineDescr where
   traverse _id data _contents := do