diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
index f61c0c4..e752648 100644
--- a/.github/workflows/update.yml
+++ b/.github/workflows/update.yml
@@ -32,5 +32,4 @@ jobs:
         with:
           bump_mode: pinned-tags
           on_update_fails: pr
-          build_args: "--wfail"
           token: ${{ steps.app-token.outputs.token }}
diff --git a/flake.lock b/flake.lock
index 584ef4f..6ffe5cb 100644
--- a/flake.lock
+++ b/flake.lock
@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1778716662,
-        "narHash": "sha256-m1Yf0wZ8j1OHjTc2UwHwyQRSnNeSgLJOd7q5Y45hzi4=",
+        "lastModified": 1785627969,
+        "narHash": "sha256-4dtXQk/NMePegK/nWp5NSeuZKLATItOq61lpEvmXqGw=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "f7c1a2d347e4c52d5fb8d10cb4d94b5884e546fb",
+        "rev": "427bf4bd9435fdf21321c8cc628c24efc14c0f7a",
         "type": "github"
       },
       "original": {
@@ -42,15 +42,15 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1784223297,
-        "narHash": "sha256-rmEX8SXvtT7Fi8hOZuCXCbpyzno3iTQYnV3WKzsAVHw=",
-        "owner": "lenianiva",
+        "lastModified": 1786478490,
+        "narHash": "sha256-fLEj7wL69j4DJva/lb5rp3m3fl6WBLMMy0V/F5clgJU=",
+        "owner": "argumentcomputer",
         "repo": "lean4-nix",
-        "rev": "82993165f5f30879fc9d40734615ec54cb541e61",
+        "rev": "2b15e1ffd5ee31e6bc4d30ec8afe0564317a8c26",
         "type": "github"
       },
       "original": {
-        "owner": "lenianiva",
+        "owner": "argumentcomputer",
         "repo": "lean4-nix",
         "type": "github"
       }
@@ -73,11 +73,11 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1777168982,
-        "narHash": "sha256-GOkGPcboWE9BmGCRMLX3worL4EMnsnG8MyKmXNeYuhQ=",
+        "lastModified": 1785031560,
+        "narHash": "sha256-OmshNvn2vupOFpYinLUu+1Dnpu4n7Q5N3ggGVNHpkUI=",
         "owner": "nix-community",
         "repo": "nixpkgs.lib",
-        "rev": "f5901329dade4a6ea039af1433fb087bd9c1fe14",
+        "rev": "0e79af5e3d4dcfcd676ab5ba3f95d2e3352e078c",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 4a4fe29..7893060 100644
--- a/flake.nix
+++ b/flake.nix
@@ -13,11 +13,10 @@
   inputs = {
     nixpkgs.follows = "lean4-nix/nixpkgs";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix.url = "github:lenianiva/lean4-nix";
+    lean4-nix.url = "github:argumentcomputer/lean4-nix";
   };
 
   outputs = inputs @ {
-    nixpkgs,
     flake-parts,
     lean4-nix,
     ...
@@ -33,43 +32,41 @@
       perSystem = {
         system,
         pkgs,
-        self',
-        config,
         ...
       }: let
-        lake2nix = pkgs.callPackage lean4-nix.lake {};
+        lean = lean4-nix.lib.${system}.fromToolchainFile ./lean-toolchain;
+        lake2nix = pkgs.callPackage lean4-nix.lake {inherit lean;};
+
+        # Restrict the build inputs to the files `lake build` reads, so edits
+        # to the flake, CI config, or docs don't invalidate the build.
+        src = lake2nix.cleanLakeSource ./.;
 
         # Library build, shared between the package output and the test check
         # so the `tests` exe reuses these artifacts instead of recompiling them.
         lspec = lake2nix.mkPackage {
           name = "LSpec";
-          src = ./.;
+          inherit src;
         };
 
         # `mkPackage "LSpec"` only builds the library target, so the `tests`
         # exe is built explicitly, reusing `lspec`'s build artifacts.
         lspecTest = lake2nix.mkPackage {
           name = "tests";
-          src = ./.;
+          inherit src;
           lakeArtifacts = lspec;
         };
       in {
-        _module.args.pkgs = import nixpkgs {
-          inherit system;
-          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
-        };
-
         # Build the library with `nix build`
         packages.default = lspec;
 
         # Build and run the test suite as a flake check (`nix flake check`).
-        checks.tests = pkgs.runCommand "LSpec-tests" { } ''
+        checks.tests = pkgs.runCommand "LSpec-tests" {} ''
           ${lspecTest}/bin/tests
           touch $out
         '';
 
         devShells.default = pkgs.mkShell {
-          packages = with pkgs.lean; [lean-all];
+          packages = [lean];
         };
       };
     };
diff --git a/lake-manifest.json b/lake-manifest.json
index 6f005e3..128455d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "LSpec",
diff --git a/lakefile.toml b/lakefile.toml
index 3ba5ef4..6490c28 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,7 +6,7 @@ testDriver = "tests"
 [[require]]
 name = "plausible"
 git = "https://github.com/leanprover-community/plausible"
-rev = "v4.31.0"
+rev = "v4.33.0"
 
 [[lean_lib]]
 name = "LSpec"
diff --git a/lean-toolchain b/lean-toolchain
index 18640c8..025e595 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.33.0