feat: interproject linking — document a project without its dependencies

[kim-em]

By default doc-gen4 documents a library together with its entire import closure, so a project built on top of a large dependency such as Mathlib regenerates the dependency's documentation too — often several GB, and close to the GitHub Pages ~1 GB artifact limit. This PR adds an opt-in mode that generates pages for only the project's own modules and links references to its dependencies out to their already-published documentation.

Three environment variables control it (in the spirit of the existing DOCGEN_SRC):

• DOCGEN_LOCAL_MODULE_ROOTS — a comma-separated list of the top-level module namespaces that belong to your project (e.g. MyProject). A module whose root is not listed is treated as external, and its pages are not generated.
• DOCGEN_DEPS_DOCS_URL — an optional fallback base URL for external dependency documentation, e.g. https://leanprover-community.github.io/mathlib4_docs.
• DOCGEN_DEPS_DOCS_URLS — optional comma-separated per-root overrides of the form Root=URL, e.g. Mathlib=https://.../mathlib4_docs,Batteries=https://.../batteries_docs. List multiple roots separately when one dependency owns multiple top-level namespaces.

For each external module, a per-root entry takes precedence over the fallback URL. A reference to an external declaration links to the selected site's /find resolver (…/find/?pattern=<decl>#doc), which looks the declaration up by name and so tolerates the dependency's docs being built from a slightly different revision than the one being linked against; module-level links point directly at the corresponding page. Every external module root must have either a per-root entry or a fallback, and doc-gen4 reports a configuration error rather than producing broken local links when a mapping is missing.

The excluded modules stay in the linking context so cross-references still resolve. When DOCGEN_LOCAL_MODULE_ROOTS is unset, the behaviour is unchanged.

The change is localized to the two link builders (moduleNameToLink / declNameToLink), dependency-URL selection and validation, and a render-set filter in fromDb, with the configuration read in getSimpleBaseContext. The README documents the variables. The multi-library regression test now also covers distinct dependency sites, fallback links, trailing-slash normalization, omitted dependency pages, and incomplete-configuration errors.

Validated end-to-end against Tau Ceti, a ~580-module Mathlib-downstream library: with DOCGEN_LOCAL_MODULE_ROOTS=TauCeti, only the 581 TauCeti pages are generated (no Mathlib/Init/Std/… trees), references to Mathlib declarations link to mathlib4_docs, and there are no broken local links — cutting the output from ~963 MB to tens of MB.

[cursor]

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

[Vtec234]

Would this be hard to generalize to per-dependency URLs?

[kim-em]

Would this be hard to generalize to per-dependency URLs?

Done.

[BorisTheBrave]

A reference to an external declaration links to the selected site's /find resolver

I note that this adds a bit of latency to actually navigating the docs. An alternative is to link to the exact url. header-data.bmp contains the necessary indexing for this.

[kim-em]

A reference to an external declaration links to the selected site's /find resolver

I note that this adds a bit of latency to actually navigating the docs. An alternative is to link to the exact url. header-data.bmp contains the necessary indexing for this.

Yes, but header-data.bmp won't work reliably if there is any version skew between the docs sites, while /find copes pretty well. Happy if someone wants to investigate this as a follow-up, but I propose that it is out of scope for this PR.