From 41da41f2e89b84d7b704ba612a6e46c2419cd6e8 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 17 Jul 2026 16:33:30 -0400 Subject: [PATCH] chore: Update Lean to v4.31.0 --- .envrc | 4 ++++ .github/workflows/ci.yml | 14 ++++++++++++-- flake.lock | 6 +++--- flake.nix | 33 ++++++++++++++++++++++++++++++--- lake-manifest.json | 4 ++-- lakefile.lean | 4 ++-- lean-toolchain | 2 +- 7 files changed, 54 insertions(+), 13 deletions(-) diff --git a/.envrc b/.envrc index 3550a30..13060e1 100644 --- a/.envrc +++ b/.envrc @@ -1 +1,5 @@ +# Trust the flake's nixConfig (the Cachix substituter) without prompting, so +# the cache applies to every nix command in this shell, not just the devShell +# build. Non-direnv users are unaffected: nix asks them before using it. +export NIX_CONFIG="accept-flake-config = true" use flake diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 02521de..a719c1e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -61,5 +61,15 @@ jobs: with: nix_path: nixpkgs=channel:nixos-unstable github_access_token: ${{ secrets.GITHUB_TOKEN }} - - run: nix build --print-build-logs - - run: nix run .#test --print-build-logs + - uses: cachix/cachix-action@v16 + with: + name: argumentcomputer + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + - run: nix build --print-build-logs --accept-flake-config + # One step per check for separate logs; the store is shared across + # steps, so nothing rebuilds. + - run: nix build --print-build-logs --accept-flake-config .#checks.x86_64-linux.clippy + - run: nix build --print-build-logs --accept-flake-config .#checks.x86_64-linux.lean-ffi-test + # Catch-all: near-free after the steps above; fails if a check is added + # to the flake without a step here. + - run: nix flake check --accept-flake-config diff --git a/flake.lock b/flake.lock index 976ee40..a0b687b 100644 --- a/flake.lock +++ b/flake.lock @@ -79,11 +79,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1775267043, - "narHash": "sha256-yUCn4Wc5kLboN9JHom/SJAknn7aoSEDyerqFq3k7g0I=", + "lastModified": 1784223297, + "narHash": "sha256-rmEX8SXvtT7Fi8hOZuCXCbpyzno3iTQYnV3WKzsAVHw=", "owner": "lenianiva", "repo": "lean4-nix", - "rev": "56e917e2766385d0b096ea8be9c40ae54bfe138a", + "rev": "82993165f5f30879fc9d40734615ec54cb541e61", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index daefc6a..8a1a7f7 100644 --- a/flake.nix +++ b/flake.nix @@ -1,6 +1,15 @@ { description = "lean-ffi Nix flake (Lean4 + Rust)"; + nixConfig = { + extra-substituters = [ + "https://argumentcomputer.cachix.org" + ]; + extra-trusted-public-keys = [ + "argumentcomputer.cachix.org-1:ovhbTx1V56BYDerOWInQvXKXl68LlhNwEA+n7EWk1m4=" + ]; + }; + inputs = { # System packages, follows lean4-nix so we stay in sync nixpkgs.follows = "lean4-nix/nixpkgs"; @@ -68,8 +77,13 @@ pkgs.libiconv ]; }; - rustPkg = craneLib.buildPackage (craneArgs // {cargoExtraArgs = "--locked --workspace";}); - rustPkgTest = craneLib.buildPackage (craneArgs // {cargoExtraArgs = "--locked -p lean-ffi --features test-ffi";}); + # Build dependencies once and share them across the package build, the + # test static lib, and the clippy check instead of recompiling per consumer. + cargoArtifacts = craneLib.buildDepsOnly craneArgs; + rustPkg = craneLib.buildPackage (craneArgs // {inherit cargoArtifacts; cargoExtraArgs = "--locked --workspace";}); + # Static lib for the Lean FFI test suite; the Lean `lean-ffi-test` check + # is where that suite runs, so skip the Rust checkPhase here. + rustPkgTest = craneLib.buildPackage (craneArgs // {inherit cargoArtifacts; cargoExtraArgs = "--locked -p lean-ffi --features test-ffi"; doCheck = false;}); # Lake test package lake2nix = pkgs.callPackage lean4-nix.lake {}; @@ -97,7 +111,20 @@ packages = { default = rustPkg; - test = lakeTest; + }; + + checks = { + # Lint the Rust workspace; warnings are errors. + clippy = craneLib.cargoClippy (craneArgs + // { + inherit cargoArtifacts; + cargoClippyExtraArgs = "--workspace --all-targets --all-features -- -D warnings"; + }); + # Build and run the Lean FFI test suite as a flake check. + lean-ffi-test = pkgs.runCommand "lean-ffi-test" {} '' + ${lakeTest}/bin/LeanFFITests + touch $out + ''; }; # Provide a unified dev shell with Lean + Rust diff --git a/lake-manifest.json b/lake-manifest.json index bdb6374..1bd19a5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e", + "rev": "3e23a4ad2e91eaf07845cecad157b7ffbb437aed", "name": "LSpec", "manifestFile": "lake-manifest.json", - "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e", + "inputRev": "3e23a4ad2e91eaf07845cecad157b7ffbb437aed", "inherited": false, "configFile": "lakefile.toml"}], "name": "«lean-ffi-test»", diff --git a/lakefile.lean b/lakefile.lean index fc59983..9c3f4e3 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" @ "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e" + "https://github.com/argumentcomputer/LSpec" @ "3e23a4ad2e91eaf07845cecad157b7ffbb437aed" section FFI @@ -22,6 +22,6 @@ end FFI lean_lib Tests -@[test_driver] +@[default_target, test_driver] lean_exe LeanFFITests where root := `Tests.Main diff --git a/lean-toolchain b/lean-toolchain index 14791d7..18640c8 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.31.0