chore: Update Lean to v4.33.0

.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 }}

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];
         };
       };
     };

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",

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"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.33.0