README.md

@@ -1,12 +1,9 @@
 # Pantograph
 
-A Machine-to-Machine interaction system for Lean 4.
+An interaction system for Lean 4.
 
 ![Pantograph](doc/icon.svg)
 
-Pantograph provides interfaces to execute proofs, construct expressions, and
-examine the symbol list of a Lean project for machine learning.
-
 ## Installation
 
 For Nix based workflow, see below.
@@ -112,12 +109,9 @@ ulimit -s unlimited
 ## Library Usage
 
 `Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
-with `Pantograph` which mirrors the REPL commands above. It is recommended to
+with `Pantograph`.
-call Pantograph via this FFI since it provides a tremendous speed up.
 
-## Developing
+## Testing
-
-### Testing
 
 The tests are based on `LSpec`. To run tests,
 ``` sh
@@ -126,10 +120,6 @@ make test
 
 ## Nix based workflow
 
-The included Nix flake provides build targets for `sharedLib` and `executable`.
-The executable can be used as-is, but linking against the shared library
-requires the presence of `lean-all`.
-
 To run tests:
 ``` sh
 nix build .#checks.${system}.test

flake.nix

@@ -37,14 +37,9 @@
       };
       project = leanPkgs.buildLeanPackage {
         name = "Pantograph";
+        #roots = pkgs.lib.optional pkgs.stdenv.isDarwin [ "Main" "Pantograph" ];
         roots = [ "Main" "Pantograph" ];
-        src = pkgs.lib.cleanSourceWith {
+        src = ./.;
-          src = ./.;
-          filter = path: type:
-            !(pkgs.lib.hasInfix "/Test/" path) &&
-            !(pkgs.lib.hasSuffix ".md" path) &&
-            !(pkgs.lib.hasSuffix "Makefile" path);
-        };
       };
       test = leanPkgs.buildLeanPackage {
         name = "Test";
@@ -63,6 +58,7 @@
       packages = {
         inherit (leanPkgs) lean lean-all;
         inherit (project) sharedLib executable;
+        test = test.executable;
         default = project.executable;
       };
       checks = {
@@ -73,9 +69,7 @@
           ${test.executable}/bin/test > $out
         '';
       };
-      devShells.default = pkgs.mkShell {
+      devShells.default = project.devShell;
-        buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
-      };
     };
   };
 }