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
-      - run: nix run .#test
+      - 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.blake3-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 = "Blake3 Nix Flake";
 
+  nixConfig = {
+    extra-substituters = [
+      "https://argumentcomputer.cachix.org"
+    ];
+    extra-trusted-public-keys = [
+      "argumentcomputer.cachix.org-1:ovhbTx1V56BYDerOWInQvXKXl68LlhNwEA+n7EWk1m4="
+    ];
+  };
+
   inputs = {
     nixpkgs.follows = "lean4-nix/nixpkgs";
     flake-parts.url = "github:hercules-ci/flake-parts";
@@ -81,7 +90,7 @@
 
         # Rust package
         craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain;
-        rustPkg = craneLib.buildPackage {
+        craneArgs = {
           src = craneLib.cleanCargoSource ./rust;
           strictDeps = true;
 
@@ -97,6 +106,18 @@
               pkgs.libiconv
             ];
         };
+        # Build dependencies once and share them across the package build and
+        # the clippy check instead of recompiling them per consumer.
+        cargoArtifacts = craneLib.buildDepsOnly craneArgs;
+        # doCheck = false: the crate has no Rust unit tests, and the Lean
+        # `blake3-test` check is where the suite runs.
+        rustPkg = craneLib.buildPackage (
+          craneArgs
+          // {
+            inherit cargoArtifacts;
+            doCheck = false;
+          }
+        );
 
         blake3C = lake2nix.mkPackage {
           name = "Blake3C";
@@ -142,7 +163,23 @@
         packages = {
           default = blake3C;
           rust = blake3Rust;
-          test = blake3Test;
+        };
+
+        checks = {
+          # Lint the Rust FFI crate; warnings are errors.
+          clippy = craneLib.cargoClippy (
+            craneArgs
+            // {
+              inherit cargoArtifacts;
+              cargoClippyExtraArgs = "--all-targets -- -D warnings";
+            }
+          );
+          # Run the Lean test suite (exercises both the C and Rust backends)
+          # at check time so it runs via `nix flake check`.
+          blake3-test = pkgs.runCommand "blake3-test" {} ''
+            ${blake3Test}/bin/Blake3Test
+            touch $out
+          '';
         };
         devShells.default = pkgs.mkShell {
           # Add libclang for FFI with rust-bindgen

lean-toolchain

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