From 05adb42c260a317725c344dfb9f172d6708c37a7 Mon Sep 17 00:00:00 2001
From: justincasher <justinchadwickasher@gmail.com>
Date: Thu, 7 May 2026 15:49:19 -0400
Subject: [PATCH] Bump PhysLean extractor to v4.29.1

PhysLean upstream is on Lean v4.29.1 and has not bumped to v4.30. The
extractor's lean-toolchain was at v4.30.0-rc1 and doc-gen4 at v4.29.0,
which left the extractor mismatched against PhysLean main and produced
stale data. Align both to v4.29.1.

Manifests regenerated via `lake update`.
---
 lean/physlean/lake-manifest.json | 19 +++++++++----------
 lean/physlean/lakefile.lean      |  2 +-
 lean/physlean/lean-toolchain     |  2 +-
 3 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/lean/physlean/lake-manifest.json b/lean/physlean/lake-manifest.json
index f9f03ae..b9844e2 100644
--- a/lean/physlean/lake-manifest.json
+++ b/lean/physlean/lake-manifest.json
@@ -1,11 +1,11 @@
-{"version": "1.2.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/HEPLean/PhysLean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5b4db3a0254fc18b9af5bcd1f5f7b0ff70e437da",
+   "rev": "04ab5a9d13b4e306795ed6970f5ade5dc699c3f7",
    "name": "PhysLean",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -15,20 +15,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "aa4c3e4e14f5b31495b7c7238762ecceddd9f52c",
+   "rev": "a0aebd77a6619214a727994fade0e05203fc5252",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.29.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95",
+   "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.29.1",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3",
+   "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.95",
+   "inputRev": "v0.0.95+lean-v4.29.1",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
@@ -152,5 +152,4 @@
    "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "«physlean-extractor»",
- "lakeDir": ".lake",
- "fixedToolchain": false}
+ "lakeDir": ".lake"}
diff --git a/lean/physlean/lakefile.lean b/lean/physlean/lakefile.lean
index b819436..c09ab62 100644
--- a/lean/physlean/lakefile.lean
+++ b/lean/physlean/lakefile.lean
@@ -9,7 +9,7 @@ lean_lib «PhysExtract» where
   roots := #[`PhysExtract]
 
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "v4.29.0"
+  "https://github.com/leanprover/doc-gen4" @ "v4.29.1"
 
 require PhysLean from git
   "https://github.com/HEPLean/PhysLean"
diff --git a/lean/physlean/lean-toolchain b/lean/physlean/lean-toolchain
index 79ac861..33e0c08 100644
--- a/lean/physlean/lean-toolchain
+++ b/lean/physlean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.30.0-rc1
\ No newline at end of file
+leanprover/lean4:v4.29.1