| # Pantograph |
|
|
| A Machine-to-Machine interaction system for Lean 4. |
|
|
|  |
|
|
| Pantograph provides interfaces to interact with Lean's frontend, execute proofs, |
| construct expressions, and examine the Lean environment. |
|
|
| See [documentations](doc/rationale.md) for design rationale and references. |
|
|
| ## Installation |
|
|
| For Nix users, run |
| ``` sh |
| nix build .#{sharedLib,executable} |
| ``` |
| to build either the shared library or executable. |
|
|
| For non-Nix users, install `lake` and `lean` fixed to the version of the |
| `lean-toolchain` file, and run |
|
|
| ``` sh |
| lake build |
| ``` |
| This builds the executable in `.lake/build/bin/repl`. |
|
|
| ### Executable Usage |
|
|
| The default build target is a Read-Eval-Print-Loop (REPL). See [REPL |
| Documentation](./doc/repl.md) |
|
|
| Another executable is the `tomograph`, which processes a Lean file and displays |
| syntax or elaboration level data. |
|
|
| ### Library Usage |
|
|
| `Pantograph/Library.lean` exposes a series of interfaces which allow FFI call |
| with `Pantograph` which mirrors the REPL commands above. Note that there isn't a |
| 1-1 correspondence between executable (REPL) commands and library functions. |
|
|
| ## Development |
|
|
| See [Contributing](./doc/contributing.md). |
|
|
