|
|
||
|---|---|---|
| doc | ||
| Pantograph | ||
| Test | ||
| .gitignore | ||
| flake.lock | ||
| flake.nix | ||
| lake-manifest.json | ||
| lakefile.lean | ||
| lean-toolchain | ||
| LICENSE | ||
| Main.lean | ||
| Pantograph.lean | ||
| README.md | ||
| Repl.lean | ||
| Tomograph.lean | ||
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.