Skip to content

fix: deduplicate machine-assigned tags - #991

Open
casavaca wants to merge 2 commits into
leanprover:mainfrom
casavaca:fix-897
Open

casavaca wants to merge 2 commits into
leanprover:mainfrom
casavaca:fix-897

Conversation

@casavaca

Copy link
Copy Markdown

Fixes #897.

Every section in a manual carries a tag: it becomes the section's HTML id and the target that cross-references resolve to, and Verso generates one from the title when the author has not chosen it. Two sections whose titles agree therefore need two different generated tags. They do not get them, and the manual fails to build instead:

# Same
First.

# Same
Second.
Duplicate tag '_private.VersoManual.Basic.0.Verso.Genre.Manual.Tag.internal "Test--Same"'

The generator, freshTag, is meant to prevent exactly this: it tries Same, then Same-0, until it finds a name that TraverseState.tags does not already hold. That search never finds anything. It looks the candidate up as a String, which Coe String Tag turns into Tag.provided, while the name it goes on to store is a Tag.internal, so it never sees the names it assigned itself and the numeric suffix is never appended.

The search was right when the suffix was introduced in e223cfc, where tagStr returned a Tag. It stopped working in e842684, which changed freshTag to return a String: the insertion was updated to Tag.internal tag, the lookup kept its old shape, and the coercion kept it compiling. Since then any two headings that sluggify to the same string collide. Headings in a non-Latin script collide readily, because every unsupported character becomes ___: two Japanese headings of the same length always produce the same slug.

This changes the lookup to use the constructor that is stored, and adds two tests to VersoTests.Tags — two elements with the same hint, and two different Japanese headings. On the current main they produce Same/Same and ______/______; with this change they produce Same/Same-0 and ______/______-0, and the example above builds, giving the two sections Test--Same and Test--Same-0. lake test passes (649 tests).

This picks up #937, which proposed the same one-line change and was closed for lack of response — the failing test and the fuller description asked for there are what this adds.


Drafted with Claude Opus 5

casavaca and others added 2 commits September 22, 2026 00:22
freshTag inserts Tag.internal but looked up the plain String, which the
Coe instance turns into Tag.provided, so the check never matched a tag it
had assigned and the numeric suffix was never appended.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017wS1phtpAFaUWUPrQMf1ip
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017wS1phtpAFaUWUPrQMf1ip

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Automatically generated tags for headings are not deduplicated

1 participant