From 1d1a151a4b2ccafb4897457fb09f857ffe9a9506 Mon Sep 17 00:00:00 2001 From: Leni Aniva 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 c5404b8210bb39b74030327d1c19efd3cbff9d72 Mon Sep 17 00:00:00 2001 From: Leni Aniva 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 bdb060b79f35663c26bbcf4ed4f3bf7d4025a201 Mon Sep 17 00:00:00 2001 From: Leni Aniva 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 ]; + }; }; }; }