Pantograph/flake.nix

97 lines
2.7 KiB
Nix
Raw Permalink Normal View History

2023-10-20 11:52:09 -07:00
{
description = "Pantograph";
inputs = {
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
flake-parts.url = "github:hercules-ci/flake-parts";
2024-03-28 11:33:15 -07:00
lean = {
2024-03-30 00:03:37 -07:00
# Do not follow input's nixpkgs since it could cause build failures
2024-07-06 19:53:50 -07:00
url = "github:leanprover/lean4?ref=v4.10.0-rc1";
2024-03-28 11:33:15 -07:00
};
lspec = {
2024-08-17 02:07:17 -07:00
url = "github:lurk-lab/LSpec?ref=8a51034d049c6a229d88dd62f490778a377eec06";
2024-03-28 11:33:15 -07:00
flake = false;
};
2023-10-20 11:52:09 -07:00
};
outputs = inputs @ {
self,
nixpkgs,
flake-parts,
lean,
2024-03-28 11:33:15 -07:00
lspec,
2023-10-20 11:52:09 -07:00
...
} : flake-parts.lib.mkFlake { inherit inputs; } {
flake = {
};
systems = [
"x86_64-linux"
"x86_64-darwin"
];
perSystem = { system, pkgs, ... }: let
leanPkgs = lean.packages.${system};
2024-03-28 11:33:15 -07:00
lspecLib = leanPkgs.buildLeanPackage {
name = "LSpec";
roots = [ "Main" "LSpec" ];
src = "${lspec}";
};
2023-10-20 11:52:09 -07:00
project = leanPkgs.buildLeanPackage {
name = "Pantograph";
roots = [ "Pantograph" ];
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
src = ./.;
filter = path: type:
!(pkgs.lib.hasInfix "/Test/" path) &&
!(pkgs.lib.hasSuffix ".md" path) &&
!(pkgs.lib.hasSuffix "Repl.lean" path);
});
};
repl = leanPkgs.buildLeanPackage {
name = "Repl";
roots = [ "Main" "Repl" ];
deps = [ project ];
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
src = ./.;
filter = path: type:
!(pkgs.lib.hasInfix "/Test/" path) &&
!(pkgs.lib.hasSuffix ".md" path);
});
2023-10-20 11:52:09 -07:00
};
2024-03-28 00:06:35 -07:00
test = leanPkgs.buildLeanPackage {
name = "Test";
2024-03-28 11:33:15 -07:00
# 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 repl ];
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
2024-03-28 11:33:15 -07:00
src = ./.;
filter = path: type:
!(pkgs.lib.hasInfix "Pantograph" path);
});
2024-03-28 00:06:35 -07:00
};
2023-10-20 11:52:09 -07:00
in rec {
2024-03-06 15:26:35 -08:00
packages = {
inherit (leanPkgs) lean lean-all;
inherit (project) sharedLib;
inherit (repl) executable;
default = repl.executable;
};
legacyPackages = {
inherit project leanPkgs;
};
2024-03-28 00:06:35 -07:00
checks = {
2024-03-28 11:33:15 -07:00
test = pkgs.runCommand "test" {
buildInputs = [ test.executable leanPkgs.lean-all ];
} ''
#export LEAN_SRC_PATH="${./.}"
${test.executable}/bin/test > $out
'';
2024-03-28 00:06:35 -07:00
};
2024-03-28 22:26:46 -07:00
devShells.default = pkgs.mkShell {
buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
};
2023-10-20 11:52:09 -07:00
};
};
}