Skip to content

CI: check for dead links#792

Open
Vierkantor wants to merge 4 commits intolean4from
dead-links-ci
Open

CI: check for dead links#792
Vierkantor wants to merge 4 commits intolean4from
dead-links-ci

Conversation

@Vierkantor
Copy link
Contributor

@Vierkantor Vierkantor commented Feb 19, 2026

This PR adds a check for dead links to the pull request CI pipeline. The check happens locally: it should not access the internet.

@Vierkantor
CI: check for dead links
8ff5b55 
This PR adds a check for dead links to the pull request CI pipeline. The check happens locally: it should not access the internet.
bryangingechen
bryangingechen reviewed Feb 19, 2026
View reviewed changes
Vierkantor and others added 2 commits February 21, 2026 13:35
@Vierkantor @bryangingechen
Add write permission to PRs.
261e0d5 
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
@bryangingechen
Remove duplicate permissions entry in build_pr.yml
6d38b39
@github-actions
Copy link

github-actions bot commented Feb 21, 2026

Summary

Status Count
🔍 Total 6552
✅ Successful 658
⏳ Timeouts 0
🔀 Redirected 0
👻 Excluded 5760
❓ Unknown 0
🚫 Errors 134
⛔ Unsupported 0

Errors per input

Errors in build/100.html

  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/AbelRuffini.html#AbelRuffini.exists_not_solvable_by_rad | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/AreaOfACircle.html#Theorems100.area_disc | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/AreaOfACircle.html#Theorems100.disc | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/AscendingDescendingSequences.html#Theorems100.erdos_szekeres | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/BallotProblem.html#Ballot.ballot_problem | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/BallotProblem.html#Ballot.countedSequence | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/BallotProblem.html#Ballot.staysPositive | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/BirthdayProblem.html#Theorems100.birthday | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/BirthdayProblem.html#Theorems100.birthday_measure | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/BuffonsNeedle.html#BuffonsNeedle.buffon_long | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/BuffonsNeedle.html#BuffonsNeedle.buffon_short | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/BuffonsNeedle.html#BuffonsNeedle.N | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/CubingACube.html#Theorems100.%C2%AB82%C2%BB.cannot_cube_a_cube | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/CubingACube.html#Theorems100.%C2%AB82%C2%BB.Cube | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/CubingACube.html#Theorems100.%C2%AB82%C2%BB.Cube.toSet | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/CubingACube.html#Theorems100.%C2%AB82%C2%BB.Cube.unitCube | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/CubingACube.html#Theorems100.%C2%AB82%C2%BB.Cube.w | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/FriendshipGraphs.html#Theorems100.ExistsPolitician | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/FriendshipGraphs.html#Theorems100.Friendship | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/FriendshipGraphs.html#Theorems100.friendship_theorem | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/HeronsFormula.html#Theorems100.heron | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/InverseTriangleSum.html#Theorems100.inverse_triangle_sum | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/Konigsberg.html#Konigsberg.graph | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/Konigsberg.html#Konigsberg.not_isEulerian | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/Konigsberg.html#Konigsberg.Verts | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/PerfectNumbers.html#Theorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.html#Theorems100.cubic_eq_zero_iff | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.html#Theorems100.quartic_eq_zero_iff | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.html#Theorems100.Real.tendsto_sum_one_div_prime_atTop | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Batteries/Data/List/Basic.html#List.prod | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/foundational_types.html | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#HasSubset.Subset | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#Iff | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#Insert.insert | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#Ne | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#Singleton.singleton | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Function.html#Function.Injective | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Function.html#Function.Surjective | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Int/Basic.html#Int | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/List/Basic.html#List.Perm | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/List/Basic.html#List.sum | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Nat/Coprime.html#Nat.Coprime | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Nat/Gcd.html#Nat.gcd | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/NeZero.html#NeZero | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Rat/Basic.html#Rat | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#And | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#DecidableEq | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Dvd.dvd | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Eq | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#False | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Fin | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#GE.ge | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#GT.gt | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HAdd.hAdd | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HDiv.hDiv | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HMod.hMod | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HMul.hMul | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HPow.hPow | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HSMul.hSMul | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HSub.hSub | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Inv.inv | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#ite | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#LE.le | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#List | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#LT.lt | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Membership.mem | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Nat | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Neg.neg | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Nonempty | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Not | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Or | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Prod | Cannot find file: File not found. Check if file exists and path is correct

