build: Toolchain bump and Nix flake fix #49
40
flake.lock
40
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"
|
||||
}
|
||||
}
|
||||
},
|
||||
|
|
36
flake.nix
36
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;
|
||||
};
|
||||
|
|
Loading…
Reference in New Issue