search

leanprover-community / repl

A simple REPL for Lean 4, returning information about errors and sorries.
69 stars 16 forks source link

Python package #5

Open zhangir-azerbayev opened 1 year ago

zhangir-azerbayev commented 1 year ago

Adds python interface via a package called pylean. See README.md for usage instructions. Unit tests in pylean/tests.

zhangir-azerbayev commented 1 year ago

Currently, we require users to build the package from source from within this repository. Once we get the compiled version of the repl working, the python package should be installable with only pip install pylean.

zhangir-azerbayev commented 1 year ago

Thanks for the reviews.

I see that since I opened this PR, the bug that prevented the repl from compiling was fixed. Therefore I'm going to convert this PR back to a draft and work on a version of the python package that installs a pre-compiled binary of the repl.