Automatically generated tags for headings are not deduplicated

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:
https://github.com/leanprover/verso/blob/f91d46ca8b63be638b2f4fef2b1011012c540a41/src/verso-manual/VersoManual/Basic.lean#L420

Because attempt is a String, the Coe String Tag instance converts it to Tag.provided attempt. However, generated tags are inserted as Tag.internal:
https://github.com/leanprover/verso/blob/f91d46ca8b63be638b2f4fef2b1011012c540a41/src/verso-manual/VersoManual/Basic.lean#L424

The lookup therefore cannot find an existing generated tag. This appears to be a regression introduced by commit https://github.com/leanprover/verso/commit/e842684798df452fa30c7528e49be21b7a5d682c. 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

Start in src/verso-manual/VersoManual/Basic.lean at freshTag, where the issue identifies the mismatched tag lookup and insertion. Reproduce with the Lean document in the issue and run lake exe, since lake build does not traverse it. Done means colliding generated headings produce unique tags and traversal succeeds without a duplicate-tag error.