From 1d1a151a4b2ccafb4897457fb09f857ffe9a9506 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 22:09:56 -0700 Subject: [PATCH] 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