Compare commits
No commits in common. "1dceb5428eeb2a0c8995849ea06bd35dd6a12f35" and "4f5dd97e554571bd6aed12cb103ee0c6f008cad4" have entirely different histories.
1dceb5428e
...
4f5dd97e55
57
flake.nix
57
flake.nix
|
@ -36,56 +36,33 @@
|
||||||
overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
|
overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
|
||||||
};
|
};
|
||||||
manifest = pkgs.lib.importJSON ./lake-manifest.json;
|
manifest = pkgs.lib.importJSON ./lake-manifest.json;
|
||||||
manifest-lspec = builtins.head manifest.packages;
|
manifest-lspec = builtins.head manifest;
|
||||||
lspecLib = pkgs.lean.buildLeanPackage {
|
lspecLib = pkgs.lean.buildLeanPackage {
|
||||||
name = "LSpec";
|
name = "LSpec";
|
||||||
roots = ["LSpec"];
|
roots = ["LSpec"];
|
||||||
src = builtins.fetchGit { inherit (manifest-lspec) url rev; };
|
src = builtins.fetchGit { inherit (manifest-lspec) url rev; };
|
||||||
};
|
};
|
||||||
inherit (pkgs.lib.fileset) unions toSource fileFilter;
|
|
||||||
src = ./.;
|
|
||||||
set-project = unions [
|
|
||||||
./Pantograph.lean
|
|
||||||
(fileFilter (file: file.hasExt "lean") ./Pantograph)
|
|
||||||
];
|
|
||||||
set-repl = unions [
|
|
||||||
./Main.lean
|
|
||||||
./Repl.lean
|
|
||||||
];
|
|
||||||
set-test = unions [
|
|
||||||
(fileFilter (file: file.hasExt "lean") ./Test)
|
|
||||||
];
|
|
||||||
src-project = toSource {
|
|
||||||
root = src;
|
|
||||||
fileset = unions [
|
|
||||||
set-project
|
|
||||||
];
|
|
||||||
};
|
|
||||||
src-repl = toSource {
|
|
||||||
root = src;
|
|
||||||
fileset = unions [
|
|
||||||
set-project
|
|
||||||
set-repl
|
|
||||||
];
|
|
||||||
};
|
|
||||||
src-test = toSource {
|
|
||||||
root = src;
|
|
||||||
fileset = unions [
|
|
||||||
set-project
|
|
||||||
set-repl
|
|
||||||
set-test
|
|
||||||
];
|
|
||||||
};
|
|
||||||
project = pkgs.lean.buildLeanPackage {
|
project = pkgs.lean.buildLeanPackage {
|
||||||
name = "Pantograph";
|
name = "Pantograph";
|
||||||
roots = ["Pantograph"];
|
roots = ["Pantograph"];
|
||||||
src = src-project;
|
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 = pkgs.lean.buildLeanPackage {
|
repl = pkgs.lean.buildLeanPackage {
|
||||||
name = "Repl";
|
name = "Repl";
|
||||||
roots = ["Main" "Repl"];
|
roots = ["Main" "Repl"];
|
||||||
deps = [project];
|
deps = [project];
|
||||||
src = src-repl;
|
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
||||||
|
src = ./.;
|
||||||
|
filter = path: type:
|
||||||
|
!(pkgs.lib.hasInfix "/Test/" path)
|
||||||
|
&& !(pkgs.lib.hasSuffix ".md" path);
|
||||||
|
});
|
||||||
};
|
};
|
||||||
test = pkgs.lean.buildLeanPackage {
|
test = pkgs.lean.buildLeanPackage {
|
||||||
name = "Test";
|
name = "Test";
|
||||||
|
@ -94,7 +71,11 @@
|
||||||
# Environment`) and thats where `lakefile.lean` resides.
|
# Environment`) and thats where `lakefile.lean` resides.
|
||||||
roots = ["Test.Main"];
|
roots = ["Test.Main"];
|
||||||
deps = [lspecLib repl];
|
deps = [lspecLib repl];
|
||||||
src = src-test;
|
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
||||||
|
src = ./.;
|
||||||
|
filter = path: type:
|
||||||
|
!(pkgs.lib.hasInfix "Pantograph" path);
|
||||||
|
});
|
||||||
};
|
};
|
||||||
in rec {
|
in rec {
|
||||||
packages = {
|
packages = {
|
||||||
|
|
Loading…
Reference in New Issue