From 34bde36463d54b1c83abaa7be365bb267c16dfca Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 16 Oct 2025 13:02:19 -0400
Subject: [PATCH 1/2] Run 'lake update' to get latest version of verso, add a
 corresponding sourcmap field that this requires

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

diff --git a/book/.verso/verso-xref-manifest.json b/book/.verso/verso-xref-manifest.json
index d927854..f6a54d9 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-16:12:58:47.024355000",
+   "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 2613db3..f1e6381 100644
--- a/book/FPLean/Examples.lean
+++ b/book/FPLean/Examples.lean
@@ -159,7 +159,7 @@ block_extension Block.leanEvalSteps (steps : Array Highlighted) where
   toTeX := none
   extraCss := [highlightingStyle, evalStepsStyle]
   extraJs := [highlightingJs]
-  extraJsFiles := [{filename := "popper.js", contents := popper}, {filename := "tippy.js", contents := tippy}]
+  extraJsFiles := [{filename := "popper.js", contents := popper, sourceMap? := none}, {filename := "tippy.js", contents := tippy, sourceMap? := none}]
   extraCssFiles := [("tippy-border.css", tippy.border.css)]
   toHtml :=
     open Verso.Output.Html in
@@ -263,7 +263,7 @@ block_extension Block.leanOutput (severity : MessageSeverity) (message : String)
         pure <| .seq #[← go b, .raw "\n"]
   extraCss := [highlightingStyle]
   extraJs := [highlightingJs]
-  extraJsFiles := [{filename := "popper.js", contents := popper}, {filename := "tippy.js", contents := tippy}]
+  extraJsFiles := [{filename := "popper.js", contents := popper, sourceMap? := none}, {filename := "tippy.js", contents := tippy, sourceMap? := none}]
   extraCssFiles := [("tippy-border.css", tippy.border.css)]
   toHtml :=
     open Verso.Output.Html in
diff --git a/book/lake-manifest.json b/book/lake-manifest.json
index 3c1ebdf..2b4ac9f 100644
--- a/book/lake-manifest.json
+++ b/book/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a54297313f81c9243c4e8c1e72270c1f7681f0f0",
+   "rev": "5a9318d373ee1c5dfc7443952b30f913ec36298b",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/book/lean-toolchain b/book/lean-toolchain
index fd384f2..58ae245 100644
--- a/book/lean-toolchain
+++ b/book/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0-rc1
+leanprover/lean4:v4.24.0
\ No newline at end of file

From 70ea603acca3c16324b33bc1cb1f4c89aaa90385 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Fri, 17 Oct 2025 20:34:46 -0400
Subject: [PATCH 2/2] Update to latest verso

---
 book/lake-manifest.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/book/lake-manifest.json b/book/lake-manifest.json
index 2b4ac9f..2587717 100644
--- a/book/lake-manifest.json
+++ b/book/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5a9318d373ee1c5dfc7443952b30f913ec36298b",
+   "rev": "38b11d9518e544b08b5b27e91197dfdb2b86690a",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",