diff --git a/Manual/Classes.lean b/Manual/Classes.lean
index 28fc3c04..52a511c7 100644
--- a/Manual/Classes.lean
+++ b/Manual/Classes.lean
@@ -26,7 +26,6 @@ set_option pp.rawOnError true
 
 set_option linter.unusedVariables false
 
-
 set_option maxRecDepth 100000
 #doc (Manual) "Type Classes" =>
 %%%
@@ -269,7 +268,7 @@ def Heap.bubbleUp [Ord α] (i : Nat) (xs : Heap α) : Heap α :=
   else
     let j := i / 2
     if Ord.compare xs.contents[i] xs.contents[j] == .lt then
-      Heap.bubbleUp j {xs with contents := xs.contents.swap i j}
+      Heap.bubbleUp j { xs with contents := xs.contents.swap i j }
     else xs
 
 def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α :=
diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean
index 24cbf481..10de99a2 100644
--- a/Manual/Elaboration.lean
+++ b/Manual/Elaboration.lean
@@ -185,7 +185,7 @@ example (b : B) : ⟨b.1, b.2⟩ = b := rfl
 error: type mismatch
   rfl
 has type
-  ?m.848 = ?m.848 : Prop
+  ?m.854 = ?m.854 : Prop
 but is expected to have type
   e1 = e2 : Prop
 -/
diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean
index ab9ca1a5..70d1dd2d 100644
--- a/Manual/Language/InductiveTypes.lean
+++ b/Manual/Language/InductiveTypes.lean
@@ -582,7 +582,9 @@ mutual
   inductive FreshList (α : Type) (r : α → α → Prop) : Type where
     | nil : FreshList α r
     | cons (x : α) (xs : FreshList α r) (fresh : Fresh r x xs)
-  inductive Fresh (r : α → FreshList α → Prop) : α → FreshList α r → Prop where
+  inductive Fresh
+      (r : α → FreshList α → Prop) :
+      α → FreshList α r → Prop where
     | nil : Fresh r x .nil
     | cons : r x y → (f : Fresh r x ys) → Fresh r x (.cons y ys f)
 end
@@ -659,11 +661,16 @@ These mutually-inductive types are a somewhat complicated way to represent run-l
 mutual
   inductive RLE : List α → Type where
   | nil : RLE []
-  | run (x : α) (n : Nat) : n ≠ 0 → PrefixRunOf n x xs ys → RLE ys → RLE xs
+  | run (x : α) (n : Nat) :
+    n ≠ 0 → PrefixRunOf n x xs ys → RLE ys → RLE xs
 
   inductive PrefixRunOf : Nat → α → List α → List α → Type where
-  | zero (noMore : ¬∃zs, xs = x :: zs := by simp) : PrefixRunOf 0 x xs xs
-  | succ : PrefixRunOf n x xs ys → PrefixRunOf (n + 1) x (x :: xs) ys
+  | zero
+    (noMore : ¬∃zs, xs = x :: zs := by simp) :
+    PrefixRunOf 0 x xs xs
+  | succ :
+    PrefixRunOf n x xs ys →
+    PrefixRunOf (n + 1) x (x :: xs) ys
 end
 
 example : RLE [1, 1, 2, 2, 3, 1, 1, 1] :=
@@ -682,11 +689,18 @@ Specifying {name}`PrefixRunOf` as a {lean}`Prop` would be sensible, but it canno
 mutual
   inductive RLE : List α → Type where
   | nil : RLE []
-  | run (x : α) (n : Nat) : n ≠ 0 → PrefixRunOf n x xs ys → RLE ys → RLE xs
+  | run
+    (x : α) (n : Nat) :
+    n ≠ 0 → PrefixRunOf n x xs ys → RLE ys →
+    RLE xs
 
   inductive PrefixRunOf : Nat → α → List α → List α → Prop where
