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/ diff --git a/README.md b/README.md index e68d6e59..004b0f6c 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. 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" +``` 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..2ce0cb52 --- /dev/null +++ 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__))) + + 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 = ( + json.dumps(dict(cmd=code, 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 new file mode 100644 index 00000000..26498973 --- /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", "pexpect"] +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 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"]))