From 603356f37188d70ca3643c5221212e537154e015 Mon Sep 17 00:00:00 2001 From: zhangir-azerbayev Date: Wed, 5 Apr 2023 14:21:59 -0400 Subject: [PATCH 1/6] added python package structure --- pylean/README.md | 0 pylean/pylean/__init__.py | 0 pylean/pyproject.toml | 14 ++++++++++++++ pylean/setup.py | 6 ++++++ pylean/tests/__init__.py | 0 5 files changed, 20 insertions(+) create mode 100644 pylean/README.md create mode 100644 pylean/pylean/__init__.py create mode 100644 pylean/pyproject.toml create mode 100644 pylean/setup.py create mode 100644 pylean/tests/__init__.py diff --git a/pylean/README.md b/pylean/README.md new file mode 100644 index 00000000..e69de29b diff --git a/pylean/pylean/__init__.py b/pylean/pylean/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/pylean/pyproject.toml b/pylean/pyproject.toml new file mode 100644 index 00000000..cb76a606 --- /dev/null +++ b/pylean/pyproject.toml @@ -0,0 +1,14 @@ +[tool.poetry] +name = "pylean" +version = "0.1.0" +description = "" +authors = ["zhangir-azerbayev "] +readme = "README.md" + +[tool.poetry.dependencies] +python = "^3.10" + + +[build-system] +requires = ["poetry-core"] +build-backend = "poetry.core.masonry.api" diff --git a/pylean/setup.py b/pylean/setup.py new file mode 100644 index 00000000..bac24a43 --- /dev/null +++ b/pylean/setup.py @@ -0,0 +1,6 @@ +#!/usr/bin/env python + +import setuptools + +if __name__ == "__main__": + setuptools.setup() diff --git a/pylean/tests/__init__.py b/pylean/tests/__init__.py new file mode 100644 index 00000000..e69de29b From 6422f1a1185f3c3f9d121ce0f9241c1fce9a5bab Mon Sep 17 00:00:00 2001 From: zhangir-azerbayev Date: Wed, 5 Apr 2023 14:39:31 -0400 Subject: [PATCH 2/6] appended python gitignore to gitignore --- .gitignore | 162 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 162 insertions(+) diff --git a/.gitignore b/.gitignore index 20c60d75..bddf148e 100644 --- a/.gitignore +++ b/.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/ From 5c7be2004b0bbea8d4f92a32f8cd21edde7d0e8e Mon Sep 17 00:00:00 2001 From: zhangir-azerbayev Date: Wed, 5 Apr 2023 14:39:52 -0400 Subject: [PATCH 3/6] pylean passing tests --- pylean/pylean/__init__.py | 37 +++++++++++++++++++++++++++++++++++++ pylean/pyproject.toml | 2 +- pylean/tests/test_server.py | 28 ++++++++++++++++++++++++++++ 3 files changed, 66 insertions(+), 1 deletion(-) create mode 100644 pylean/tests/test_server.py diff --git a/pylean/pylean/__init__.py b/pylean/pylean/__init__.py index e69de29b..45ecd012 100644 --- a/pylean/pylean/__init__.py +++ b/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__))) + print(f"PATH TO REPL {path_to_repl}") + 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 diff --git a/pylean/pyproject.toml b/pylean/pyproject.toml index cb76a606..26498973 100644 --- a/pylean/pyproject.toml +++ b/pylean/pyproject.toml @@ -10,5 +10,5 @@ python = "^3.10" [build-system] -requires = ["poetry-core"] +requires = ["poetry-core", "pexpect"] build-backend = "poetry.core.masonry.api" diff --git a/pylean/tests/test_server.py b/pylean/tests/test_server.py new file mode 100644 index 00000000..66c57bb2 --- /dev/null +++ b/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"])) From 82aefa41cd6dbd66fc9efd1d99b6214bffbe430e Mon Sep 17 00:00:00 2001 From: zhangir-azerbayev Date: Wed, 5 Apr 2023 15:03:21 -0400 Subject: [PATCH 4/6] remove useless print statement; add instructions in readme --- README.md | 31 +++++++++++++++++++++++++++++++ pylean/pylean/__init__.py | 2 +- 2 files changed, 32 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index e68d6e59..8c0e4855 100644 --- a/README.md +++ b/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. + +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 program 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" +``` diff --git a/pylean/pylean/__init__.py b/pylean/pylean/__init__.py index 45ecd012..7ab6b1f8 100644 --- a/pylean/pylean/__init__.py +++ b/pylean/pylean/__init__.py @@ -6,7 +6,7 @@ class LeanServer: def __init__(self): path_to_repl = os.path.dirname(os.path.dirname(os.path.dirname(__file__))) - print(f"PATH TO REPL {path_to_repl}") + self.proc = pexpect.spawn( "lake env lean --run REPL/Main.lean", cwd=path_to_repl, encoding="utf-8" ) From c2a04451fc965cfd2f1b0aaf8c2a2a5082b37084 Mon Sep 17 00:00:00 2001 From: zhangir-azerbayev Date: Wed, 5 Apr 2023 15:07:31 -0400 Subject: [PATCH 5/6] updated readme --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 8c0e4855..004b0f6c 100644 --- a/README.md +++ b/README.md @@ -47,7 +47,7 @@ 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. +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 @@ -71,7 +71,7 @@ This should output {"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 program 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`. +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" From bddf452deda0df2240b248e651bcc37fb8e59d01 Mon Sep 17 00:00:00 2001 From: Zhangir Azerbayev <59542043+zhangir-azerbayev@users.noreply.github.com> Date: Sun, 18 Jun 2023 20:39:04 -0400 Subject: [PATCH 6/6] Update pylean/pylean/__init__.py Co-authored-by: Eric Wieser --- pylean/pylean/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pylean/pylean/__init__.py b/pylean/pylean/__init__.py index 7ab6b1f8..2ce0cb52 100644 --- a/pylean/pylean/__init__.py +++ b/pylean/pylean/__init__.py @@ -14,7 +14,7 @@ def __init__(self): def run_code(self, code, env=None, verbose=False): if env: command = ( - '{ "cmd" : "' + repr(code)[1:-1] + f'", "env" : {env}' + " }" + json.dumps(dict(cmd=code, env=env)) ) # [1:-1] removes single quotes else: command = (