Leni Aniva
75f14358cd
|
||
|---|---|---|
| Pantograph | ||
| Test | ||
| doc | ||
| .gitignore | ||
| LICENSE | ||
| Main.lean | ||
| Pantograph.lean | ||
| README.md | ||
| Repl.lean | ||
| Tomograph.lean | ||
| flake.lock | ||
| flake.nix | ||
| lake-manifest.json | ||
| lakefile.lean | ||
| lean-toolchain | ||
README.md
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
A Lean development shell is provided in the Nix flake. Nix usage is optional.
Testing
The tests are based on LSpec. To run tests, use either
nix flake check
or
lake test
You can run an individual test by specifying a prefix
lake test -- "Tactic/No Confuse"