-  | zero (noMore : ¬∃zs, xs = x :: zs := by simp) : PrefixRunOf 0 x xs xs
-  | succ : PrefixRunOf n x xs ys → PrefixRunOf (n + 1) x (x :: xs) ys
+  | zero
+    (noMore : ¬∃zs, xs = x :: zs := by simp) :
+    PrefixRunOf 0 x xs xs
+  | succ :
+    PrefixRunOf n x xs ys →
+    PrefixRunOf (n + 1) x (x :: xs) ys
 end
 ```
 ```leanOutput rleBad
diff --git a/Manual/Meta/ElanOpt.lean b/Manual/Meta/ElanOpt.lean
index bb6965e4..6965b407 100644
--- a/Manual/Meta/ElanOpt.lean
+++ b/Manual/Meta/ElanOpt.lean
@@ -109,15 +109,15 @@ def elanOptDef.descr : InlineDescr where
   toHtml :=
     open Verso.Output.Html in
     some <| fun goB id data content => do
-      let .arr #[.str name, _jsonKind, meta] := data
+      let .arr #[.str name, _jsonKind, metadata] := data
         | HtmlT.logError s!"Failed to deserialize metadata for Elan option def: {data}"; content.mapM goB
 
       let idAttr := (← read).traverseState.htmlId id
 
-      let .ok meta := FromJson.fromJson? (α := Option String) meta
-        | HtmlT.logError s!"Failed to deserialize argument metadata for Elan option def: {meta}"; content.mapM goB
+      let .ok metadata := FromJson.fromJson? (α := Option String) metadata
+        | HtmlT.logError s!"Failed to deserialize argument metadata for Elan option def: {metadata}"; content.mapM goB
 
-      if let some mv := meta then
+      if let some mv := metadata then
         pure {{<code {{idAttr}} class="elan-opt">{{name}}" "{{mv}}</code>}}
       else
         pure {{<code {{idAttr}} class="elan-opt">{{name}}</code>}}
diff --git a/Manual/Meta/LakeOpt.lean b/Manual/Meta/LakeOpt.lean
index beb280e1..02731bd1 100644
--- a/Manual/Meta/LakeOpt.lean
+++ b/Manual/Meta/LakeOpt.lean
@@ -107,15 +107,15 @@ def lakeOptDef.descr : InlineDescr where
   toHtml :=
     open Verso.Output.Html in
     some <| fun goB id data content => do
-      let .arr #[.str name, _jsonKind, meta] := data
+      let .arr #[.str name, _jsonKind, metadata] := data
         | HtmlT.logError s!"Failed to deserialize metadata for Lake option def: {data}"; content.mapM goB
 
       let idAttr := (← read).traverseState.htmlId id
 
-      let .ok meta := FromJson.fromJson? (α := Option String) meta
-        | HtmlT.logError s!"Failed to deserialize argument metadata for Lake option def: {meta}"; content.mapM goB
+      let .ok metadata := FromJson.fromJson? (α := Option String) metadata
+        | HtmlT.logError s!"Failed to deserialize argument metadata for Lake option def: {metadata}"; content.mapM goB
 
-      if let some mv := meta then
+      if let some mv := metadata then
         pure {{<code {{idAttr}} class="lake-opt">{{name}}"="{{mv}}</code>}}
       else
         pure {{<code {{idAttr}} class="lake-opt">{{name}}</code>}}
@@ -149,7 +149,7 @@ def lakeOpt.descr : InlineDescr where
 
   toHtml :=
     open Verso.Output.Html in
-    some <| fun goB id data content => do
+    some <| fun goB _ data content => do
       let .arr #[.str name, .str original] := data
         | HtmlT.logError s!"Failed to deserialize metadata for Lake option ref: {data}"; content.mapM goB
 
