Leni Aniva d23f99fd44 | ||
---|---|---|
Pantograph | ||
Test | ||
doc | ||
.gitignore | ||
LICENSE | ||
Main.lean | ||
Pantograph.lean | ||
README.md | ||
Repl.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.
Installation
For Nix users, run
nix build .#{sharedLib,executable}
to build either the shared library or executable.
Install elan
and lake
, and run
lake build
This builds the executable in .lake/build/bin/pantograph-repl
.
Executable Usage
pantograph MODULES|LEAN_OPTIONS
The REPL loop accepts commands as single-line JSON inputs and outputs either an
Error:
(indicating malformed command) or a JSON return value indicating the
result of a command execution. The command can be passed in one of two formats
command { ... }
{ "cmd": command, "payload": ... }
The list of available commands can be found in Pantograph/Protocol.lean
and below. An
empty command aborts the REPL.
The pantograph
executable must be run with a list of modules to import. It can
also accept lean options of the form --key=value
e.g. --pp.raw=true
.
Example: (~5k symbols)
$ pantograph Init
env.catalog
env.inspect {"name": "Nat.le_add_left"}
Example with mathlib4
(~90k symbols, may stack overflow, see troubleshooting)
$ pantograph Mathlib.Analysis.Seminorm
env.catalog
Example proving a theorem: (alternatively use goal.start {"copyFrom": "Nat.add_comm"}
) to prime the proof
$ pantograph Init
goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"}
goal.delete {"stateIds": [0]}
stat {}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
stat
where the application of assumption
should lead to a failure.
Commands
See Pantograph/Protocol.lean
for a description of the parameters and return values in JSON.
-
reset
: Delete all cached expressions and proof trees -
stat
: Display resource usage -
expr.echo {"expr": <expr>, "type": <optional expected type>, ["levels": [<levels>]]}
: Determine the type of an expression and format it. -
env.catalog
: Display a list of all safe Lean symbols in the current environment -
env.inspect {"name": <name>, "value": <bool>}
: Show the type and package of a given symbol; If value flag is set, the value is printed or hidden. By default only the values of definitions are printed. -
options.set { key: value, ... }
: Set one or more options (not Lean options; those have to be set via command line arguments.), for options, seePantograph/Protocol.lean
One particular option for interest for machine learning researchers is the automatic mode (flag:
"automaticMode"
). By default it is turned on, with all goals automatically resuming. This makes Pantograph act like a gym, with no resumption necessary to manage your goals. -
options.print
: Display the current set of options -
goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}
: Start a new proof from a given expression or symbol -
goal.tactic {"stateId": <id>, "goalId": <id>, ...}
: Execute a tactic string on a given goal. The tactic is supplied as additional key-value pairs in one of the following formats:{ "tactic": <tactic> }
: Execute an ordinary tactic{ "expr": <expr> }
: Assign the given proof term to the current goal{ "have": <expr>, "binderName": <name> }
: Executehave
and creates a branch goal{ "calc": <expr> }
: Execute one step of acalc
tactic. Each step must be of the formlhs op rhs
. Anlhs
of_
indicates that it should be set to the previousrhs
.{ "conv": <bool> }
: Enter or exit conversion tactic mode. In the case of exit, the goal id is ignored.
-
goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}
: Execute continuation/resumption{ "branch": <id> }
: Continue on branch state. The current state must have no goals.{ "goals": <names> }
: Resume the given goals
-
goal.remove {"stateIds": [<id>]}"
: Drop the goal states specified in the list -
goal.print {"stateId": <id>}"
: Print a goal state -
frontend.process { ["fileName": <fileName>",] ["file": <str>], invocations: <bool>, sorrys: <bool> }
: Executes the Lean frontend on a file, collecting either the tactic invocations ("invocations": true
) or the sorrys into goal states ("sorrys": true
)
Errors
When an error pertaining to the execution of a command happens, the returning JSON structure is
{ "error": "type", "desc": "description" }
Common error forms:
command
: Indicates malformed command structure which results from either invalid command or a malformed JSON structure that cannot be fed to an individual command.index
: Indicates an invariant maintained by the output of one command and input of another is broken. For example, attempting to query a symbol not existing in the library or indexing into a non-existent proof state.
Project Environment
To use Pantograph in a project environment, setup the LEAN_PATH
environment
variable so it contains the library path of lean libraries. The libraries must
be built in advance. For example, if mathlib4
is stored at ../lib/mathlib4
,
the environment might be setup like this:
LIB="../lib"
LIB_MATHLIB="$LIB/mathlib4/lake-packages"
export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
The $LEAN_PATH
executable of any project can be extracted by
lake env printenv LEAN_PATH
Troubleshooting
If lean encounters stack overflow problems when printing catalog, execute this before running lean:
ulimit -s unlimited
Library Usage
Pantograph/Library.lean
exposes a series of interfaces which allow FFI call
with Pantograph
which mirrors the REPL commands above. It is recommended to
call Pantograph via this FFI since it provides a tremendous speed up.
The executable can be used as-is, but linking against the shared library
requires the presence of lean-all
. 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.
Developing
A Lean development shell is provided in the Nix flake.
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"