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

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.