Keep the text of a published link that leaves the blueprint

[Deicyde]

Supersedes #299. I did this at the user's request (2026-10-14), after reviewing #299: #299 (comment)

Problem

The site holds only the blueprint. When render cannot send readers to the repository, it keeps source notes in the site:

• no origin remote;
• uncommitted edits;
• a Lean root below the Git top level, which is make check-example's layout;
• a blueprint outside the repository.

Their evidence links to Lean files beside the blueprint, such as [Basic.lean](../../src/CabannesThesis/Basic.lean#L5), were left pointing outside the blueprint. Those are dead links, and MkDocs reports each one as missing (... is not found among documentation files), so mkdocs build --strict fails. #299 describes large blueprints such as Formal-Math's and ATLAS's carrying thousands of these links.

#299 excluded sources/** from MkDocs instead:

• In a verified Pages build, render already leaves source notes out, so the exclusion changed nothing there.
• In every other mode, it turned the published notes' ## Sources links into 404s, which MkDocs 1.6 logs only at INFO.

Change

_rewrite_links now replaces an inline link whose resolved target lies outside the blueprint with its label. For example, the link above becomes Basic.lean. This applies to every published page; articles cannot hold such links anyway, because check and audit refuse a ## Sources link that leaves the blueprint. Links inside the blueprint, URLs, absolute paths and fragment-only links are unchanged. A reference-style definition that leaves the blueprint is left as it was.

Tests

• test_a_published_link_out_of_the_blueprint_keeps_only_its_text (tests/test_render.py): a published source note with links to a Lean file and to a directory outside the blueprint, and a link to an article. The outside links keep only their text; the article link is still rewritten. The test fails if the change is reverted.
• The bundled example's source map now cites the Lean file that holds CabannesThesis.supervision. make check-example (in CI's test job) renders the example in this mode and runs mkdocs build --strict, so it now covers this path end to end. A scratch run of main plus only that line shows the strict build failing on the link; the run is linked in a comment below.

Overlap

Trial merges against #90, #213-#219, #284, #300, #301 and #307 add no conflicts beyond what each already has with main.

This machine is over the agreed load limit for local pytest runs. The new test and its neighbours were called directly in Python, and CI on this PR is the full run.

[Deicyde]

This is the evidence for the end-to-end check in the description. Main with only the new line in the example's source map, and without the render change, fails make check-example:

WARNING -  Doc file 'sources/thesis.md' contains a link '../../src/CabannesThesis/Basic.lean#L20', but the target '../src/CabannesThesis/Basic.lean' is not found among documentation files.
Aborted with 1 warnings in strict mode!

https://github.com/facebookresearch/autoform-bot/actions/runs/38618403157

Posted by PR swarm: PR Swarm Lead