repl.md

REPL

This documentation is about interacting with the REPL.

Examples

After building the repl, it will be available in .lake/build/bin/repl. Execute it by either directly referring to its name, or lake exe repl.

repl MODULES|LEAN_OPTIONS

The repl executable must be given with a list of modules to import. By default it will import nothing, not even Init. It can also accept lean options of the form --key=value e.g. --pp.raw=true.

Running repl with --version shows the version and then exits.

After it emits the ready. signal, repl 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 must be given in one of two formats

command { ... }
{ "cmd": command, "payload": ... }

The list of available commands can be found below. An empty command aborts the REPL.

Example: (~5k symbols)

$ repl Init
env.catalog {}
env.inspect {"name": "Nat.le_add_left"}

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

$ repl Mathlib.Analysis.Seminorm
env.catalog {}

Example proving a theorem: (alternatively use goal.start {"copyFrom": "Nat.add_comm"}) to prime the proof

$ repl Init
goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
goal.tactic {"stateId": 0, "tactic": "intro n m"}
goal.tactic {"stateId": 1, "tactic": "assumption"}
goal.delete {"stateIds": [0]}
stat {}
goal.tactic {"stateId": 1, "tactic": "rw [Nat.add_comm]"}
stat

where the application of assumption should lead to a failure.

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:

LIB="../lib"
LIB_MATHLIB="$LIB/mathlib4/.lake"
export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"

LEAN_PATH=$LEAN_PATH repl $@

The $LEAN_PATH executable of any project can be extracted by

lake env printenv LEAN_PATH

Additional modules cannot be imported after the perennial process starts, either via env.load or the frontend functions. The technical reason for this is when Lean cannot determine whether an imported module's initializer has run.

Commands

See Pantograph/Protocol.lean for a description of the parameters and return values in JSON.

• reset: Delete all cached expressions and proof trees

• stat: Display resource usage

• options.set { key: value, ... }: Set one or more options. These are not Lean CoreM options; those have to be set via command line arguments.), for options see below.

• options.print: Display the current set of options

• expr.echo {"expr": <expr>, "type": <optional expected type>, ["levels": [<levels>]]}: Determine the type of an expression and format 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.

• env.save { "path": <fileName> }, env.load { "path": <fileName> }: Save/Load the current environment to/from a file

• env.module_read { "module": <name> }: Reads a list of symbols from a module

• env.describe {}: Describes the imports and modules in the current environment

• env.parse { "input": <input>, "category": <parser-category> }: Parse a bit of syntax and returns the parser's terminal position.

• goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}: Start a new proof from a given expression or symbol

• goal.tactic {"stateId": <id>, ["goalId": <id>], ["autoResume": <bool>], ...}: Execute a tactic string on a given goal site. The tactic is supplied as additional key-value pairs in one of the following formats:

  • { "tactic": <tactic> }: Executes a tactic or a sequence of tactics in the current mode.
  • { "mode": <mode> }: Enter a different tactic mode. The permitted values are tactic (default), conv, calc. In case of calc, each step must be of the form lhs op rhs. An lhs of _ indicates that it should be set to the previous rhs.
  • { "expr": <expr> }: Assign the given proof term to the current goal
  • { "have": <expr>, "binderName": <name> }: Execute have and creates a branch goal
  • { "let": <expr>, "binderName": <name> }: Execute let and creates a branch goal
  • { "draft": <expr> }: Draft an expression with sorrys, turning them into goals. Coupling is not allowed. If the goals field does not exist, the tactic execution has failed. Read messages to find the reason.

• 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.subsume {"stateId": <id>, "goal": <name>, "candidates": <names>, ["srcStateId": <id>]}: determine if any goal in candidates (coming from either the provided state id or srcStateId) subsumes goal. It returns the subsumptor (goal providing the solution) and a new state id if the subsumption is not a cycle, in which case the subsumend goal is erased.

• goal.remove {"stateIds": [<id>]}": Drop the goal states specified in the list

• goal.print {"stateId": <id>}": Print a goal state

• goal.save { "id": <id>, "path": <fileName> }, goal.load { "path": <fileName> }: Save/Load a goal state to/from a file. The environment is not carried with the state. The user is responsible to ensure the sender/receiver instances share the same environment.

• frontend.process { ["fileName": <fileName>,] ["file": <str>], readHeader: <bool>, inheritEnv: <bool>, invocations: <string>, newConstants: <bool> }: Executes the Lean frontend on a file, collecting the tactic invocations ("invocations": output-path), or new constants (newConstants)

• frontend.distil { "file": <str>, ["binderName": <str>], "ignoreValues": bool }: Extract condensed search targets from a file, where coupled search targets will be condensed into one. Set binderName to override the binder name to e.g. f. Set ignoreValues to false to incorporate existing solutions.

  Note that examples are not search targets!

• frontend.track { "src": <str>, "dst": <str> }: Check if one file conforms to another. The declarations in src could have sorrys and the declarations in dst would fill them.

• [Experimental] frontend.refactor { "file": <str>, "coreOptions": [["<key>=<val>"]] }: Group dependent sorrys into one single sorry. Currently only flat dependencies are supported (i.e. an object with a list of properties).

Options

The full list of options can be found in Pantograph/Protocol.lean. Particularly:

• automaticMode (default on): Goals will not become dormant when this is turned on. By default it is turned on, with all goals automatically resuming. This makes Pantograph act like a gym, with no resumption necessary to manage your goals.
• timeout (default 0): Set timeout to a non-zero number to specify timeout (milliseconds) for all CoreM and frontend operations.

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.
• parse: Indicates parsing errors
• elab: Indicates elaboration errors
• frontend: Indicates whole-file parsing and elaboration errors
• io: Generic IO error
• command: The command's argument is malformed

Troubleshooting

If lean encounters stack overflow problems when printing catalog, execute this before running lean:

ulimit -s unlimited