diff --git a/.github/workflows/nix-ci.yml b/.github/workflows/nix-ci.yml
index 3f06a875e7..dd77663e69 100644
--- a/.github/workflows/nix-ci.yml
+++ b/.github/workflows/nix-ci.yml
@@ -90,6 +90,13 @@ jobs:
           # https://github.com/netlify/cli/issues/1809
           cp -r --dereference ./result ./dist
         if: matrix.name == 'Nix Linux'
+      - name: Check manual for broken links
+        id: lychee
+        uses: lycheeverse/lychee-action@v1.9.0
+        with:
+          fail: true
+          # gmplib.org consistently times out from GH actions
+          args: --base './dist' --no-progress --exclude 'gmplib.org' './dist/**/*.html'
       - name: Push to Cachix
         run: |
           [ -z "${{ secrets.CACHIX_AUTH_TOKEN }}" ] || cachix push -j4 lean4 ./push-* || true
@@ -112,6 +119,7 @@ jobs:
           echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
       - name: Publish manual to Netlify
         uses: nwtgck/actions-netlify@v2.0
+        id: publish-manual
         with:
           publish-dir: ./dist
           production-branch: master
diff --git a/doc/functions.md b/doc/functions.md
index 8da59fc04a..ae9d17a4c5 100644
--- a/doc/functions.md
+++ b/doc/functions.md
@@ -32,9 +32,7 @@ def fact x :=
 
 #eval fact 100
 ```
-By default, Lean only accepts total functions (see [The Equation
-Compiler](declarations.md#_the_equation_compiler) for how Lean determines
-whether functions are total).
+By default, Lean only accepts total functions.
 The `partial` keyword may be used to define a recursive function without a termination proof; `partial` functions compute in compiled programs, but are opaque in proofs and during type checking.
 ```lean
 partial def g (x : Nat) (p : Nat -> Bool) : Nat :=
diff --git a/doc/make/index.md b/doc/make/index.md
index eba03bdd7f..58eab87a43 100644
--- a/doc/make/index.md
+++ b/doc/make/index.md
@@ -10,7 +10,6 @@ Platform-Specific Setup
 
 - [Linux (Ubuntu)](ubuntu.md)
 - [Windows (msys2)](msys2.md)
-- [Windows (Visual Studio)](msvc.md)
 - [Windows (WSL)](wsl.md)
 - [macOS (homebrew)](osx-10.9.md)
 - Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it.
diff --git a/doc/metaprogramming-arith.md b/doc/metaprogramming-arith.md
index de03cac28f..b845ace808 100644
--- a/doc/metaprogramming-arith.md
+++ b/doc/metaprogramming-arith.md
@@ -60,7 +60,7 @@ While parsing `a * (b + c)`, `(b + c)` is assigned a precedence `60` by the addi
 the right argument to have precedence **at least** 71. Thus, this parse is invalid. In contrast, `(a * b) + c` assigns
 a precedence of `70` to `(a * b)`. This is compatible with addition which expects the left argument to have precedence
 **at least `60` ** (`70` is greater than `60`). Thus, the string `a * b + c` is parsed as `(a * b) + c`.
-For more details, please look at the [Lean manual on syntax extensions](../syntax.md#notations-and-precedence).
+For more details, please look at the [Lean manual on syntax extensions](./syntax.md#notations-and-precedence).
 
 To go from strings into `Arith`, we define a macro to
 translate the syntax category `arith` into an `Arith` inductive value that
diff --git a/doc/tour.md b/doc/tour.md
index 294f296225..010bf4076f 100644
--- a/doc/tour.md
+++ b/doc/tour.md
@@ -15,7 +15,7 @@ The most fundamental pieces of any Lean program are functions organized into nam
 [Functions](./functions.md) perform work on inputs to produce outputs,
 and they are organized under [namespaces](./namespaces.md),
 which are the primary way you group things in Lean.
-They are defined using the [`def`](./definitions.md) command,
+They are defined using the `def` command,
 which give the function a name and define its arguments.
 
 ```lean
diff --git a/doc/whatIsLean.md b/doc/whatIsLean.md
index 3c91dc80b6..ce14919978 100644
--- a/doc/whatIsLean.md
+++ b/doc/whatIsLean.md
@@ -37,6 +37,6 @@ Lean has numerous features, including:
 - [Extensible syntax](./syntax.md)
 - Hygienic macros
 - [Dependent types](https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html)
-- [Metaprogramming](./metaprogramming.md)
+- [Metaprogramming](./macro_overview.md)
 - Multithreading
 - Verification: you can prove properties of your functions using Lean itself