Pantograph

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

Pantograph provides interfaces to execute proofs, construct expressions, and examine the symbol list of a Lean project for machine learning.

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.

Inject any project path via the pantograph_init_search function.

Development

See Contributing.