From a35c3a7c9bd6cf2281022b42d95ee92f193dd949 Mon Sep 17 00:00:00 2001
From: Alok Singh <alokbeniwal@gmail.com>
Date: Fri, 10 Jul 2026 15:22:53 -0700
Subject: [PATCH 1/2] Update Lean toolchain to v4.32.0-rc1

---
 lake-manifest.json | 29 ++++++++++++++++++++---------
 lakefile.toml      |  2 ++
 lean-toolchain     |  2 +-
 3 files changed, 23 insertions(+), 10 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 8cc0d5f..e66d9f0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,31 +1,41 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6f0c12be90063de6d4e5ca14867ad7243064ad99",
+   "rev": "8cb04559a9b9feb8efab43e135f662514561f668",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.32.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "627a9728700546ebc9cc274821ad7c0b420c2e35",
+   "rev": "e4952ae2afde0dd2868b313356d1ce00da677bd9",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.104",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/illuminate",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e",
+   "name": "illuminate",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
+   "rev": "f3f26cc72646205ca167117487c008ee1dafe816",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "38ac5945d744903ffcc473ce1030223991b11cf6",
+   "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,11 +55,12 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "eb77622e97e942ba2cfe02f60637705fc2d9481b",
+   "rev": "0bd508e8362f56d4a05cbf63614d4c97db954041",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "LeanPlot",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
index 1a1d5e7..784b445 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -54,7 +54,9 @@ root = "TestExport"
 [[require]]
 name = "proofwidgets"
 scope = "leanprover-community"
+rev = "v0.0.104"
 
 [[require]]
 name = "verso"
 scope = "leanprover"
+rev = "v4.32.0-rc1"
diff --git a/lean-toolchain b/lean-toolchain
index bd19bde..2694eb7 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.27.0-rc1
+leanprover/lean4:v4.32.0-rc1

From afeb8047aa280f9c760e437f217c399c1afd8673 Mon Sep 17 00:00:00 2001
From: Alok Singh <alokbeniwal@gmail.com>
Date: Fri, 10 Jul 2026 15:28:11 -0700
Subject: [PATCH 2/2] Update docs generator for Verso 4.32

---
 doc/LeanPlotDocMain.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/LeanPlotDocMain.lean b/doc/LeanPlotDocMain.lean
index 70a5329..4f25fd6 100644
--- a/doc/LeanPlotDocMain.lean
+++ b/doc/LeanPlotDocMain.lean
@@ -11,11 +11,11 @@ open Verso.Genre.Manual.InlineLean
 
 def config : Config where
   emitTeX := false
-  emitHtmlSingle := true
-  emitHtmlMulti := true
+  emitHtmlSingle := .immediately
+  emitHtmlMulti := .immediately
   htmlDepth := 2
   destination := "_out/docs"
   sourceLink := some "https://github.com/alok/LeanPlot"
   issueLink := some "https://github.com/alok/LeanPlot/issues"
 
-def main := manualMain (%doc Manual) (config := config)
+def main := manualMain (%doc Manual) (config := { config with })