Python package

.gitignore

@@ -1,2 +1,164 @@
 /build
 /lake-packages/*
+
+# python gitignore
+# Byte-compiled / optimized / DLL files
+__pycache__/
+*.py[cod]
+*$py.class
+
+# C extensions
+*.so
+
+# Distribution / packaging
+.Python
+build/
+develop-eggs/
+dist/
+downloads/
+eggs/
+.eggs/
+lib/
+lib64/
+parts/
+sdist/
+var/
+wheels/
+share/python-wheels/
+*.egg-info/
+.installed.cfg
+*.egg
+MANIFEST
+
+# PyInstaller
+#  Usually these files are written by a python script from a template
+#  before PyInstaller builds the exe, so as to inject date/other infos into it.
+*.manifest
+*.spec
+
+# Installer logs
+pip-log.txt
+pip-delete-this-directory.txt
+
+# Unit test / coverage reports
+htmlcov/
+.tox/
+.nox/
+.coverage
+.coverage.*
+.cache
+nosetests.xml
+coverage.xml
+*.cover
+*.py,cover
+.hypothesis/
+.pytest_cache/
+cover/
+
+# Translations
+*.mo
+*.pot
+
+# Django stuff:
+*.log
+local_settings.py
+db.sqlite3
+db.sqlite3-journal
+
+# Flask stuff:
+instance/
+.webassets-cache
+
+# Scrapy stuff:
+.scrapy
+
+# Sphinx documentation
+docs/_build/
+
+# PyBuilder
+.pybuilder/
+target/
+
+# Jupyter Notebook
+.ipynb_checkpoints
+
+# IPython
+profile_default/
+ipython_config.py
+
+# pyenv
+#   For a library or package, you might want to ignore these files since the code is
+#   intended to run in multiple environments; otherwise, check them in:
+# .python-version
+
+# pipenv
+#   According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
+#   However, in case of collaboration, if having platform-specific dependencies or dependencies
+#   having no cross-platform support, pipenv may install dependencies that don't work, or not
+#   install all needed dependencies.
+#Pipfile.lock
+
+# poetry
+#   Similar to Pipfile.lock, it is generally recommended to include poetry.lock in version control.
+#   This is especially recommended for binary packages to ensure reproducibility, and is more
+#   commonly ignored for libraries.
+#   https://python-poetry.org/docs/basic-usage/#commit-your-poetrylock-file-to-version-control
+#poetry.lock
+
+# pdm
+#   Similar to Pipfile.lock, it is generally recommended to include pdm.lock in version control.
+#pdm.lock
+#   pdm stores project-wide configurations in .pdm.toml, but it is recommended to not include it
+#   in version control.
+#   https://pdm.fming.dev/#use-with-ide
+.pdm.toml
+
+# PEP 582; used by e.g. github.com/David-OConnor/pyflow and github.com/pdm-project/pdm
+__pypackages__/
+
+# Celery stuff
+celerybeat-schedule
+celerybeat.pid
+
+# SageMath parsed files
+*.sage.py
+
+# Environments
+.env
+.venv
+env/
+venv/
+ENV/
+env.bak/
+venv.bak/
+
+# Spyder project settings
+.spyderproject
+.spyproject
+
+# Rope project settings
+.ropeproject
+
+# mkdocs documentation
+/site
+
+# mypy
+.mypy_cache/
+.dmypy.json
+dmypy.json
+
+# Pyre type checker
+.pyre/
+
+# pytype static type analyzer
+.pytype/
+
+# Cython debug symbols
+cython_debug/
+
+# PyCharm
+#  JetBrains specific template is maintained in a separate JetBrains.gitignore that can
+#  be found at https://github.com/github/gitignore/blob/main/Global/JetBrains.gitignore
+#  and can be added to the global gitignore or merged into this file.  For a more nuclear
+#  option (not recommended) you can uncomment the following to ignore the entire idea folder.
+#.idea/

README.md

@@ -45,3 +45,34 @@ showing any messages generated, or sorries with their goal states.
 
 Information is generated for tactic mode sorries,
 but currently not for term mode sorries.
+
+## Python package
+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 
+```python
+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"
+```

pylean/pylean/__init__.py

@@ -0,0 +1,37 @@
+import pexpect
+import json
+
+import os
+
+class LeanServer:
+    def __init__(self):
+        path_to_repl = os.path.dirname(os.path.dirname(os.path.dirname(__file__)))
+
+        self.proc = pexpect.spawn(
+            "lake env lean --run REPL/Main.lean", cwd=path_to_repl, encoding="utf-8"
+        )
+
+    def run_code(self, code, env=None, verbose=False):
+        if env:
+            command = (
+                '{ "cmd" : "' + repr(code)[1:-1] + f'", "env" : {env}' + " }"
+            )  # [1:-1] removes single quotes
+        else:
+            command = (
+                '{ "cmd" : "' + repr(code)[1:-1] + '" }'
+            )  # [1:-1] removes single quotes
+
+        if verbose:
+            print(command)
+        self.proc.sendline(command)
+        self.proc.expect_exact(command + "\r\n")
+        self.proc.sendline()
+        self.proc.expect_exact("\r\n")
+        try:
+            index = self.proc.expect('env": \d+\}', timeout=20)
+            output = self.proc.before + self.proc.match.group()
+            if verbose: 
+                print(output)
+            return json.loads(output)
+        except pexpect.exceptions.TIMEOUT:
+            raise pexpect.exceptions.TIMEOUT

pylean/pyproject.toml

@@ -0,0 +1,14 @@
+[tool.poetry]
+name = "pylean"
+version = "0.1.0"
+description = ""
+authors = ["zhangir-azerbayev <zazerbayev@gmail.com>"]
+readme = "README.md"
+
+[tool.poetry.dependencies]
+python = "^3.10"
+
+
+[build-system]
+requires = ["poetry-core", "pexpect"]
+build-backend = "poetry.core.masonry.api"

pylean/setup.py

@@ -0,0 +1,6 @@
+#!/usr/bin/env python
+
+import setuptools
+
+if __name__ == "__main__":
+    setuptools.setup()

pylean/tests/test_server.py

@@ -0,0 +1,28 @@
+import unittest
+from pylean import LeanServer
+import os
+
+
+class TestGym(unittest.TestCase):
+    def test_run_code(self): 
+        proofsearch = LeanServer()
+
+        # should return empty sorries and goals
+        out = proofsearch.run_code("def f := 2", verbose=True)
+        self.assertEqual(out["sorries"], [])
+        self.assertEqual(out["messages"], [])
+
+        # should return goal state
+        out = proofsearch.run_code("example : 2 = 2 := by", verbose=True)
+        self.assertTrue(any("unsolved goals" in m["data"] for m in out["messages"]))
+
+        # should return error
+        out = proofsearch.run_code("example : 2 = 3 := rfl", verbose=True)
+        self.assertTrue("type mismatch" in out["messages"][0]["data"])
+
+        # should return goal state
+        feedback = proofsearch.run_code("def f := 37", verbose=True)
+        env = feedback["env"]
+        out = proofsearch.run_code("#check (rfl: f = 37)", env=env, verbose=True)
+        print(out)
+        self.assertTrue(all(m["severity"]!="error" for m in out["messages"]))