From ee7987a4fa9f29a2a1d083271f5c8176a8304b08 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 13:14:08 +0000 Subject: [PATCH 1/3] chore: Update Lean to v4.33.0 Toolchain and dependencies bumped by lean-update. --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) 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 From 7aec85b5d91b9fec2664157664896c8cbaf3d1b5 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 09:36:27 -0400 Subject: [PATCH 2/3] Update Nix --- flake.lock | 22 +++++++++++----------- flake.nix | 25 +++++++++++-------------- 2 files changed, 22 insertions(+), 25 deletions(-) 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]; }; }; }; From 7fbc246bbdd5d85dcb74ab90d9b5ecd6c1f10493 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 09:47:51 -0400 Subject: [PATCH 3/3] ci: Drop --wfail from update validation The action opens the update PR on both validation outcomes, so the validation verdict is not consumed by anything; the PR's own CI is the authority on whether the update builds, and it already enforces --wfail. --- .github/workflows/update.yml | 1 - 1 file changed, 1 deletion(-) 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 }}