\lean{} links silently fall back to Mathlib docs when \dochome is not set

[spitters]

Problem

When a blueprint does not set \dochome{...} in its web.tex, all \lean{MyProject.Foo.bar} declarations generate links to:

https://leanprover-community.github.io/mathlib4_docs/find/#doc/MyProject.Foo.bar

This is because of the hardcoded fallback in blueprint.py line 202:

project_dochome = document.userdata.get('project_dochome',
                                        'https://leanprover-community.github.io/mathlib4_docs')

For any project that is not Mathlib itself, these links 404. There is no warning emitted during the build, so the broken links go unnoticed until a user clicks them.

Expected behaviour

One or more of:

1. Emit a warning during build if \lean{} declarations are used but \dochome is not set, e.g.:

   WARNING: \lean{} declarations found but \dochome not set — Lean links will point to Mathlib docs
   

2. Omit the Lean link entirely when \dochome is not set, rather than generating a broken link to Mathlib's docs. The \leanok checkmark can still render.

3. Use a neutral fallback like # or a relative ./find/#doc/ path instead of hardcoding Mathlib's URL.

Reproduction

1. Create a blueprint for a non-Mathlib project
2. Add \lean{MyProject.SomeDecl} + \leanok to a definition
3. Do not set \dochome{...} in web.tex
4. Build with plastex
5. Click the "Lean" link in the rendered HTML — it goes to leanprover-community.github.io/mathlib4_docs/find/#doc/MyProject.SomeDecl which 404s

Environment

• leanblueprint 0.8.x (installed via pipx)
• plasTeX 3.1
• Python 3.12