max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix Nix setup (leanprover/lake#38)

Browse source
This commit is contained in:
Anders Christiansen Sørby 2021-12-10 23:59:56 +01:00 • committed by GitHub
parent 0555e29808
commit bec311bf48
1 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
flake.nix
View file

@ -28,16 +28,20 @@
name = packageName;
inherit src;
};
cli = leanPkgs.buildLeanPackage {
name = "Lake.Main";
deps = [ project ];
inherit src;
};
in
{
packages.${packageName} = project.lean-package;
packages.lakeProject = project;
packages.${packageName} = project;
packages.cli = cli.executable;
defaultPackage = self.packages.${system}.${packageName};
defaultPackage = self.packages.${system}.cli;
apps.lake = flake-utils.lib.mkApp {
name = "lake";
drv = project.executable;
drv = cli.executable;
};
defaultApp = self.apps.${system}.lake;
@ -47,6 +51,7 @@
buildInputs = with pkgs; [
leanPkgs.lean
];
LEAN_PATH = "${leanPkgs.Lean.modRoot}:${project.modRoot}";
};
});
}