feat: add mathlib3 deprecation banner and point canonical URLs at mathlib4#180
feat: add mathlib3 deprecation banner and point canonical URLs at mathlib4#180
Conversation
…hlib4 Adds a fixed red banner across the top of every page declaring that mathlib3 is deprecated, with a link to the mathlib4 docs. Sets the canonical URL on every page to the mathlib4 docs root, so search engines consolidate ranking onto the maintained library. The previous canonical_roots mapping was self-referential (mathlib3 -> mathlib3), which is a no-op as far as SEO goes. Discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/De-emphasizing.20mathlib3.20docs.20in.20search.20results.20via.20canonical Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
#deploy |
1 similar comment
|
#deploy |
|
This PR has been successfully deployed! You can find it at http://leanprover-community.github.io/mathlib_docs_demo in around 10 minutes, or watch the deployment progress by going to http://github.com/leanprover-community/mathlib_docs_demo |
Here's what a typical page looks like. I think `display: flex` is causing there to be missing spaces between some of the text elements and the links. Should be easy to fix.
|
…l writes - banner: drop flex, use line-height for vertical centering, white link on red, mobile media query (leanprover-community#180 review feedback) - canonical: per-page mapping via port_status.yaml + resolved sidecar; previously every page pointed at mathlib4_docs root which is the many-to-one canonical anti-pattern Google explicitly rejects - noindex: emit <meta name='robots' content='noindex,follow'> for entries the resolver tagged as deleted/unknown/unverified_404 so we don't try to canonicalise where there's no successor - print_docs.py: new -j/--jobs flag parallelising write_redirects via multiprocessing.Pool with an initializer to share file_map without per-task pickling; safe with default 1, ~3-4× speedup at -j 4 on Apple container's virtio-fs (8+ ENFILEs)
FordUniver
left a comment
FordUniver
left a comment
There was a problem hiding this comment.
I think this scales cleanly across screen sizes
| # TODO: allow extending this for third-party projects | ||
| canonical_roots = { | ||
| 'core': 'https://leanprover-community.github.io/mathlib_docs', | ||
| 'mathlib': 'https://leanprover-community.github.io/mathlib_docs', | ||
| 'mathlib-archive': 'https://leanprover-community.github.io/mathlib_docs', | ||
| 'mathlib-counterexamples': 'https://leanprover-community.github.io/mathlib_docs', | ||
| } | ||
| # mathlib3 is deprecated. Every page declares the mathlib4 docs root as | ||
| # its canonical URL, to redirect search-engine ranking onto the | ||
| # maintained library. | ||
| MATHLIB4_DOCS_ROOT = 'https://leanprover-community.github.io/mathlib4_docs/' | ||
|
|
||
| def get_canonical_url(path, project='mathlib'): | ||
| try: | ||
| root = canonical_roots[project] | ||
| except KeyError: | ||
| return None | ||
| return root + '/' + path | ||
| return MATHLIB4_DOCS_ROOT |
There was a problem hiding this comment.
I think blanket pointing to the root of mathlib4 docs is exactly the thing that will lead search engines to ignore a canonical link. There needs to be some reasonable overlap in content, so the map is needed if we do the canonical link approach instead of just a de-index.
There was a problem hiding this comment.
I think the best approach is to commit a one-off snapshot a map that covers 90%+ of the mathlib3 docs with newer (current) mathlib4 references. The code could then just check if a replacement is known:
import yaml as _yaml
MATHLIB4_DOCS = 'https://leanprover-community.github.io/mathlib4_docs/'
try:
with open(os.path.join(os.path.dirname(__file__), 'mathlib4_canonical_map.yaml')) as _f:
_mathlib4_map = _yaml.safe_load(_f) or {}
except FileNotFoundError:
_mathlib4_map = {}
def get_canonical_url(path, project='mathlib'):
if project == 'mathlib' and path.endswith('.html'):
target = _mathlib4_map.get(path[:-5].replace('/', '.'))
if target:
return MATHLIB4_DOCS + target + '.html'
try:
root = canonical_roots[project]
except KeyError:
return None
return root + '/' + path
There was a problem hiding this comment.
I like this idea. Do you mind making a PR into this branch?
There was a problem hiding this comment.
I like this idea. Do you mind making a PR into this branch?
Done, see #181
Co-authored-by: FordUniver <61389961+FordUniver@users.noreply.github.com>
|
#deploy |
|
This PR has been successfully deployed! You can find it at http://leanprover-community.github.io/mathlib_docs_demo in around 10 minutes, or watch the deployment progress by going to http://github.com/leanprover-community/mathlib_docs_demo |
3 participants
This PR adds a fixed red banner across the top of every mathlib3 doc page, declaring that mathlib3 is deprecated and linking to the mathlib4 docs, and sets the
<link rel="canonical">on every page to the mathlib4 docs root. The previouscanonical_rootsmapping was self-referential (mathlib3 → mathlib3), which is a no-op for SEO.The motivation is that the deprecated mathlib3 docs consistently outrank the mathlib4 docs in Google and DuckDuckGo, which is confusing for newcomers. A blanket canonical pointer to the mathlib4 docs root is a deliberately simple choice — a per-page mapping was considered (snake_case → CamelCase covers ~67% of files cleanly) but rejected as not worth the complexity given that many files have been split, renamed, or moved.
Discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/De-emphasizing.20mathlib3.20docs.20in.20search.20results.20via.20canonical
🤖 Prepared with Claude Code