Run using ./run
.
Communicates via JSON on stdin and stdout.
Commands should be separated by blank lines.
Commands may be of the form
{ "cmd" : "import Mathlib.Data.List.Basic\ndef f := 2" }
or
{ "cmd" : "example : f = 2 := rfl", "env" : 3 }
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 results are of the form
{"sorries":
[{"pos": {"line": 1, "column": 18},
"endPos": {"line": 1, "column": 23},
"goal": "⊢ Nat"}],
"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, or sorries with their goal states.
Information is generated for tactic mode sorries, but currently not for term mode sorries.
This repository comes with pylean
, a package that creates Python bindings for the repl. Currently, the python package depends on pexpect
, and is therefore is only compatible with MacOS/Linux/FreeBSD systems.
To use the python bindings, first cd
into the root directory of this repository and run lake build
. Then, run pip install pylean
. Now, you should be able to execute python scripts such as
from pylean import LeanServer
lean = LeanServer()
out = lean.run_code("example : 2 = 2 := rfl", verbose=True)
out1 = lean.run_code("def f := 37")
env_num = out1["env"]
out2 = lean.run_code("#check (rfl: f = 37)", env=env_num)
print(out2)
This should output
{ "cmd" : "example : 2 = 2 := rfl" }
{"sorries": [], "messages": [], "env": 0}
{'sorries': [], 'messages': [{'severity': 'info', 'pos': {'line': 1, 'column': 0}, 'endPos': {'line': 1, 'column': 6}, 'data': 'rfl : f = f'}], 'env': 2}
Running Lean programs that import Mathlib
is a common use case. To enable mathlib4
imports, simply add the following to lakefile.lean
and run lake exe cache get
before running lake build
.
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"