Errors in build/1000.html

  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/AbelRuffini.html#AbelRuffini.exists_not_solvable_by_rad | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/AscendingDescendingSequences.html#Theorems100.erdos_szekeres | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/BallotProblem.html#Ballot.ballot_problem | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/BallotProblem.html#Ballot.countedSequence | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/BallotProblem.html#Ballot.staysPositive | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/FriendshipGraphs.html#Theorems100.ExistsPolitician | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/FriendshipGraphs.html#Theorems100.Friendship | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/FriendshipGraphs.html#Theorems100.friendship_theorem | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/PerfectNumbers.html#Theorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.html#Theorems100.cubic_eq_zero_iff | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.html#Theorems100.quartic_eq_zero_iff | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Batteries/Data/List/Basic.html#List.prod | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/foundational_types.html | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#HasEquiv.Equiv | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#HasSubset.Subset | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#Iff | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#Insert.insert | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#Inter.inter | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#Ne | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#SDiff.sdiff | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#Singleton.singleton | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Core.html#Superset | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Function.html#Function.Injective | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Function.html#Function.Surjective | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Int/Basic.html#Int | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/List/Basic.html#List.Perm | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Nat/Coprime.html#Nat.Coprime | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Nat/Gcd.html#Nat.gcd | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/NeZero.html#NeZero | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Rat/Basic.html#Rat | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Data/Rat/Basic.html#Rat.den | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#And | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#DecidableEq | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#DecidablePred | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#DecidableRel | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Dvd.dvd | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Eq | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Fin | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Function.comp | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HAdd.hAdd | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HDiv.hDiv | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HMod.hMod | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HMul.hMul | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HPow.hPow | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HSMul.hSMul | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#HSub.hSub | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#id | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Inv.inv | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#LE.le | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#List | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#LT.lt | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Membership.mem | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Nat | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Neg.neg | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Nonempty | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Not | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Or | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Prod | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Prod.mk | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Subtype | Cannot find file: File not found. Check if file exists and path is correct
  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/Init/Prelude.html#Subtype.val | Cannot find file: File not found. Check if file exists and path is correct

Errors in build/glossary.html

  • [ERROR] file:///home/runner/work/leanprover-community.github.io/leanprover-community.github.io/build/simp.html#simp-normal-form | Cannot find file: File not found. Check if file exists and path is correct
    Full Github Actions output

@Vierkantor Vierkantor mentioned this pull request Feb 27, 2026
Merged
@kim-em
Copy link
Collaborator

kim-em commented Mar 4, 2026

@Vierkantor this is failing on all links into the doc-gen4 generated docs, I think. Shall we just filter those out from the link checker, to at least get something useful in?

@kim-em kim-em mentioned this pull request Mar 4, 2026
Closed
@kim-em
fix: rewrite all doc-relative links in header HTML, fix glossary link
7901a76 
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.
@kim-em
Copy link
Collaborator

kim-em commented Mar 4, 2026

:bot: says:

I had a look at the 134 errors. There are two pre-existing issues, and I've pushed a fix in 7901a76:

133 errors from make_site.py: The header HTML from header-data.json contains doc-relative links for all prefixes (Archive/, Init/, Batteries/, foundational_types.html), but only ./Mathlib/ links were being rewritten to ./mathlib4_docs/Mathlib/. The fix is to rewrite all href="./" links, not just ./Mathlib/. After that, the existing --exclude '/mathlib4_docs' catches everything.

1 error from glossary.md: The simp-normal form entry links to simp.html#simp-normal-form but the page is at extras/simp.html.

@Vierkantor
Copy link
Contributor Author

Vierkantor commented Mar 4, 2026

@kim-em true, the site has a lot of dead links in doc-gen. I opened #785 which sadly has gone without review for weeks now.

@kim-em
Copy link
Collaborator

kim-em commented Mar 5, 2026

@kim-em true, the site has a lot of dead links in doc-gen. I opened #785 which sadly has gone without review for weeks now.

Merged!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@bryangingechen bryangingechen bryangingechen left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Vierkantor @kim-em @bryangingechen