chore: Update Lean to v4.31.0

.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

.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

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

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

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

lean-toolchain

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