From 9fa9f39ec3874428826ebc0a8ff76fa8f8b27cbf Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Thu, 23 Oct 2025 20:31:39 +0200
Subject: [PATCH] chore: bump to latest Lean and Verso for a bug fix

---
 book/.verso/verso-xref-manifest.json     |  3 ++-
 book/FPLean/Examples.lean                | 12 ++++++------
 book/FPLean/Examples/OtherLanguages.lean |  2 +-
 book/lake-manifest.json                  |  4 ++--
 book/lean-toolchain                      |  2 +-
 5 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/book/.verso/verso-xref-manifest.json b/book/.verso/verso-xref-manifest.json
index d927854..cf2f25c 100644
--- a/book/.verso/verso-xref-manifest.json
+++ b/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"}},
diff --git a/book/FPLean/Examples.lean b/book/FPLean/Examples.lean
index f1e6381..418add1 100644
--- a/book/FPLean/Examples.lean
+++ b/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
diff --git a/book/FPLean/Examples/OtherLanguages.lean b/book/FPLean/Examples/OtherLanguages.lean
index 8d4760c..a6b3c56 100644
--- a/book/FPLean/Examples/OtherLanguages.lean
+++ b/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
diff --git a/book/lake-manifest.json b/book/lake-manifest.json
index 28dd393..132d071 100644
--- a/book/lake-manifest.json
+++ b/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",
diff --git a/book/lean-toolchain b/book/lean-toolchain
index 58ae245..137937a 100644
--- a/book/lean-toolchain
+++ b/book/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0
\ No newline at end of file
+leanprover/lean4:v4.25.0-rc2
\ No newline at end of file