pantograph

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

Pantograph provides interfaces to interact with Lean's frontend, execute proofs, construct expressions, and examining the Lean environment.

See documentations for design rationale and references.

Installation

For Nix users, run

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

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

Another executable is the tomograph, which processes a Lean file and displays syntax or elaboration level data.

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.

Inject any project path via the pantograph_init_search function.

Development

See Contributing.

Testing

The tests are based on LSpec. To run tests, use either

nix flake check

lake test

You can run an individual test suite by specifying a prefix

lake test -- "Library/my_test"