Dead lean-manual:// cross-references in core docstrings 404 in the manual

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to "Lean nightly")
  — verified the dead tags are also absent from the latest manual's xref database

Description

Several core docstrings link to manual sections via lean-manual://section/NAME where NAME is not a target in the manual's cross-reference database. At render time these are rewritten to the Verso cross-reference redirector (<root>/find/?domain=Verso.Genre.Manual.section&name=NAME), which returns "Not found" because the tag does not exist.

The links are dead both in editor hovers and on the published manual pages (which use the same docstrings).

Context

I believe these links date from the introduction of the lean-manual:// scheme in #7240.

Related, but distinct from this issue:

• #7872 — RFC to make lean-manual:// links ctrl-clickable in the source buffer.
  • That's about the click-handling in the editor. This issue is about broken targets in the docstring content, which 404 even where the links already work (hovers, manual pages).
• #6906 — info-view hover resolving to the wrong declaration's docs.
  • Adjacent docstring/hover behavior, not the same bug.

Steps to Reproduce

1a. Editor hover: On a 4.31.0 toolchain, hover Quot.lift in Prelude.lean#L520
1b. Manual: Open the manual's Quotients page, which shows the Quot.lift docstring: https://lean-lang.org/doc/reference/4.31.0/The-Type-System/Quotients/#Quot___lift
2. Click the "definitional reduction" link.
3. It navigates to https://lean-lang.org/doc/reference/4.31.0/find/?domain=Verso.Genre.Manual.section&name=type-theory

Expected behavior:

The link resolves to the manual section describing the quotient reduction rule.

Actual behavior:

The redirector reports Not found: name 'type-theory'. No section has the tag type-theory.

Versions

4.31.0
macOS Sequoia Version 15.7.4 (24G517)

Reproduced against the published 4.31.0 manual. The dead tags are also absent from latest.

Additional Information

A scan of src/ for lean-manual:// links found 7 dead instances across 3 distinct tags each absent from both the latest and 4.31.0 cross-reference databases (so this is not version skew). The other 43 lean-manual:// links in src/ resolve correctly.

• section/type-theory — Init/Prelude.lean (Quot.lift), 1 link
• section/do-notation-let-mut — Init/Prelude.lean, 2 links
• section/monad-lifting — Init/Control/{State,StateCps,StateRef,Option}.lean, 4 links

Proposed corrections (existing tags that match):

• do-notation-let-mut → let-mut
• monad-lifting → lifting-monads — matches existing usage in Init/System/IO.lean
• type-theory → quotient-reduction — the §5.1 "Quotient Reduction" subsection that documents the rule.
  • This last one is a judgment call: I'd point it to the specific subsection, but we could also do the broader quotient-model section if preferred.

Happy to send a PR for the fix.

Impact

A fix would correct the nightly manual and the next release, but not 4.31.0.

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Search src/Init/Prelude.lean and src/Init/Control/{State,StateCps,StateRef,Option}.lean for the seven lean-manual:// links. Compare their targets with the latest and 4.31.0 xref databases, then update the dead tags to the proposed existing targets, resolving the type-theory choice with the maintainers. Done means all seven links resolve in the generated manual.