fix: section tag overlap in Manual

doc/UsersGuide/Releases/Assemble.lean

@@ -97,13 +97,13 @@ public def bucket
       if hasSection entry then
         -- The entry's own metadata is kept; only its permalink comes from the release note.
         some { entry with
-          metadata := some { entry.metadata.getD {} with tag := some (metadata.tag : Manual.Tag) },
+          metadata := some { entry.metadata.getD {} with tag := some metadata.tag },
           content := entry.content.extract 1 }
       else none
     some <| Part.mk
       #[Inline.text title]
       title
-      (some { tag := some (tag : Manual.Tag) })
+      (some { tag := some tag })
       #[ Doc.Block.other
            (Block.release (toString version) { title, version })
            #[],
@@ -252,7 +252,7 @@ private def summaryTags (part : Part Manual) : Array (Option String) :=
   (bucket ⟨4, 33, 0⟩ false #[(testMetadata, entry)]).any fun part =>
     part.subParts.all fun s =>
       (s.metadata.map (·.draft)).getD false &&
-      (s.metadata.bind (·.tag)) == some ("entry" : Manual.Tag)
+      (s.metadata.bind (·.tag)) == some "entry"
 
 end Tests
 

src/multi-verso/MultiVerso.lean

@@ -285,6 +285,12 @@ public instance : GetElem? RefDomain String (Array RefObject) fun dom name => na
   getElem dom name ok := dom.contents[name]'ok
   getElem? dom name := dom.contents[name]?
 
+/--
+Returns the canonical names used in {name}`domain`, in sorted order.
+-/
+public def RefDomain.canonicalNames (domain : RefDomain) : Array String :=
+  domain.contents.keysArray.qsortOrd
+
 private def RefDomain.structEq (x y : RefDomain) :=
   let ⟨t1, d1, c1⟩ := x
   let ⟨t2, d2, c2⟩ := y

src/tests/Tests/Tags.lean

@@ -5,6 +5,7 @@ Author: David Thrane Christiansen
 -/
 module
 import VersoManual
+meta import VersoManual
 
 set_option doc.verso true
 
@@ -94,4 +95,171 @@ info: (false, some "my-tag", none, true)
     pure (tag, machine, chosen)
   pure (tag.isSome, htmlId state machine, htmlId state chosen, failed)
 
+/-
+A name containing a space gives the element its slug as an HTML id.
+-/
+/-- info: (true, some "some-tag", false) -/
+#guard_msgs in
+#eval show IO _ from do
+  let ((tag, id), state, failed) ← run do
+    let id ← freshId
+    let tag ← providedTag id #["page"] "some tag"
+    pure (tag, id)
+  pure (tag.isSome, htmlId state id, failed)
+
+/-
+Names that share a slug are duplicates, because both need the same HTML id. The error names the
+slug when it differs from the name as written.
+-/
+/--
+info: Duplicate tag 'some tag': its slug 'some-tag' is already in use
+An error was encountered!
+---
+info: (false, some "some-tag", none, true)
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let ((tag, first, second), state, failed) ← run do
+    let first ← freshId
+    let second ← freshId
+    let _ ← providedTag first #["page"] "some-tag"
+    let tag ← providedTag second #["page"] "some tag"
+    pure (tag, first, second)
+  pure (tag.isSome, htmlId state first, htmlId state second, failed)
+
+/--
+info: Duplicate tag 'some-tag'
+An error was encountered!
+---
+info: (false, some "some-tag", none, true)
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let ((tag, first, second), state, failed) ← run do
+    let first ← freshId
+    let second ← freshId
+    let _ ← providedTag first #["page"] "some tag"
+    let tag ← providedTag second #["page"] "some-tag"
+    pure (tag, first, second)
+  pure (tag.isSome, htmlId state first, htmlId state second, failed)
+
+/-! Tests for assigning tags to parts with {name}`tagPart`. -/
+
+/--
+Runs a traversal action with no extensions against an empty state and context, returning its
+result, the resulting state, and whether any errors were logged.
+-/
+private def runTraverse (act : TraverseM α) : IO (α × TraverseState × Bool) := do
+  let logger ← Logger.new
+  let (result, state) ←
+    (TraverseM.run (ExtensionImpls.fromLists [] []) {} (TraverseState.initialize {}) act).run logger
+  let failed ← logger.failIfErrors
+  return (result, state, failed != 0)
+
+/-
+Traversal registers a part in the section domain under its name exactly as written, resolvable by
+{name}`TraverseState.resolveDomainObject`, while its HTML id is the slug. The name in the part's
+metadata is untouched.
+-/
+/-- info: (some "some tag", some "some-tag", true, some "some-tag", false) -/
+#guard_msgs in
+#eval show IO _ from do
+  let ((name, id), state, failed) ← runTraverse do
+    let id ← freshId
+    let md : PartMetadata := { tag := some "some tag", id := some id }
+    let part : Doc.Part Manual := .mk #[Doc.Inline.text "Some Tag"] "Some Tag" (some md) #[] #[]
+    -- Two rounds, as the traversal driver would run them
+    let t ← tagPart part md (·.id) (·.xrefTag) (·.tag) savePartXref
+    let md := { md with xrefTag := some t }
+    let _ ← tagPart part md (·.id) (·.xrefTag) (·.tag) savePartXref
+    pure (md.tag, id)
+  let resolved :=
+    match state.resolveDomainObject sectionDomain "some tag" with
+    | .ok link => some link.htmlId.toString
+    | .error _ => none
+  pure (name, htmlId state id,
+    (state.getDomainObject? sectionDomain "some-tag").isNone, resolved, failed)
+
+/-
+Two parts that claim the same name produce a single, readable duplicate error.
+-/
+/--
+info: Duplicate tag 'some tag': its slug 'some-tag' is already in use
+An error was encountered!
+---
+info: true
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let (_, _, failed) ← runTraverse do
+    let first ← freshId
+    let md1 : PartMetadata := { tag := some "some tag", id := some first }
+    let part1 : Doc.Part Manual := .mk #[Doc.Inline.text "A"] "A" (some md1) #[] #[]
+    let _ ← tagPart part1 md1 (·.id) (·.xrefTag) (·.tag) savePartXref
+    let second ← freshId
+    let md2 : PartMetadata := { tag := some "some tag", id := some second }
+    let part2 : Doc.Part Manual := .mk #[Doc.Inline.text "B"] "B" (some md2) #[] #[]
+    let _ ← tagPart part2 md2 (·.id) (·.xrefTag) (·.tag) savePartXref
+  pure failed
+
+/-! Tests for suggesting alternatives to unresolved cross-references. -/
+
+/-- info: "" -/
+#guard_msgs in
+#eval suggestRefTargets #["alpha", "beta"] "zzzzzzzzzzzz"
+
+/-- info: "\nDid you mean one of these?\n * 'some tag'\n * 'some-tag'" -/
+#guard_msgs in
+#eval suggestRefTargets #["some-tag", "some tag", "other"] "some tg"
+
+/-
+At most five targets are suggested.
+-/
+/-- info: "\nDid you mean one of these?\n * 'tag1'\n * 'tag2'\n * 'tag3'\n * 'tag4'\n * 'tag5'" -/
+#guard_msgs in
+#eval suggestRefTargets #["tag6", "tag5", "tag4", "tag3", "tag2", "tag1"] "tag"
+
+/-! Tests for the unresolved-reference error message with {name}`unresolvedRefMessage`. -/
+
+/-
+A name that is absent from the domain gets suggestions of nearby names.
+-/
+/--
+info: "No destination found for tag 'some tg' in Verso.Genre.Manual.section\nDid you mean one of these?\n * 'some tag'"
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let (_, state, _) ← runTraverse do
+    let id ← freshId
+    modify (·.saveDomainObject sectionDomain "some tag" id)
+  pure (unresolvedRefMessage state none "some tg")
+
+/-
+A name that is present in the domain failed to resolve for another reason, which the message
+states instead of suggesting the name to itself.
+-/
+/--
+info: "Ref some tag in Verso.Genre.Manual.section has 2 targets, can only link to one"
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let (_, state, _) ← runTraverse do
+    let first ← freshId
+    let second ← freshId
+    modify (·.saveDomainObject sectionDomain "some tag" first
+      |>.saveDomainObject sectionDomain "some tag" second)
+  pure (unresolvedRefMessage state none "some tag")
+
+/-
+A name whose domain object has no targets at all, which happens when only data was saved for it.
+-/
+/--
+info: "No link target registered for some tag in Verso.Genre.Manual.section"
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let (_, state, _) ← runTraverse do
+    modify (·.saveDomainObjectData sectionDomain "some tag" .null)
+  pure (unresolvedRefMessage state none "some tag")
+
 end Verso.Tests.Tags

src/verso-manual/VersoManual.lean

@@ -17,6 +17,7 @@ public import Verso.Output.Html.ElasticLunr
 public import Verso.Doc.Lsp
 public import Verso.Doc.Elab
 public import Verso.FS
+public import Verso.SmartSuggestions
 
 public import VersoSearch
 public import VersoSearch.DomainSearch
@@ -84,6 +85,34 @@ deriving BEq, ToJson, FromJson
 defmethod Part.htmlToc (part : Part Manual) : Bool :=
   part.metadata.map (·.htmlToc) |>.getD true
 
+/--
+Renders the names among {name}`candidates` that are close to {name}`name`, as a suffix for the
+error message about an unresolved cross-reference. Returns the empty string when no candidate is
+close enough.
+-/
+def suggestRefTargets (candidates : Array String) (name : String) : String :=
+  let suggestions := smartSuggestions candidates name (count := 5)
+  if suggestions.isEmpty then ""
+  else suggestions.foldl (init := "\nDid you mean one of these?") (· ++ s!"\n * '{·}'")
+
+/--
+The error message for a cross-reference to {name}`name` that traversal could not resolve.
+
+When the name is absent from the domain, nearby names from the domain's contents in {name}`st`
+are suggested. When the name is present, resolution failed for another reason, such as the name
+having multiple targets. The resulting message preserves this.
+-/
+def unresolvedRefMessage (st : TraverseState) (domain : Option Name) (name : String) : String :=
+  let domain := domain.getD sectionDomain
+  if (st.getDomainObject? domain name).isSome then
+    match st.resolveDomainObject domain name with
+    | .error e => e
+    | .ok _ =>
+      s!"'{name}' in {domain} was not resolved during traversal; the document may need more traversal passes"
+  else
+    let candidates := st.domains[domain]?.map (·.canonicalNames) |>.getD #[]
+    s!"No destination found for tag '{name}' in {domain}{suggestRefTargets candidates name}"
+
 inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (remote : Option String) (resolvedDestination : Option Link := none) where
   data := ToJson.toJson (RefInfo.mk canonicalName domain remote resolvedDestination)
   traverse := fun _ info content => do
@@ -108,7 +137,7 @@ inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (rem
       | .error e =>
         reportError e; content.mapM go
       | .ok { canonicalName := name, domain, remote := none, resolvedDestination := none } =>
-        reportError ("No destination found for tag '" ++ name ++ "' in " ++ toString domain); content.mapM go
+        reportError (unresolvedRefMessage (← Doc.TeX.state) domain name); content.mapM go
       | .ok { canonicalName := name, domain, remote := some remote, resolvedDestination := none } =>
         reportError ("No destination found for remote '" ++ remote ++ "' tag '" ++ name ++ "' in " ++ toString domain); content.mapM go
       | .ok {resolvedDestination := some dest, remote, ..} =>
@@ -127,7 +156,7 @@ inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (rem
       | .error e =>
         reportError e; content.mapM go
       | .ok { canonicalName := name, domain, remote := none, resolvedDestination := none } =>
-        reportError ("No destination found for tag '" ++ name ++ "' in " ++ toString domain); content.mapM go
+        reportError (unresolvedRefMessage (← Doc.Html.HtmlT.state) domain name); content.mapM go
       | .ok { canonicalName := name, domain, remote := some remote, resolvedDestination := _ } =>
         let domain := domain |>.getD sectionDomain
         let remoteData ← readThe AllRemotes
@@ -141,7 +170,7 @@ inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (rem
               else
                 let dests := objs.map (s!" * {·.link.link}") |>.toList |> "\n".intercalate
                 reportError s!"Remote '{remote}' domain '{domain}' contains multiple destinations for '{name}':\n{dests}"
-            else reportError s!"Remote '{remote}' contains domain '{domain}, but it not item '{name}'"
+            else reportError s!"Remote '{remote}' contains domain '{domain}', but not item '{name}'{suggestRefTargets dom.canonicalNames name}"
           else reportError s!"Remote '{remote}' does not contain domain '{domain}' (looking up '{name}')"
         else reportError s!"Remote '{remote}' not found for tag '{name}' in domain '{domain}'"
         -- If any error was logged, just don't emit a link