Lean Syntax Check from Python

Stream: lean4

[Austin Shen]

I want to pass in lean codes, such as
"""
import mathlib

example ....
"""
from python to check whether the lean code is syntatically accurate.

All my approaches either fail or takes minutes to check 1 single lean theorem. Is there any existing projects that does similar things?

[metakuntyyy]

Did you try calling lean from python?

[Austin Shen]

Yes, this is what I used:
self.proc = subprocess.Popen(
["lake", "env", "lean", "--server"],
cwd=project_root,
stdin=subprocess.PIPE,
stdout=subprocess.PIPE,
stderr=subprocess.PIPE,
text=True,
bufsize=1,
)

[metakuntyyy]

Try this one

lake env lean exe Filename.lean

[metakuntyyy]

You can then check the exit code.

[Niels Voss]

You can use https://github.com/augustepoiroux/LeanInteract (which is a wrapper for https://github.com/leanprover-community/repl) to spend a minute importing Mathlib once, and then re-use the same lean process so you don't have to keep re-importing