chore: bump to latest Lean and Verso for a bug fix

book/.verso/verso-xref-manifest.json

@@ -1,7 +1,8 @@
 {"version": 0,
  "sources":
  {"manual":
-  {"updateFrequency": "manual",
+  {"updated": "2025-10-23:16:40:12.244921000",
+   "updateFrequency": "manual",
    "shortName": "ref",
    "root": "https://lean-lang.org/doc/reference/4.23.0/",
    "longName": "Lean Language Reference"}},

book/FPLean/Examples.lean

@@ -460,7 +460,7 @@ private def editCodeBlock [Monad m] [MonadFileMap m] (stx : Syntax) (newContents
   let some rng := stx.getRange?
     | pure none
   let { start := {line := l1, ..}, .. } := txt.utf8RangeToLspRange rng
-  let line1 := txt.source.extract (txt.lineStart (l1 + 1)) (txt.lineStart (l1 + 2))
+  let line1 := (txt.lineStart (l1 + 1)).extract txt.source (txt.lineStart (l1 + 2))
   if line1.startsWith "```" then
     return some s!"{delims}{line1.dropWhile (· == '`') |>.trim}\n{withNl newContents}{delims}"
   else
@@ -859,7 +859,7 @@ def plainFile : CodeBlockExpander
     return #[← ``(Block.other (InlineLean.Block.exampleFile (FileType.other $(quote (show?.getD (fn.fileName.getD fn.toString))))) #[Block.code $(quote contents)])]
 
 
-private def severityName {m} [Monad m] [MonadEnv m] [MonadResolveName m] : MessageSeverity → m String
+private def severityName {m} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadOptions m] [MonadLog m] [AddMessageContext m] : MessageSeverity → m String
   | .error => unresolveNameGlobal ``MessageSeverity.error <&> (·.toString)
   | .warning => unresolveNameGlobal ``MessageSeverity.warning <&> (·.toString)
   | .information => unresolveNameGlobal ``MessageSeverity.information <&> (·.toString)
@@ -959,16 +959,16 @@ def hasSubstring (s pattern : String) : Bool :=
   if h : pattern.endPos.1 = 0 then false
   else
     have hPatt := Nat.zero_lt_of_ne_zero h
-    let rec loop (pos : String.Pos) :=
+    let rec loop (pos : String.Pos.Raw) :=
       if h : pos.byteIdx + pattern.endPos.byteIdx > s.endPos.byteIdx then
         false
       else
         have := Nat.lt_of_lt_of_le (Nat.add_lt_add_left hPatt _) (Nat.ge_of_not_lt h)
-        if s.substrEq pos pattern 0 pattern.endPos.byteIdx then
+        if pos.substrEq s pattern 0 pattern.endPos.byteIdx then
           have := Nat.sub_lt_sub_left this (Nat.add_lt_add_left hPatt _)
           true
         else
-          have := Nat.sub_lt_sub_left this (s.lt_next pos)
-          loop (s.next pos)
+          have := Nat.sub_lt_sub_left this (pos.byteIdx_lt_byteIdx_next s)
+          loop (pos.next s)
       termination_by s.endPos.1 - pos.1
     loop 0

book/FPLean/Examples/OtherLanguages.lean

@@ -173,7 +173,7 @@ private def stringAnchors (s : String) : Except String (String × HashMap String
   let mut out := ""
   let mut anchors : HashMap String String := {}
   let mut openAnchors : HashMap String String := {}
-  let lines := s.split (· == '\n')
+  let lines := s.splitToList (· == '\n')
   for line in lines do
     if let some (a, isOpener) := anchor? line |>.toOption then
       if isOpener then

book/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c68870b3fd3ae8e99ea242bf17197db3b0d39b0f",
+   "rev": "b1cdd66be1f055926796aa804fdc13c9e9ac17c6",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "767f10408ca8abe29a15add2bf111eefdd9522b2",
+   "rev": "57f4e6c99a4132d54a2105dec21c2e3c2af98b15",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

book/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.25.0-rc2