Skip to content

CI: check for dead links#792

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

CI: check for dead links#792
Vierkantor wants to merge 3 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

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.

2 participants

@Vierkantor @bryangingechen