A Lean Machine-to-Machine Interface
Go to file
Leni Aniva 01a23b338a
feat: Unfold aux lemmas when printing root expr
2024-03-28 18:56:42 -07:00
Pantograph feat: Unfold aux lemmas when printing root expr 2024-03-28 18:56:42 -07:00
Test feat: Unfold aux lemmas when printing root expr 2024-03-28 18:56:42 -07:00
doc Add documentation; Remove mathlib dependency 2023-06-09 14:45:45 -07:00
.gitignore Bump Lean version to 4.1.0 2023-10-05 17:49:43 -07:00
Main.lean feat(lib): Search path function 2024-03-09 19:36:25 -08:00
Makefile chore: Lean version bump to 4.7.0-rc2 2024-03-15 06:01:25 -07:00
Pantograph.lean feat(lib): Export goal.print function 2024-03-14 16:34:01 -07:00
README.md doc: Update README.md 2024-03-28 11:37:07 -07:00
flake.lock build: Nix build targets and checks 2024-03-28 11:33:15 -07:00
flake.nix build: Nix build targets and checks 2024-03-28 11:33:15 -07:00
lake-manifest.json chore: Lean version bump to 4.7.0-rc2 2024-03-15 06:01:25 -07:00
lakefile.lean chore: Lean version bump to 4.7.0-rc2 2024-03-15 06:01:25 -07:00
lean-toolchain feat: Bump toolchain version 2024-03-28 00:06:35 -07:00

README.md

Pantograph

An interaction system for Lean 4.

Pantograph

Installation

For Nix based workflow, see below.

Install elan and lake. Execute

make build/bin/pantograph

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,

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 provided flake.nix has a develop environment with Lean already setup.

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
  • expr.echo {"expr": <expr>}: Determine the type of an expression and round-trip 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, see Pantograph/Protocol.lean
  • options.print: Display the current set of options
  • goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}: Start a new goal from a given expression or symbol
  • goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}: Execute a tactic string on a given goal
  • goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}: Continue from a proof state
  • goal.remove {"stateIds": [<id>]}": Remove a bunch of stored goals.
  • goal.print {"stateId": <id>}": Print a goal state
  • stat: Display resource usage

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.

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.

Testing

The tests are based on LSpec. To run tests,

make test

Nix based workflow

To run tests:

nix build .#checks.${system}.test

For example, ${system} could be x86_64-linux. Using nix develop drops the current session into a development shell with fixed Lean version.