Automatically generated tags for headings are not deduplicated

[KBone12]

Summary

When automatically generated tags for headings collide, freshTag should append a suffix to make them unique. Instead, this deduplication does not work, resulting in a "Duplicate tag" error during manual traversal.

In particular, this issue is easy to encounter with non-ASCII headings. Every unsupported character is converted to ___, so completely different headings can still collide if they contain the same number of unsupported characters, such as Japanese characters.

This occurs in Verso v4.29.0 and on the current main branch.

Steps to reproduce

Create the following Lean file in a Verso project:

import VersoManual
open Verso.Genre Manual

def main := manualMain <| Verso.Doc.VersoDoc.toPart <| #doc (Manual) "Test" =>
# Same
First.

# Same
Second.

Then run lake exe.

Expected behavior

Traversal succeeds. The generated tags are unique, for example Test--Same and Test--Same-0.

Actual behavior

lake exe exits with status 1 and reports:

Duplicate tag '_private.VersoManual.Basic.0.Verso.Genre.Manual.Tag.internal "Test--Same"'
An error was encountered!

lake build alone does not expose the problem because it compiles the document without running traversal.

Cause

In src/verso-manual/VersoManual/Basic.lean, freshTag checks whether the String candidate is already present:

verso/src/verso-manual/VersoManual/Basic.lean

Line 420 in f91d46c

if (← get).tags.contains attempt then

Because attempt is a String, the Coe String Tag instance converts it to Tag.provided attempt. However, generated tags are inserted as Tag.internal:

verso/src/verso-manual/VersoManual/Basic.lean

Line 424 in f91d46c

modify fun st => {st with tags := st.tags.insert (Tag.internal tag) id}

The lookup therefore cannot find an existing generated tag. This appears to be a regression introduced by commit e842684. That commit changed tagStr from producing a Tag.internal value to producing a plain String. The insertion was updated to wrap the string in Tag.internal, but the preceding lookup was not.

Suggested fix

Check for the same tag variant that is inserted:

if (← get).tags.contains (Tag.internal attempt) then