Pantograph/README.md

171 lines
6.1 KiB
Markdown
Raw Permalink Normal View History

2023-05-09 22:51:19 -07:00
# Pantograph
2024-03-28 22:09:56 -07:00
A Machine-to-Machine interaction system for Lean 4.
2023-05-09 22:51:19 -07:00
![Pantograph](doc/icon.svg)
2024-03-28 22:09:56 -07:00
Pantograph provides interfaces to execute proofs, construct expressions, and
examine the symbol list of a Lean project for machine learning.
2023-05-09 22:51:19 -07:00
## Installation
2024-03-28 11:37:07 -07:00
For Nix based workflow, see below.
Install `elan` and `lake`, and run
2023-05-09 22:51:19 -07:00
``` sh
lake build
2023-05-09 22:51:19 -07:00
```
2024-04-15 19:57:05 -07:00
This builds the executable in `.lake/build/bin/pantograph`.
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:
2023-05-12 01:08:36 -07:00
``` sh
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 $@
2023-05-12 01:08:36 -07:00
```
2024-04-15 19:57:05 -07:00
The `$LEAN_PATH` executable of any project can be extracted by
``` sh
lake env printenv LEAN_PATH
```
2023-05-09 22:51:19 -07:00
2024-03-28 11:37:07 -07:00
## Executable Usage
2023-05-09 22:51:19 -07:00
``` sh
2023-10-02 10:26:19 -07:00
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": ... }
```
2023-11-06 11:04:28 -08:00
The list of available commands can be found in `Pantograph/Protocol.lean` and below. An
empty command aborts the REPL.
2023-05-12 16:12:21 -07:00
2023-10-02 10:26:19 -07:00
The `pantograph` executable must be run with a list of modules to import. It can
2023-08-13 21:19:06 -07:00
also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
2023-05-12 16:12:21 -07:00
Example: (~5k symbols)
```
2023-10-02 10:26:19 -07:00
$ pantograph Init
env.catalog
env.inspect {"name": "Nat.le_add_left"}
2023-05-12 16:12:21 -07:00
```
Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
2023-05-12 01:08:36 -07:00
```
2023-10-02 10:26:19 -07:00
$ pantograph Mathlib.Analysis.Seminorm
env.catalog
2023-05-09 22:51:19 -07:00
```
2023-08-27 19:58:52 -07:00
Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
2023-05-21 17:41:39 -07:00
```
2023-10-02 10:26:19 -07:00
$ pantograph Init
2023-08-27 19:58:52 -07:00
goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
2023-11-06 11:04:28 -08:00
goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"}
goal.delete {"stateIds": [0]}
2023-08-27 19:58:52 -07:00
stat {}
2023-11-06 11:04:28 -08:00
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
2023-08-27 19:58:52 -07:00
stat
2023-05-21 17:41:39 -07:00
```
where the application of `assumption` should lead to a failure.
2023-05-09 22:51:19 -07:00
2024-03-28 11:37:07 -07:00
### Commands
2023-11-06 11:04:28 -08:00
See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
2024-04-15 19:57:05 -07:00
* `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.
2024-04-15 19:57:05 -07:00
* `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.
2024-04-15 19:57:05 -07:00
* `options.set { key: value, ... }`: Set one or more options (not Lean options; those
2023-11-06 11:04:28 -08:00
have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
2024-09-06 21:32:02 -07:00
One particular option for interest for machine learning researchers is the automatic mode.
`options.set { "automaticMode": true }`. This makes Pantograph act like
LeanDojo, with no resumption necessary to manage your goals.
2024-04-15 19:57:05 -07:00
* `options.print`: Display the current set of options
* `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
2024-04-15 19:57:05 -07:00
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> }`: Execute `have` and creates a branch goal
- `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
2024-04-15 19:57:05 -07:00
be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
to the previous `rhs`.
- `{ "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
2024-04-15 19:57:05 -07:00
* `goal.print {"stateId": <id>}"`: Print a goal state
2024-03-28 11:37:07 -07:00
### Errors
When an error pertaining to the execution of a command happens, the returning JSON structure is
``` json
2024-04-15 19:57:05 -07:00
{ "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.
2024-03-28 11:37:07 -07:00
### Troubleshooting
2023-05-09 22:51:19 -07:00
2023-05-14 15:22:41 -07:00
If lean encounters stack overflow problems when printing catalog, execute this before running lean:
```sh
ulimit -s unlimited
```
2024-03-28 11:37:07 -07:00
## Library Usage
`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
2024-03-28 22:09:56 -07:00
with `Pantograph` which mirrors the REPL commands above. It is recommended to
call Pantograph via this FFI since it provides a tremendous speed up.
## Developing
2024-03-28 11:37:07 -07:00
2024-04-15 19:57:05 -07:00
A Lean development shell is provided in the Nix flake.
2024-03-28 22:09:56 -07:00
### Testing
The tests are based on `LSpec`. To run tests,
``` sh
lake test
```
You can run an individual test by specifying a prefix
``` sh
lake test -- "Tactic/No Confuse"
```
2024-03-28 11:37:07 -07:00
## Nix based workflow
2024-03-28 22:09:56 -07:00
The included Nix flake provides build targets for `sharedLib` and `executable`.
The executable can be used as-is, but linking against the shared library
requires the presence of `lean-all`.
2024-03-28 11:37:07 -07:00
To run tests:
``` sh
nix flake check
2024-03-28 11:37:07 -07:00
```