From 8ff5b55ded1366f187cffc54f485b788a6431969 Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Thu, 19 Feb 2026 16:02:26 +0100 Subject: [PATCH 1/4] CI: check for dead links This PR adds a check for dead links to the pull request CI pipeline. The check happens locally: it should not access the internet. --- .github/workflows/build_pr.yml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/.github/workflows/build_pr.yml b/.github/workflows/build_pr.yml index b0972ab01..5ad8c87e2 100644 --- a/.github/workflows/build_pr.yml +++ b/.github/workflows/build_pr.yml @@ -46,3 +46,18 @@ jobs: with: name: site path: build/ + + - name: Check links + id: check-links + uses: lycheeverse/lychee-action@a8c4c7cb88f0c7386610c35eb25108e448569cb0 # v2.7.0 + with: + args: --no-progress --offline --root-dir $PWD'/build' --exclude '/mathlib4_docs' --exclude '/queueboard' --exclude '/blog' './build/**/*.html' + fail: false + + - name: Add comment to PR about link check outcome + id: check-links-comment + uses: marocchino/sticky-pull-request-comment@773744901bac0e8cbb5a0dc842800d45e9b2b405 # v2.9.4 + if: steps.check-links.outputs.exit_code != 0 + with: + header: 'Link check errors' + path: ./lychee/out.md From 261e0d5ce784d842ce7a14b5d8204be90e9f1ea6 Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Sat, 21 Feb 2026 13:35:36 +0100 Subject: [PATCH 2/4] Add write permission to PRs. Co-authored-by: Bryan Gin-ge Chen --- .github/workflows/build_pr.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/build_pr.yml b/.github/workflows/build_pr.yml index 5ad8c87e2..f8fdf0d64 100644 --- a/.github/workflows/build_pr.yml +++ b/.github/workflows/build_pr.yml @@ -12,6 +12,9 @@ concurrency: permissions: contents: write +permissions: + contents: write + pull-requests: write jobs: build: From 6d38b399502cfb4c658da04c5ff81373cec876ee Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Sat, 21 Feb 2026 08:25:09 -0500 Subject: [PATCH 3/4] Remove duplicate permissions entry in build_pr.yml --- .github/workflows/build_pr.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/build_pr.yml b/.github/workflows/build_pr.yml index f8fdf0d64..e0f0e3219 100644 --- a/.github/workflows/build_pr.yml +++ b/.github/workflows/build_pr.yml @@ -10,8 +10,6 @@ concurrency: # and new runs after that will cancel pending runs cancel-in-progress: false -permissions: - contents: write permissions: contents: write pull-requests: write From 7901a763e81b40823474e6c25bca49ae4f568182 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 4 Mar 2026 06:03:01 +0000 Subject: [PATCH 4/4] 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. --- 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 c9c1b878c..e9676f84b 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 db3f581bf..7bf4016f0 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