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 ed2d0f9..27cbb6a 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/LSpec/LSpec.lean b/LSpec/LSpec.lean index 7d91d2e..614fcb3 100644 --- a/LSpec/LSpec.lean +++ b/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 diff --git a/flake.lock b/flake.lock index c13bdc8..584ef4f 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1775087534, - "narHash": "sha256-91qqW8lhL7TLwgQWijoGBbiD4t7/q75KTi8NxjVmSmA=", + "lastModified": 1778716662, + "narHash": "sha256-m1Yf0wZ8j1OHjTc2UwHwyQRSnNeSgLJOd7q5Y45hzi4=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "3107b77cd68437b9a76194f0f7f9c55f2329ca5b", + "rev": "f7c1a2d347e4c52d5fb8d10cb4d94b5884e546fb", "type": "github" }, "original": { @@ -42,11 +42,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": { @@ -73,11 +73,11 @@ }, "nixpkgs-lib": { "locked": { - "lastModified": 1774748309, - "narHash": "sha256-+U7gF3qxzwD5TZuANzZPeJTZRHS29OFQgkQ2kiTJBIQ=", + "lastModified": 1777168982, + "narHash": "sha256-GOkGPcboWE9BmGCRMLX3worL4EMnsnG8MyKmXNeYuhQ=", "owner": "nix-community", "repo": "nixpkgs.lib", - "rev": "333c4e0545a6da976206c74db8773a1645b5870a", + "rev": "f5901329dade4a6ea039af1433fb087bd9c1fe14", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 3ea0dea..4a4fe29 100644 --- a/flake.nix +++ b/flake.nix @@ -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,6 +38,21 @@ ... }: 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; @@ -36,10 +60,13 @@ }; # 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]; 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