# Pantograph

A Machine-to-Machine interaction system for Lean 4.

![Pantograph](doc/icon.svg)

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).