chore: Update Lean to v4.31.0 (#79)

* feat: update to lean v4.31.0

* ci: Update Nix config

---------

Co-authored-by: Serhii Khoma <sergey@nordicresults.com>

Author: samuelburnham

.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

@@ -19,3 +19,22 @@ jobs:
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail"
+
+  # Builds the library and runs the test suite via Nix flake checks
+  nix-test:
+    name: Nix Tests
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: cachix/install-nix-action@v31
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+          github_access_token: ${{ secrets.GITHUB_TOKEN }}
+      - uses: cachix/cachix-action@v16
+        with:
+          name: argumentcomputer
+          authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+      # Build the library and test binary
+      - run: nix build --print-build-logs --accept-flake-config
+      # Run the test suite as a flake check
+      - run: nix flake check --print-build-logs --accept-flake-config

LSpec/LSpec.lean

@@ -95,7 +95,7 @@ instance (priority := 25) (p : Prop) [d : Decidable p] : Testable p :=
   | isTrue  h => .isTrue  h
 
 open SlimCheck in
-instance instTestableOfCheckable (p : Prop) (cfg : Configuration) [Checkable p] : Testable p :=
+abbrev instTestableOfCheckable (p : Prop) (cfg : Configuration) [Checkable p] : Testable p :=
   let ((res, numSamples), _) := ReaderT.run (Checkable.runSuite p cfg) (.up mkStdGen)
   match res with
   | .success (.inr h) => .isTrue h

flake.lock

@@ -1,6 +1,15 @@
 {
   description = "LSpec 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";
@@ -29,17 +38,35 @@
         ...
       }: let
         lake2nix = pkgs.callPackage lean4-nix.lake {};
+
+        # 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 = ./.;
+        };
+
+        # `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 = ./.;
+          lakeArtifacts = lspec;
+        };
       in {
         _module.args.pkgs = import nixpkgs {
           inherit system;
           overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
         };
 
         # Build the library with `nix build`
-        packages.default = lake2nix.mkPackage {
-          name = "LSpec";
-          src = ./.;
-        };
+        packages.default = lspec;
+
+        # Build and run the test suite as a flake check (`nix flake check`).
+        checks.tests = pkgs.runCommand "LSpec-tests" { } ''
+          ${lspecTest}/bin/tests
+          touch $out
+        '';
 
         devShells.default = pkgs.mkShell {
           packages = with pkgs.lean; [lean-all];

flake.nix

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