From 4a89aaf70eecff007a4622fabb3481f4e7fa4e62 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 28 Mar 2024 22:09:56 -0700
Subject: [PATCH 1/3] doc: Main README.md

---
 README.md | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index c845b89..cde0807 100644
--- a/README.md
+++ b/README.md
@@ -1,9 +1,12 @@
 # Pantograph
 
-An interaction system for Lean 4.
+A Machine-to-Machine 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.
@@ -109,9 +112,12 @@ ulimit -s unlimited
 ## Library Usage
 
 `Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
-with `Pantograph`.
+with `Pantograph` which mirrors the REPL commands above. It is recommended to
+call Pantograph via this FFI since it provides a tremendous speed up.
 
-## Testing
+## Developing
+
+### Testing
 
 The tests are based on `LSpec`. To run tests,
 ``` sh
@@ -120,6 +126,10 @@ 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

From 4a1114ab00c8d1b8e33c8acf2a0e810c0323a2c5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 28 Mar 2024 22:23:19 -0700
Subject: [PATCH 2/3] build: Ignore test files when building target

---
 flake.nix | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/flake.nix b/flake.nix
index 539d391..df63845 100644
--- a/flake.nix
+++ b/flake.nix
@@ -39,7 +39,13 @@
         name = "Pantograph";
         #roots = pkgs.lib.optional pkgs.stdenv.isDarwin [ "Main" "Pantograph" ];
         roots = [ "Main" "Pantograph" ];
-        src = ./.;
+        src = pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "/Test/" path) &&
+            !(pkgs.lib.hasSuffix ".md" path) &&
+            !(pkgs.lib.hasSuffix "Makefile" path);
+        };
       };
       test = leanPkgs.buildLeanPackage {
         name = "Test";
@@ -58,7 +64,6 @@
       packages = {
         inherit (leanPkgs) lean lean-all;
         inherit (project) sharedLib executable;
-        test = test.executable;
         default = project.executable;
       };
       checks = {

From cfd74aba918cd5d77a52fdc8768506b8c7a6cb9e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 28 Mar 2024 22:26:46 -0700
Subject: [PATCH 3/3] build: Dev shell

---
 flake.nix | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/flake.nix b/flake.nix
index df63845..fdb3f6b 100644
--- a/flake.nix
+++ b/flake.nix
@@ -37,7 +37,6 @@
       };
       project = leanPkgs.buildLeanPackage {
         name = "Pantograph";
-        #roots = pkgs.lib.optional pkgs.stdenv.isDarwin [ "Main" "Pantograph" ];
         roots = [ "Main" "Pantograph" ];
         src = pkgs.lib.cleanSourceWith {
           src = ./.;
@@ -74,7 +73,9 @@
           ${test.executable}/bin/test > $out
         '';
       };
-      devShells.default = project.devShell;
+      devShells.default = pkgs.mkShell {
+        buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
+      };
     };
   };
 }