Lean 4 REPL

In command mode, you send complete Lean commands (such as declarations) using a JSON object with a cmd key.

To maintain state across commands, include the env field in your request. The env value must be the numeric label received in the env field of a previous response. If the env field is omitted, a new environment is created. Note that import commands can only be used when no env field is specified.

Response Fields:

• env: A numeric label for the Environment after your command.
• messages: A list of messages (errors, warnings, etc.) generated during processing.
• sorries: A list of sorry locations in the command, including their expected type and a proofState numeric label used for Tactic mode.

{ "cmd" : "def f := 2" }

{ "cmd" : "example : f = 2 := rfl", "env" : 1 }

Tactic mode allows you to interactively solve goals generated by sorry.

Workflow:

1. Issue a command containing a sorry in Command mode.
2. Identify the proofState index returned in the response for that sorry.
3. Send a JSON object with the tactic key and the corresponding proofState index to apply a tactic.
4. The REPL will return the new proofState and the updated goals.

Note: Currently, you cannot replace the original sorry with the tactic script to obtain a new Environment.

// 1. Start with a sorry
{"cmd" : "def f (x : Unit) : Nat := by sorry"}

// 2. Use the returned proofState (e.g., 0) to apply a tactic
{"tactic": "apply Int.natAbs", "proofState": 0}

// 3. Continue with the next proofState
{"tactic": "exact -37", "proofState": 1}

To use the REPL within a different Lean project (e.g., one that depends on Mathlib), use lake env to ensure the REPL inherits the project's environment and dependencies.

Run the command by pointing to the compiled REPL binary in the repl repository's .lake/build/bin/ directory.

lake env ../path/to/repl/.lake/build/bin/repl < commands.in

The REPL supports saving (pickling) environments and proof states to disk as .olean files. This allows you to move sessions between machines, provided the same imports are available.

Commands:

• {"pickleTo": "path/to/file.olean", "env": <number>}: Saves the current environment.
• {"pickleTo": "path/to/file.olean", "proofState": <number>}: Saves a specific proof state.
• {"unpickleEnvFrom": "path/to/file.olean"}: Loads an environment from a file.
• {"unpickleProofStateFrom": "path/to/file.olean"}: Loads a proof state from a file.

Unpickling commands return the new env or proofState identifier for use in subsequent commands.

{"pickleTo": "path/to/file.olean", "env": 7}
{"unpickleEnvFrom": "path/to/file.olean"}

File mode is a wrapper around command mode that allows you to process an entire .lean file. You provide a JSON object specifying the path to the file and whether to include all tactics via allTactics.

echo '{"path": "test/file.lean", "allTactics": true}' | lake exe repl