flake.lock

@@ -38,7 +38,9 @@
         "flake-utils": "flake-utils",
         "lean4-mode": "lean4-mode",
         "nix": "nix",
-        "nixpkgs": "nixpkgs_2",
+        "nixpkgs": [
+          "nixpkgs"
+        ],
         "nixpkgs-old": "nixpkgs-old"
       },
       "locked": {
@@ -88,6 +90,23 @@
         "type": "github"
       }
     },
+    "lspec": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1701971219,
+        "narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=",
+        "owner": "lurk-lab",
+        "repo": "LSpec",
+        "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+        "type": "github"
+      },
+      "original": {
+        "owner": "lurk-lab",
+        "ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+        "repo": "LSpec",
+        "type": "github"
+      }
+    },
     "nix": {
       "inputs": {
         "lowdown-src": "lowdown-src",
@@ -176,22 +195,6 @@
       }
     },
     "nixpkgs_2": {
-      "locked": {
-        "lastModified": 1686089707,
-        "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixpkgs-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "nixpkgs_3": {
       "locked": {
         "lastModified": 1697456312,
         "narHash": "sha256-roiSnrqb5r+ehnKCauPLugoU8S36KgmWraHgRqVYndo=",
@@ -211,7 +214,8 @@
       "inputs": {
         "flake-parts": "flake-parts",
         "lean": "lean",
-        "nixpkgs": "nixpkgs_3"
+        "lspec": "lspec",
+        "nixpkgs": "nixpkgs_2"
       }
     }
   },

flake.nix

@@ -4,7 +4,14 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean.url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
+    lean = {
+      url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
+    lspec = {
+      url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
+      flake = false;
+    };
   };
 
   outputs = inputs @ {
@@ -12,6 +19,7 @@
     nixpkgs,
     flake-parts,
     lean,
+    lspec,
     ...
   } : flake-parts.lib.mkFlake { inherit inputs; } {
     flake = {
@@ -22,24 +30,44 @@
     ];
     perSystem = { system, pkgs, ... }: let
       leanPkgs = lean.packages.${system};
+      lspecLib = leanPkgs.buildLeanPackage {
+        name = "LSpec";
+        roots = [ "Main" "LSpec" ];
+        src = "${lspec}";
+      };
       project = leanPkgs.buildLeanPackage {
         name = "Pantograph";
+        #roots = pkgs.lib.optional pkgs.stdenv.isDarwin [ "Main" "Pantograph" ];
         roots = [ "Main" "Pantograph" ];
         src = ./.;
       };
       test = leanPkgs.buildLeanPackage {
         name = "Test";
-        roots = [ "Main" ];
-        src = ./Test;
+        # NOTE: The src directory must be ./. since that is where the import
+        # root begins (e.g. `import Test.Environment` and not `import
+        # Environment`) and thats where `lakefile.lean` resides.
+        roots = [ "Test.Main" ];
+        deps = [ lspecLib project ];
+        src = pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "Pantograph" path);
+        };
       };
     in rec {
       packages = {
         inherit (leanPkgs) lean lean-all;
         inherit (project) sharedLib executable;
+        test = test.executable;
         default = project.executable;
       };
       checks = {
-        test = test.executable;
+        test = pkgs.runCommand "test" {
+          buildInputs = [ test.executable leanPkgs.lean-all ];
+        } ''
+          #export LEAN_SRC_PATH="${./.}"
+          ${test.executable}/bin/test > $out
+        '';
       };
       devShells.default = project.devShell;
     };