Pantograph/README.md

111 lines
3.9 KiB
Markdown
Raw Permalink Normal View History

2023-05-09 22:51:19 -07:00
# Pantograph
An interaction system for Lean 4.
![Pantograph](doc/icon.svg)
2023-05-09 22:51:19 -07:00
## Installation
Install `elan` and `lean4`. Then, execute
``` sh
lake build
```
Then, 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`,
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
```
Note that `lean-toolchain` must be present in the `$PWD` in order to run Pantograph! This is because Pantograph taps into Lean's internals.
2023-05-09 22:51:19 -07:00
## Usage
``` sh
2023-08-13 21:19:06 -07:00
build/bin/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/Commands.lean` and below. An
empty command aborts the REPL.
2023-05-12 16:12:21 -07:00
2023-05-24 00:55:54 -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)
```
$ build/bin/Pantograph Init
lib.catalog
lib.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
```
$ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm
lib.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
```
$ env build/bin/Pantograph Init
2023-08-27 19:58:52 -07:00
goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
goal.tactic {"goalId": 0, "tactic": "intro n m"}
goal.tactic {"goalId": 1, "tactic": "assumption"}
goal.delete {"goalIds": [0]}
2023-08-27 19:58:52 -07:00
stat {}
goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"}
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
## Commands
See `Pantograph/Commands.lean` for a description of the parameters and return values in JSON.
- `reset`: Delete all cached expressions and proof trees
- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
- `lib.catalog`: Display a list of all safe Lean symbols in the current context
- `lib.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, see `Pantograph/Commands.lean`
- `options.print`: Display the current set of options
2023-08-27 19:58:52 -07:00
- `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
- `goal.tactic {"goalId": <id>, "tactic": <tactic>}`: Execute a tactic string on a given goal
- `goal.remove {"goalIds": [<id>]}"`: Remove a bunch of stored goals.
2023-08-27 19:58:52 -07:00
- `stat`: Display resource usage
## Errors
When an error pertaining to the execution of a command happens, the returning JSON structure is
``` json
{ 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.
2023-05-14 15:22:41 -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
```
## Testing
The tests are based on `LSpec`. To run tests,
``` sh
test/all.sh
```