From 5d0a7e84432aef08919767328afcc45c930232a1 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 8 Mar 2025 22:50:04 -0800
Subject: [PATCH 1/2] fix: Manifest key error
---
flake.nix | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/flake.nix b/flake.nix
index 424f863..71d957f 100644
--- a/flake.nix
+++ b/flake.nix
@@ -36,7 +36,7 @@
overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
};
manifest = pkgs.lib.importJSON ./lake-manifest.json;
- manifest-lspec = builtins.head manifest;
+ manifest-lspec = builtins.head manifest.packages;
lspecLib = pkgs.lean.buildLeanPackage {
name = "LSpec";
roots = ["LSpec"];
From 9e1ea54cbe0ad5d8527134d98033c123831d8148 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 8 Mar 2025 22:52:36 -0800
Subject: [PATCH 2/2] chore: Cleanup file filtering system
---
flake.nix | 57 ++++++++++++++++++++++++++++++++++++-------------------
1 file changed, 38 insertions(+), 19 deletions(-)
diff --git a/flake.nix b/flake.nix
index 71d957f..839ff9c 100644
--- a/flake.nix
+++ b/flake.nix
@@ -40,29 +40,52 @@
lspecLib = pkgs.lean.buildLeanPackage {
name = "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 {
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);
- });
+ src = src-project;
};
repl = pkgs.lean.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);
- });
+ src = src-repl;
};
test = pkgs.lean.buildLeanPackage {
name = "Test";
@@ -71,11 +94,7 @@
# Environment`) and thats where `lakefile.lean` resides.
roots = ["Test.Main"];
deps = [lspecLib repl];
- src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
- src = ./.;
- filter = path: type:
- !(pkgs.lib.hasInfix "Pantograph" path);
- });
+ src = src-test;
};
in rec {
packages = {