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
|
|
|
|
2023-06-09 14:45:45 -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-09-09 12:39:32 -07:00
|
|
|
For Nix users, run
|
2023-05-09 22:51:19 -07:00
|
|
|
``` sh
|
2024-09-09 12:39:32 -07:00
|
|
|
nix build .#{sharedLib,executable}
|
2023-05-09 22:51:19 -07:00
|
|
|
```
|
2024-09-09 12:39:32 -07:00
|
|
|
to build either the shared library or executable.
|
2024-04-15 19:57:05 -07:00
|
|
|
|
2024-09-09 12:39:32 -07:00
|
|
|
Install `elan` and `lake`, and run
|
2023-05-12 01:08:36 -07:00
|
|
|
``` sh
|
2024-09-09 12:39:32 -07:00
|
|
|
lake build
|
2024-04-15 19:57:05 -07:00
|
|
|
```
|
2024-09-09 12:39:32 -07:00
|
|
|
This builds the executable in `.lake/build/bin/pantograph-repl`.
|
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
|
|
|
|
2023-05-24 22:33:10 -07:00
|
|
|
``` sh
|
2023-10-02 10:26:19 -07:00
|
|
|
pantograph MODULES|LEAN_OPTIONS
|
2023-05-24 22:33:10 -07:00
|
|
|
```
|
|
|
|
|
|
|
|
The REPL loop accepts commands as single-line JSON inputs and outputs either an
|
2023-08-24 22:51:40 -07:00
|
|
|
`Error:` (indicating malformed command) or a JSON return value indicating the
|
2023-05-24 22:33:10 -07:00
|
|
|
result of a command execution. The command can be passed in one of two formats
|
2023-05-20 13:03:12 -07:00
|
|
|
```
|
|
|
|
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
|
2023-05-20 15:58:38 -07:00
|
|
|
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-23 05:12:46 -07:00
|
|
|
|
2023-05-12 16:12:21 -07:00
|
|
|
Example: (~5k symbols)
|
|
|
|
```
|
2023-10-02 10:26:19 -07:00
|
|
|
$ pantograph Init
|
2023-12-12 18:56:25 -08:00
|
|
|
env.catalog
|
|
|
|
env.inspect {"name": "Nat.le_add_left"}
|
2023-05-12 16:12:21 -07:00
|
|
|
```
|
2023-06-09 14:45:45 -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
|
2023-12-12 18:56:25 -08:00
|
|
|
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-12-05 15:59:07 -08:00
|
|
|
For a list of commands, see [REPL Documentation](doc/repl.md).
|
2023-08-24 22:51:40 -07:00
|
|
|
|
2024-09-09 12:39:32 -07:00
|
|
|
### 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:
|
|
|
|
|
|
|
|
``` 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 $@
|
|
|
|
```
|
|
|
|
The `$LEAN_PATH` executable of any project can be extracted by
|
|
|
|
``` sh
|
|
|
|
lake env printenv LEAN_PATH
|
|
|
|
```
|
|
|
|
|
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
|
|
|
|
```
|
2023-05-22 14:49:56 -07:00
|
|
|
|
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.
|
|
|
|
|
2024-09-09 12:39:32 -07:00
|
|
|
The executable can be used as-is, but linking against the shared library
|
2024-09-09 17:35:10 -07:00
|
|
|
requires the presence of `lean-all`. Note that there isn't a 1-1 correspondence
|
|
|
|
between executable (REPL) commands and library functions.
|
2024-09-09 12:39:32 -07:00
|
|
|
|
|
|
|
Inject any project path via the `pantograph_init_search` function.
|
|
|
|
|
2024-03-28 22:09:56 -07:00
|
|
|
## 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
|
2023-05-22 14:49:56 -07:00
|
|
|
|
2024-09-09 12:39:32 -07:00
|
|
|
The tests are based on `LSpec`. To run tests, use either
|
|
|
|
``` sh
|
|
|
|
nix flake check
|
|
|
|
```
|
|
|
|
or
|
2023-05-22 14:49:56 -07:00
|
|
|
``` sh
|
2024-08-18 12:22:59 -07:00
|
|
|
lake test
|
|
|
|
```
|
|
|
|
You can run an individual test by specifying a prefix
|
|
|
|
|
|
|
|
``` sh
|
|
|
|
lake test -- "Tactic/No Confuse"
|
2023-05-22 14:49:56 -07:00
|
|
|
```
|