Compare commits

..

No commits in common. "1dceb5428eeb2a0c8995849ea06bd35dd6a12f35" and "4f5dd97e554571bd6aed12cb103ee0c6f008cad4" have entirely different histories.

1 changed files with 20 additions and 39 deletions

View File

@ -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 = {