A read-eval-print-loop for Lean 4

Run using lake exe repl. Communicates via JSON on stdin and stdout. Commands should be separated by blank lines.

The REPL works both in "command" mode and "tactic" mode.

Command mode

In command mode, you send complete commands (e.g. declarations) to the REPL.

Commands may be of the form

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

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

The env field, if present, must contain a number received in the env field of a previous response, and causes the command to be run in the existing environment.

If there is no env field, a new environment is created.

You can only use import commands when you do not specify the env field.

You can backtrack simply by using earlier values for env.

The response includes:

• A numeric label for the Environment after your command, which you can use as the starting point for subsequent commands.
• Any messages generated while processing your command.
• A list of the sorrys in your command, including
  • their expected type, and
  • a numeric label for the proof state at the sorry, which you can then use in tactic mode.

Example output:

{"sorries":
 [{"pos": {"line": 1, "column": 18},
   "endPos": {"line": 1, "column": 23},
   "goal": "⊢ Nat",
   "proofState": 0}],
 "messages":
 [{"severity": "error",
   "pos": {"line": 1, "column": 23},
   "endPos": {"line": 1, "column": 26},
   "data":
   "type mismatch\n  rfl\nhas type\n  f = f : Prop\nbut is expected to have type\n  f = 2 : Prop"}],
 "env": 6}

showing any messages generated, and sorries with their goal states.

File mode

There is a simple wrapper around command mode that allows reading in an entire file.

If test/file.lean contains

def f : Nat := 37

def g := 2

theorem h : f + g = 39 := by exact rfl

then

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

results in output

{"tactics":
 [{"tactic": "exact rfl",
   "proofState": 0,
   "pos": {"line": 5, "column": 29},
   "goals": "⊢ f + g = 39",
   "endPos": {"line": 5, "column": 38}}],
 "env": 0}

Tactic mode (experimental)

To enter tactic mode issue a command containing a sorry, and then use the proofState index returned for each sorry.

Example usage:

{"cmd" : "def f (x : Unit) : Nat := by sorry"}

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 1, "column": 29},
   "goal": "x : Unit\n⊢ Nat",
   "endPos": {"line": 1, "column": 34}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 1, "column": 4},
   "endPos": {"line": 1, "column": 5},
   "data": "declaration uses 'sorry'"}],
 "env": 0}

{"tactic": "apply Int.natAbs", "proofState": 0}

{"proofState": 1, "goals": ["x : Unit\n⊢ Int"]}

{"tactic": "exact -37", "proofState": 1}

{"proofState": 2, "goals": []}

You can use sorry in tactic mode. The result will contain additional proofState identifiers for the goal at each sorry.

At present there is nothing you can do with a completed proof state: we would like to extend this so that you can replace the original sorry with your tactic script, and obtain the resulting Environment

Pickling

The REPL supports pickling environments and proof states to disk as .olean files. As long as the same imports are available, it should be possible to move such an .olean file to another machine and unpickle into a new REPL session.

The commands are

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

{"pickleTo": "path/to/file.olean", "proofState": 17}

{"unpickleEnvFrom": "path/to/file.olean"}

{"unpickleProofStateFrom": "path/to/file.olean"}

The unpickling commands will report the new "env" or "proofState" identifier that you can use in subsequent commands.

Pickling is quite efficient:

• we don't record full Environments, only the changes relative to imports
• unpickling uses memory mapping
• file sizes are generally small, but see https://github.com/digama0/leangz if compression is desirable

Using the REPL from another project

Set up your project as usual using lake new or lake init (or the interactive setup GUI available via the VSCode extension under the ∀ menu).

In that project, add require statements in the lakefile.lean for any dependencies you need (e.g. Mathlib). (You probably should verify that lake build works as expected in that project.)

Now you can run the REPL as:

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

(Here ../path/to/repl/ represents the path to your checkout of this repository, in which you've already run lake build.)

The lake env prefix sets up the environment associated to your local project, so that the REPL can find needed imports.

Future work

• Replay tactic scripts from tactic mode back into the original sorry.
• Currently if you create scoped environment extensions (e.g. scoped notations) in a session these are not correctly pickled and unpickled in later sessions.