diff --git a/Manual/Meta/ParserAlias.lean b/Manual/Meta/ParserAlias.lean
index 6a495bad..2c8f83ac 100644
--- a/Manual/Meta/ParserAlias.lean
+++ b/Manual/Meta/ParserAlias.lean
@@ -128,7 +128,7 @@ def parserAlias.descr : BlockDescr where
         if autoGroupArgs then
           some {{"Automatically wraps arguments in a " <code>"null"</code> " node unless there's exactly one"}}
         else none
-      let meta :=
+      let metadata :=
         match grp with
         | none => {{<p>{{arity}}</p>}}
         | some g => {{<ul><li>{{arity}}</li><li>{{g}}</li></ul>}}
@@ -139,7 +139,7 @@ def parserAlias.descr : BlockDescr where
           <span class="label">"parser alias"</span>
           <pre class="signature hl lean block">{{← (Highlighted.seq #[x, args]).toHtml}}</pre>
           <div class="text">
-            {{meta}}
+            {{metadata}}
             {{← contents.mapM goB}}
           </div>
         </div>
diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean
index 897c2430..c71a7c75 100644
--- a/Manual/Meta/Syntax.lean
+++ b/Manual/Meta/Syntax.lean
@@ -915,7 +915,7 @@ def withOpenedNamespaces (nss : List Name) (act : DocElabM α) : DocElabM α :=
 
 
 inductive SearchableTag where
-  | meta
+  | metavar
   | keyword
   | literalIdent
   | ws
@@ -924,13 +924,13 @@ deriving DecidableEq, Ord, Repr
 open Lean.Syntax in
 instance : Quote SearchableTag where
   quote
-    | .meta => mkCApp ``SearchableTag.meta #[]
+    | .metavar => mkCApp ``SearchableTag.metavar #[]
     | .keyword => mkCApp ``SearchableTag.keyword #[]
     | .literalIdent => mkCApp ``SearchableTag.literalIdent #[]
     | .ws => mkCApp ``SearchableTag.ws #[]
 
 def SearchableTag.toKey : SearchableTag → String
-  | .meta => "meta"
+  | .metavar => "meta"
   | .keyword => "keyword"
   | .literalIdent => "literalIdent"
   | .ws => "ws"
@@ -941,7 +941,7 @@ instance : ToJson SearchableTag where
   toJson := SearchableTag.toJson
 
 def SearchableTag.fromJson? : Json → Except String SearchableTag
-  | .str "meta" => pure .meta
+  | .str "meta" => pure .metavar
   | .str "keyword" => pure .keyword
   | .str "literalIdent" => pure .literalIdent
   | .str "ws" => pure .ws
@@ -967,7 +967,7 @@ def searchableJson (ss : Array (SearchableTag × String)) : Json :=
 partial def searchable (cat : Name) (txt : TaggedText GrammarTag) : Array (SearchableTag × String) :=
   (go txt *> get).run' #[] |> fixup
 where
-  dots : SearchableTag × String := (.meta, "…")
+  dots : SearchableTag × String := (.metavar, "…")
   go : TaggedText GrammarTag → StateM (Array (SearchableTag × String)) String
     | .text s => do
       ws s
@@ -1007,9 +1007,9 @@ where
           if st.isEmpty then return st
         -- Don't parenthesize just "..."
         | ")" | ")?" | ")*" =>
-          if let some st' := suffixMatches #[(· == (.meta, "(")) , (· == dots)] st then return st'.push dots
+          if let some st' := suffixMatches #[(· == (.metavar, "(")) , (· == dots)] st then return st'.push dots
         | _ => pure ()
-        return st.push (.meta, s)
+        return st.push (.metavar, s)
       pure s
     | .tag other txt => do
       go txt
@@ -1019,7 +1019,7 @@ where
     | `command => Id.run do
       -- Drop leading ellipses from commands
       for h : i in [0:s.size] do
-        if s[i] ∉ [dots, (.meta, "?"), (.ws, " ")] then return s.extract i s.size
+        if s[i] ∉ [dots, (.metavar, "?"), (.ws, " ")] then return s.extract i s.size
       return s
     | _ => s
   ws (s : String) : StateM (Array (SearchableTag × String)) Unit := do
@@ -1051,7 +1051,7 @@ where
       -- Don't push ellipsis onto ellipsis
       if let some _ := suffixMatches #[(· == dots)] st then st
       -- Don't alternate ellipses
-      else if let some st' := suffixMatches #[(· == dots), (· == (.meta, "|"))] st then st'.push dots
+      else if let some st' := suffixMatches #[(· == dots), (· == (.metavar, "|"))] st then st'.push dots
       else st.push dots
 
 
@@ -1061,19 +1061,19 @@ where
 
 /-- info: some #[(Manual.SearchableTag.keyword, "aaa")] -/
 #guard_msgs in
-#eval searchable.suffixMatches #[(· == (.meta, "(")), (· == searchable.dots)] #[(.keyword, "aaa"),(.meta, "("), (.ws, " "),(.meta, "…")]
+#eval searchable.suffixMatches #[(· == (.metavar, "(")), (· == searchable.dots)] #[(.keyword, "aaa"),(.metavar, "("), (.ws, " "),(.metavar, "…")]
 
 /-- info: some #[(Manual.SearchableTag.keyword, "aaa")] -/
 #guard_msgs in
-#eval searchable.suffixMatches #[(· == searchable.dots)] #[(.keyword, "aaa"),(.meta, "…"), (.ws, " ")]
+#eval searchable.suffixMatches #[(· == searchable.dots)] #[(.keyword, "aaa"),(.metavar, "…"), (.ws, " ")]
 
 /-- info: some #[] -/
 #guard_msgs in
-#eval searchable.suffixMatches #[(· == searchable.dots)] #[(.meta, "…"), (.ws, " ")]
+#eval searchable.suffixMatches #[(· == searchable.dots)] #[(.metavar, "…"), (.ws, " ")]
 
 /-- info: some #[] -/
 #guard_msgs in
-#eval searchable.suffixMatches #[(· == searchable.dots)] #[(.meta, "…")]
+#eval searchable.suffixMatches #[(· == searchable.dots)] #[(.metavar, "…")]
 
 open Manual.Meta.PPrint Grammar in
 /--
diff --git a/Manual/Monads/Lift.lean b/Manual/Monads/Lift.lean
index b7cca446..c1ca0a68 100644
--- a/Manual/Monads/Lift.lean
+++ b/Manual/Monads/Lift.lean
@@ -212,7 +212,8 @@ def getByte (n : Nat) : Except String UInt8 :=
     pure n.toUInt8
   else throw s!"Out of range: {n}"
 
-def getBytes (input : Array Nat) : StateT (Array UInt8) (Except String) Unit := do
+def getBytes (input : Array Nat) :
+    StateT (Array UInt8) (Except String) Unit := do
   input.forM fun i =>
     liftM (Except.tryCatch (some <$> getByte i) fun _ => pure none) >>=
       fun
@@ -233,7 +234,10 @@ Ideally, state updates would be performed within the {name}`tryCatch` call direc
 
 Attempting to save bytes and handled exceptions does not work, however, because the arguments to {name}`Except.tryCatch` have type {lean}`Except String Unit`:
 ```lean (error := true) (name := getBytesErr) (keep := false)
-def getBytes' (input : Array Nat) : StateT (Array String) (StateT (Array UInt8) (Except String)) Unit := do
+def getBytes' (input : Array Nat) :
+    StateT (Array String)
+      (StateT (Array UInt8)
+        (Except String)) Unit := do
   input.forM fun i =>
     liftM
       (Except.tryCatch
@@ -254,7 +258,10 @@ It provides the inner action with an interpreter for the outer monad.
 In the case of {name}`StateT`, this interpreter expects that the inner monad returns a tuple that includes the updated state, and takes care of providing the initial state and extracting the updated state from the tuple.
 
 ```lean
-def getBytes' (input : Array Nat) : StateT (Array String) (StateT (Array UInt8) (Except String)) Unit := do
+def getBytes' (input : Array Nat) :
+    StateT (Array String)
+      (StateT (Array UInt8)
+        (Except String)) Unit := do
   input.forM fun i =>
     control fun run =>
       (Except.tryCatch
diff --git a/Manual/Monads/Syntax.lean b/Manual/Monads/Syntax.lean
index a2ea1db2..5c15365b 100644
--- a/Manual/Monads/Syntax.lean
+++ b/Manual/Monads/Syntax.lean
@@ -563,7 +563,9 @@ When iterating over multiple collections, iteration stops when any of the collec
 
 When iterating over the valid indices for an array with {keywordOf Lean.Parser.Term.doFor}`for`, naming the membership proof allows the tactic that searches for proofs that array indices are in bounds to succeed.
 ```lean (keep := false)
-def satisfyingIndices (p : α → Prop) [DecidablePred p] (xs : Array α) : Array Nat := Id.run do
+def satisfyingIndices
+    (p : α → Prop) [DecidablePred p]
+    (xs : Array α) : Array Nat := Id.run do
   let mut out := #[]
   for h : i in [0:xs.size] do
     if p xs[i] then out := out.push i
diff --git a/Manual/RecursiveDefs/Structural.lean b/Manual/RecursiveDefs/Structural.lean
index 3d14e079..abf3960f 100644
--- a/Manual/RecursiveDefs/Structural.lean
+++ b/Manual/RecursiveDefs/Structural.lean
@@ -17,6 +17,8 @@ open Verso.Genre.Manual.InlineLean
 
 open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
 
+set_option guard_msgs.diff true
+
 #doc (Manual) "Structural Recursion" =>
 %%%
 tag := "structural-recursion"
@@ -157,7 +159,8 @@ The decreasing parameter's type must be an inductive type.
 In {lean}`notInductive`, a function is specified as the decreasing parameter:
 
 ```lean (error := true) (name := badnoindct)
-def notInductive (x : Nat → Nat) : Nat := notInductive (fun n => x (n+1))
+def notInductive (x : Nat → Nat) : Nat :=
+  notInductive (fun n => x (n+1))
 termination_by structural x
 ```
 ```leanOutput badnoindct
@@ -573,7 +576,7 @@ set_option pp.all true in
 trace: [Elab.definition.body] half : Nat → Nat :=
     fun (x : Nat) =>
       half.match_1.{1} (fun (x : Nat) => Nat) x (fun (_ : Unit) => Nat.zero) (fun (_ : Unit) => Nat.zero)
-        fun (n : Nat) => Nat.succ (half n)
+        fun (n : Nat) => Nat.succ (_root_.half n)
 -/
 #guard_msgs in
 def half : Nat → Nat
diff --git a/Manual/RecursiveDefs/WF/PreprocessExample.lean b/Manual/RecursiveDefs/WF/PreprocessExample.lean
index 5969a305..0deac9c8 100644
--- a/Manual/RecursiveDefs/WF/PreprocessExample.lean
+++ b/Manual/RecursiveDefs/WF/PreprocessExample.lean
@@ -176,7 +176,9 @@ macro "sizeOf_pair_dec" : tactic =>
     omega
     done)
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_pair_dec)
+macro_rules
+  | `(tactic| decreasing_trivial) =>
+    `(tactic| sizeOf_pair_dec)
 
 def Tree.map (f : α → β) : Tree α → Tree β
   | leaf x => leaf (f x)
diff --git a/Manual/Terms.lean b/Manual/Terms.lean
index b0cf7739..1dcf348e 100644
--- a/Manual/Terms.lean
+++ b/Manual/Terms.lean
@@ -1321,9 +1321,9 @@ partial instance : OfNat Blah n where
 -- This shows that the partial instance was not unfolded
 /--
 error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
-  motive (instOfNatBlah_1.f 0) : Sort ?u.903
+  motive (instOfNatBlah_1.f 0) : Sort ?u.909
 but is expected to have type
-  motive n✝ : Sort ?u.903
+  motive n✝ : Sort ?u.909
 -/
 #guard_msgs in
 def defg (n : Blah) : Bool :=
@@ -1332,9 +1332,9 @@ def defg (n : Blah) : Bool :=
 
 /--
 error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
-  motive (Float.ofScientific 25 true 1) : Sort ?u.946
+  motive (Float.ofScientific 25 true 1) : Sort ?u.953
 but is expected to have type
-  motive x✝ : Sort ?u.946
+  motive x✝ : Sort ?u.953
 -/
 #guard_msgs in
 def twoPointFive? : Float → Option Float
@@ -1391,7 +1391,7 @@ is not definitionally equal to the right-hand side
   3 = 5
 ⊢ 3 = 3 ∨ 3 = 5
 ---
-info: { val := 3, val2 := ?m.1743, ok := ⋯ } : OnlyThreeOrFive
+info: { val := 3, val2 := ?m.1757, ok := ⋯ } : OnlyThreeOrFive
 -/
 #guard_msgs in
 #check OnlyThreeOrFive.mk 3 ..
@@ -1439,9 +1439,21 @@ This {tech}[indexed family] describes mostly-balanced trees, with the depth enco
 ```lean
 inductive BalancedTree (α : Type u) : Nat → Type u where
   | empty : BalancedTree α 0
-  | branch (left : BalancedTree α n) (val : α) (right : BalancedTree α n) : BalancedTree α (n + 1)
-  | lbranch (left : BalancedTree α (n + 1)) (val : α) (right : BalancedTree α n) : BalancedTree α (n + 2)
-  | rbranch (left : BalancedTree α n) (val : α) (right : BalancedTree α (n + 1)) : BalancedTree α (n + 2)
+  | branch
+    (left : BalancedTree α n)
+    (val : α)
+    (right : BalancedTree α n) :
+    BalancedTree α (n + 1)
+  | lbranch
+    (left : BalancedTree α (n + 1))
+    (val : α)
+    (right : BalancedTree α n) :
+    BalancedTree α (n + 2)
+  | rbranch
+    (left : BalancedTree α n)
+    (val : α)
+    (right : BalancedTree α (n + 1)) :
+    BalancedTree α (n + 2)
 ```
 
 To begin the implementation of a function to construct a perfectly balanced tree with some initial element and a given depth, a {tech}[hole] can be used for the definition.
@@ -1461,7 +1473,9 @@ depth : Nat
 Matching on the expected depth and inserting holes results in an error message for each hole.
 These messages demonstrate that the expected type has been refined, with `depth` replaced by the matched values.
 ```lean (error := true) (name := fill2)
-def BalancedTree.filledWith (x : α) (depth : Nat) : BalancedTree α depth :=
+def BalancedTree.filledWith
+    (x : α) (depth : Nat) :
+    BalancedTree α depth :=
   match depth with
   | 0 => _
   | n + 1 => _
diff --git a/lake-manifest.json b/lake-manifest.json
index d0e1586d..9ed3df26 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "136f897aa927cacc71a396479a296f5228673135",
+   "rev": "94472367e2ad3acae8fd8d46267a7ae991d5ee62",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b2be765e1989efb87f63d427b11e3d9d974603a2",
+   "rev": "9ff8c4e0d9912170d5cfc2e5067231d5f6eaac3c",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.lean b/lakefile.lean
index a8b86868..f116f29e 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -19,6 +19,7 @@ package "verso-manual" where
       #["-Wl,-ignore_optimization_hints"]
     else #[]
 
+  leanOptions := #[⟨`weak.verso.code.warnLineLength, .ofNat 72⟩]
 
 lean_lib Manual where
 
diff --git a/lean-toolchain b/lean-toolchain
index 42fa6a00..a8cce637 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-06-01
+leanprover/lean4:nightly-2025-06-05