A Lean Machine-to-Machine Interface
Go to file
Leni Aniva 538ba6e7d7 Store states instead of goals
1. Rename {Commands, Protocol}, and {Symbols, Symbol}
2. Store the root mvarId in the proof state along with goal indices
3. Add diagnostics function which prints out the state
4. Bump version to 0.2.6 (breaking change)

Documentations pending
2023-10-15 17:15:23 -07:00
Pantograph Store states instead of goals 2023-10-15 17:15:23 -07:00
Test Store states instead of goals 2023-10-15 17:15:23 -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 Store states instead of goals 2023-10-15 17:15:23 -07:00
Makefile Rename tactic to goal and restructure 2023-10-15 12:31:22 -07:00
Pantograph.lean Store states instead of goals 2023-10-15 17:15:23 -07:00
README.md Use makefile instead of ad-hoc script 2023-10-02 10:26:19 -07:00
lake-manifest.json Bump lean version to 4.0.0 2023-09-13 21:02:26 -07:00
lakefile.lean Add documentation; Remove mathlib dependency 2023-06-09 14:45:45 -07:00
lean-toolchain Bump Lean version to 4.1.0 2023-10-05 17:49:43 -07:00

README.md

Pantograph

An interaction system for Lean 4.

Pantograph

Installation

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 $@

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/Commands.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
lib.catalog
lib.inspect {"name": "Nat.le_add_left"}

Example with mathlib4 (~90k symbols, may stack overflow, see troubleshooting)

$ pantograph Mathlib.Analysis.Seminorm
lib.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 {"goalId": 0, "tactic": "intro n m"}
goal.tactic {"goalId": 1, "tactic": "assumption"}
goal.delete {"goalIds": [0]}
stat {}
goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"}
stat

where the application of assumption should lead to a failure.

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
  • 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.
  • 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

Testing

The tests are based on LSpec. To run tests,

make test