From 7970afaacc518087f623cffa2bea9884921ca0ef Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Sat, 22 Aug 2026 00:18:10 +0000
Subject: [PATCH 1/3] chore: Update Lean to v4.33.1

Toolchain and dependencies bumped by lean-update.
---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 025e595..a8afa7d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.0
+leanprover/lean4:v4.33.1

From 74cd691fcd3f4fba540a47e137f801b9713e0319 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Sat, 22 Aug 2026 11:32:46 -0400
Subject: [PATCH 2/3] Update lean4-nix

---
 flake.lock | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/flake.lock b/flake.lock
index b5b5fbf..f82621f 100644
--- a/flake.lock
+++ b/flake.lock
@@ -2,11 +2,11 @@
   "nodes": {
     "crane": {
       "locked": {
-        "lastModified": 1785782307,
-        "narHash": "sha256-MPaRdVkf6zZP5fCPxYCi8Dr4pZzgmXzg8T9nVEbp3Mw=",
+        "lastModified": 1787326676,
+        "narHash": "sha256-lWhBbBvC05/xwivKBBiM2YNizpmgqCgyOIzomvRuwxs=",
         "owner": "ipetkov",
         "repo": "crane",
-        "rev": "2c71e194474d13de031d729b729c968ddbe3507f",
+        "rev": "692f7e9ef2ece8125b466f66f2af532b3edaed0d",
         "type": "github"
       },
       "original": {
@@ -24,11 +24,11 @@
         "rust-analyzer-src": "rust-analyzer-src"
       },
       "locked": {
-        "lastModified": 1786520346,
-        "narHash": "sha256-2CVNv6zvKhr/Xky1jkZXZfCTKfZpyo0gij70lR1DMTA=",
+        "lastModified": 1787381277,
+        "narHash": "sha256-ZTCk8w6UKzlWSJiFtQTy+HahC79d/p5kh97prdRkkHE=",
         "owner": "nix-community",
         "repo": "fenix",
-        "rev": "9a4f7863c93539f17a1785962d58471fdc7f5fe4",
+        "rev": "eacb66f3a1e40cc5ac88ef588ed6bc9bbff1c79c",
         "type": "github"
       },
       "original": {
@@ -79,11 +79,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1786543565,
-        "narHash": "sha256-zHMoHO85jizkIXH0OfnvabpNLTl90rR3GCc1h/e2sx4=",
+        "lastModified": 1787412565,
+        "narHash": "sha256-M1y7JYDUzvOSYv0DWcCCmkL2DqDfQZePsKDrQf/Or6U=",
         "owner": "argumentcomputer",
         "repo": "lean4-nix",
-        "rev": "4026c657eecf16beea7d266ce32933ef3d7db2e5",
+        "rev": "1ecad9d6f99cf3255a858861c9a2e6966cdd0290",
         "type": "github"
       },
       "original": {
@@ -153,11 +153,11 @@
     "rust-analyzer-src": {
       "flake": false,
       "locked": {
-        "lastModified": 1786467811,
-        "narHash": "sha256-56LDY016VYO+KOfJ3FN98kM7S2GIE2HQSbkxgzXW6jE=",
+        "lastModified": 1787308443,
+        "narHash": "sha256-Ou4Up06Sr6pm+Q3nKm0zZdqajHXM9sCSRNrOhE3Fm7g=",
         "owner": "rust-lang",
         "repo": "rust-analyzer",
-        "rev": "b2d445b22a2dd4c3469dfeddc2d5eb533c42baf6",
+        "rev": "d2e55da49132fa70a13dfbdc99122432b02cf464",
         "type": "github"
       },
       "original": {

From c86c645ff0e2c877e33024a469f27a9f0fdac405 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Sat, 22 Aug 2026 11:48:06 -0400
Subject: [PATCH 3/3] Update LSpec

---
 lake-manifest.json | 4 ++--
 lakefile.lean      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 829ac22..b09a5c2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e780f4188c9649aef988270f4d126651460ca9c4",
+   "rev": "ab4d5eb461941837f48eb891be755c8c73e89fdd",
    "name": "LSpec",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "e780f4188c9649aef988270f4d126651460ca9c4",
+   "inputRev": "ab4d5eb461941837f48eb891be755c8c73e89fdd",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
diff --git a/lakefile.lean b/lakefile.lean
index 0ab72a0..85c896f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -5,7 +5,7 @@ package «lean-ffi-test» where
   version := v!"0.1.0"
 
 require LSpec from git
-  "https://github.com/argumentcomputer/LSpec" @ "e780f4188c9649aef988270f4d126651460ca9c4"
+  "https://github.com/argumentcomputer/LSpec" @ "ab4d5eb461941837f48eb891be755c8c73e89fdd"
 
 section FFI