From 1baad9c95aa8b9be592d38fa153f86f22e2682f8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 4 Mar 2026 06:01:27 +0000 Subject: [PATCH] fix: rewrite all doc-relative links in header HTML, fix glossary link The header HTML from header-data.json contains doc-relative links for all prefixes (Archive/, Init/, Batteries/, etc.), but only ./Mathlib/ links were being rewritten to ./mathlib4_docs/Mathlib/. This caused broken links on 100.html and 1000.html for declarations in Archive/, Init/, and Batteries/. Fix by rewriting all href="./" links to href="./mathlib4_docs/", matching the existing treatment of docs_link on line 417. Also fix a broken relative link in the glossary: simp.html should be extras/simp.html. Co-Authored-By: Claude Opus 4.6 --- make_site.py | 5 +++-- templates/glossary.md | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/make_site.py b/make_site.py index c9c1b878c1..e9676f84b6 100755 --- a/make_site.py +++ b/make_site.py @@ -408,8 +408,9 @@ def download_N_theorems(kind: NTheorems) -> dict: except KeyError: print(f'Error: {thms} entry {id} refers to a nonexistent declaration {decl}') continue - # note: the `header-data.json` data file uses doc-relative links - header = decl_info.header.replace('href="./Mathlib/', 'href="./mathlib4_docs/Mathlib/') + # note: the `header-data.json` data file uses doc-relative links; + # rewrite all of them to point into the mathlib4_docs subdirectory + header = decl_info.header.replace('href="./', 'href="./mathlib4_docs/') doc_decls.append(DocDecl( name=decl, decl_header_html = header, diff --git a/templates/glossary.md b/templates/glossary.md index db3f581bf4..7bf4016f03 100644 --- a/templates/glossary.md +++ b/templates/glossary.md @@ -373,7 +373,7 @@ Good `simp` lemmas guide the `simp` tactic towards reducing complex expressions A convention within [Mathlib](#Mathlib) for expressing propositions with multiple equivalent forms in a single conventional one. -Examples and further detail can be found on [the `simp` page](simp.html#simp-normal-form). +Examples and further detail can be found on [the `simp` page](extras/simp.html#simp-normal-form). ### syntax linter