| Name | lean-interact JSON |
| Version |
0.1.0
JSON |
| download |
| home_page | None |
| Summary | LeanInteract is a Python package that allows you to interact with the Lean theorem prover. |
| upload_time | 2025-02-05 17:09:42 |
| maintainer | None |
| docs_url | None |
| author | None |
| requires_python | >=3.10 |
| license | MIT License Copyright (c) 2023 LeanDojo Team Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. |
| keywords |
lean
repl
autoformalization
theorem proving
|
| VCS |
|
| bugtrack_url |
|
| requirements |
No requirements were recorded.
|
| Travis-CI |
No Travis.
|
| coveralls test coverage |
No coveralls.
|
# LeanInteract
**LeanInteract** is a Python package designed to seamlessly interact with Lean 4 through the [Lean REPL](https://github.com/leanprover-community/repl).
> [!NOTE]
> This tool is still experimental and has been primarily tested on Linux. Compatibility with macOS is not guaranteed. Windows is not supported at the moment. Please report any issues you encounter.
## Key Features
- **š Ease of Use**: LeanInteract abstracts the complexities of Lean setup and interaction, enabling quick experimentation.
- **š Interactivity**: Execute Lean code, files, tactics, and (partial) proofs directly from Python. Easily iterate through environment and proof states.
- **š§ Compatibility**: Supports Lean versions from `v4.7.0-rc1` to `v4.16.0-rc2`.
- Ensures compatibility with various Lean projects and machine learning benchmarks.
- Need older versions? Open an issue [here](https://github.com/augustepoiroux/repl).
- **š Up-to-date**: LeanInteract is a lightweight wrapper around [Lean REPL](https://github.com/leanprover-community/repl), ensuring it stays current with the latest Lean versions and features.
- **š„ Automatic Setup**: Automatically downloads and builds Lean REPL versions for you. Versions are cached for fast reuse.
- **š¦ Temporary Projects**: Easily instantiate temporary Lean environments with dependencies.
- Useful for experimenting and interacting with benchmarks like [ProofNet](https://github.com/zhangir-azerbayev/ProofNet) and [MiniF2F](https://github.com/yangky11/miniF2F-lean4) without manual setup.
## Similar tools
We recommend checking out these tools:
- **[PyPantograph](https://github.com/lenianiva/PyPantograph)**: Based on Pantograph, offering more options for proof interactions than Lean REPL.
- **[LeanDojo](https://github.com/lean-dojo/LeanDojo)**: Parses Lean projects to create datasets and interact with theorems to prove them.
- **[leanclient](https://github.com/oOo0oOo/leanclient)**: Interact with the Lean LSP server.
LeanInteract is inspired by:
- **[pylean](https://github.com/zhangir-azerbayev/repl)**
- **[lean4_jupyter](https://github.com/utensil/lean4_jupyter)**
## Installation and Setup
Requirements:
- Python >= 3.10
- git
- [Lean 4](https://leanprover-community.github.io/get_started.html)
If the requirements are met, install the LeanInteract package:
```bash
pip install lean-interact
```
## Script examples
In the `examples` directory, you will find various scripts demonstrating how to use LeanInteract:
- `minif2f_deepseek_prover_v1_5.py`: use [DeepSeek-Prover-V1.5](https://arxiv.org/abs/2408.08152) to prove theorems from the [MiniF2F](https://github.com/yangky11/miniF2F-lean4) benchmark.
- `proofnetsharp_type_check.py`: type check theorems from the [ProofNet#](https://github.com/zhangir-azerbayev/ProofNet) benchmark.
- `proofnetsharp_false_theorems.py`: find theorems that can be proven false from the [ProofNet#](https://github.com/zhangir-azerbayev/ProofNet) benchmark.
- `proofnet_metric_beq_plus.py`: run a simple [BEq](https://openreview.net/forum?id=hUb2At2DsQ) checker on the ProofNet-Metric benchmark.
- `improving_autoformalization_using_type_checking.py`: an implementation of the sampling method used in [Improving Autoformalization using Type Checking](https://arxiv.org/abs/2406.07222).
## Usage
### Default Lean version (latest available)
```python
from lean_interact import LeanREPLConfig, LeanServer
config = LeanREPLConfig() # download and build Lean REPL
server = LeanServer(config) # start Lean REPL
server.run_code("theorem ex (n : Nat) : n = 5 ā n = 5 := sorry")
```
<details>
<summary>Output</summary>
```json
{"sorries": [{"proofState": 0,
"pos": {"line": 1, "column": 40},
"goal": "n : Nat\nā¢ n = 5 ā n = 5",
"endPos": {"line": 1, "column": 45}}],
"messages": [{"severity": "warning",
"pos": {"line": 1, "column": 8},
"endPos": {"line": 1, "column": 10},
"data": "declaration uses 'sorry'"}],
"env": 0}
```
</details>
You can then iterate on the proof state by executing tactics:
```python
server.run_tactic("intro h", proof_state=0)
```
<details>
<summary>Output</summary>
```json
{"proofState": 1, "goals": ["n : Nat\nh : n = 5\nā¢ n = 5"]}
```
</details>
```python
server.run_tactic("exact h", proof_state=1)
```
<details>
<summary>Output</summary>
```json
{"proofState": 2, "goals": []}
```
</details>
Or by running the entire proof:
```python
server.run_proof("intro h\nexact h", proof_state=0)
```
<details>
<summary>Output</summary>
```json
{"proofState": 3, "goals": []}
```
</details>
You can also iterate on the environment:
```python
server.run_code("theorem ex2 (x : Nat) : x = 5 ā x = 5 := by\n exact ex x", env=0)
```
<details>
<summary>Output</summary>
```json
{"env": 1}
```
</details>
> [!NOTE]
> The initial invocation of `LeanREPLConfig` might take some time as it downloads and builds Lean REPL. Future executions with identical parameters will be significantly quicker due to caching.
### Using a specific Lean version
```python
config = LeanREPLConfig(lean_version="v4.7.0")
```
### Using an existing Lean project directory
```python
config = LeanREPLConfig(project_dir="path/to/your/project")
```
You can then use `run_code`, `run_tactic` and `run_file` as usual:
```python
server = LeanServer(config)
server.run_file("file.lean")
```
> [!IMPORTANT]
> Ensure the project in `project_dir` has been *successfully* built with `lake build` before using the REPL.
### Using a temporary project with dependencies
```python
config = LeanREPLConfig(lean_version="v4.7.0", require=[LeanRequire(
name="mathlib",
git="https://github.com/leanprover-community/mathlib4.git",
rev="v4.7.0"
)])
```
Mathlib being a frequent requirement, a shortcut is available:
```python
config = LeanREPLConfig(lean_version="v4.7.0", require="mathlib")
```
You can then use Mathlib:
```python
server = LeanServer(config_readme_mathlib)
server.run_code("""import Mathlib
theorem ex_mathlib (x : ā) (y : ā) :\n ( Irrational x ) -> Irrational ( x + y ) := sorry""")
```
<details>
<summary>Output</summary>
```json
{"sorries": [{"proofState": 0,
"pos": {"line": 4, "column": 26},
"goal": "x : ā\ny : ā\nā¢ Irrational (x + āy)",
"endPos": {"line": 4, "column": 31}}],
"messages": [{"severity": "warning",
"pos": {"line": 3, "column": 8},
"endPos": {"line": 3, "column": 18},
"data": "declaration uses 'sorry'"}],
"env": 0}
```
</details>
> [!NOTE]
>
> - Mathlib is a large library and may take some time to download and build.
> - Mathlib, and other libraries, are not available for all Lean versions. An error will be raised if the Lean version you are using does not support Mathlib. You can always specify a different version with the `lean_version` parameter if you know a compatible version.
> - A separate cache is used for each unique set of dependencies.
## Advanced options
### LeanServer
Two versions of Lean servers are available:
- **`LeanServer`**: A wrapper around Lean REPL. Interact with it using `run_code`, `run_file`, and `run_tactic` methods.
- **`AutoLeanServer`**: An experimental subclass of `LeanServer` monitoring memory usage to limit *out of memory* crashes in multiprocessing contexts. Additionally, since Lean REPL retains all environment and proof states, `AutoLeanServer` regularly clears the REPL's memory to prevent crashes. Use the `add_to_session_cache` attribute in various methods to prevent selected environment/proof states to be cleared.
> [!TIP]
>
> - To run multiple requests in parallel, we recommend using multiprocessing with one `AutoLeanServer` instance per process.
> - Make sure to instantiate `LeanREPLConfig` before starting the processes to avoid conflicts during Lean REPL's download and build.
> - While `AutoLeanServer` can help prevent crashes, it is not a complete solution. If you encounter crashes, consider reducing the number of parallel processes or increasing the memory available to your system.
### Helper Methods and Variables
- `clear_cache()`: Removes all Lean REPL versions and temporary projects in the package cache. This can help resolve some issues. If it does, please open an issue.
### Custom Lean REPL
To use a forked Lean REPL project, specify the git repository using the `repl_git` parameter in the `LeanREPLConfig`. Your fork should have a similar format to <https://github.com/augustepoiroux/repl>. For assistance, feel free to contact [us](mailto:auguste.poiroux@epfl.ch).
Raw data
{
"_id": null,
"home_page": null,
"name": "lean-interact",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.10",
"maintainer_email": null,
"keywords": "Lean, REPL, autoformalization, theorem proving",
"author": null,
"author_email": "Auguste Poiroux <auguste.poiroux@epfl.ch>",
"download_url": "https://files.pythonhosted.org/packages/5e/3a/3cc1aacbfe25a3b88d6007651dc0e4e1fe6db2f478082bd8727297466dd3/lean_interact-0.1.0.tar.gz",
"platform": null,
"description": "# LeanInteract\n\n**LeanInteract** is a Python package designed to seamlessly interact with Lean 4 through the [Lean REPL](https://github.com/leanprover-community/repl).\n\n> [!NOTE]\n> This tool is still experimental and has been primarily tested on Linux. Compatibility with macOS is not guaranteed. Windows is not supported at the moment. Please report any issues you encounter.\n\n## Key Features\n\n- **\ud83d\ude80 Ease of Use**: LeanInteract abstracts the complexities of Lean setup and interaction, enabling quick experimentation.\n- **\ud83d\udd17 Interactivity**: Execute Lean code, files, tactics, and (partial) proofs directly from Python. Easily iterate through environment and proof states.\n- **\ud83d\udd27 Compatibility**: Supports Lean versions from `v4.7.0-rc1` to `v4.16.0-rc2`.\n - Ensures compatibility with various Lean projects and machine learning benchmarks.\n - Need older versions? Open an issue [here](https://github.com/augustepoiroux/repl).\n- **\ud83d\udd04 Up-to-date**: LeanInteract is a lightweight wrapper around [Lean REPL](https://github.com/leanprover-community/repl), ensuring it stays current with the latest Lean versions and features.\n- **\ud83d\udce5 Automatic Setup**: Automatically downloads and builds Lean REPL versions for you. Versions are cached for fast reuse.\n- **\ud83d\udce6 Temporary Projects**: Easily instantiate temporary Lean environments with dependencies.\n - Useful for experimenting and interacting with benchmarks like [ProofNet](https://github.com/zhangir-azerbayev/ProofNet) and [MiniF2F](https://github.com/yangky11/miniF2F-lean4) without manual setup.\n\n## Similar tools\n\nWe recommend checking out these tools:\n\n- **[PyPantograph](https://github.com/lenianiva/PyPantograph)**: Based on Pantograph, offering more options for proof interactions than Lean REPL.\n- **[LeanDojo](https://github.com/lean-dojo/LeanDojo)**: Parses Lean projects to create datasets and interact with theorems to prove them.\n- **[leanclient](https://github.com/oOo0oOo/leanclient)**: Interact with the Lean LSP server.\n\nLeanInteract is inspired by:\n\n- **[pylean](https://github.com/zhangir-azerbayev/repl)**\n- **[lean4_jupyter](https://github.com/utensil/lean4_jupyter)**\n\n## Installation and Setup\n\nRequirements:\n\n- Python >= 3.10\n- git\n- [Lean 4](https://leanprover-community.github.io/get_started.html)\n\nIf the requirements are met, install the LeanInteract package:\n\n```bash\npip install lean-interact\n```\n\n## Script examples\n\nIn the `examples` directory, you will find various scripts demonstrating how to use LeanInteract:\n\n- `minif2f_deepseek_prover_v1_5.py`: use [DeepSeek-Prover-V1.5](https://arxiv.org/abs/2408.08152) to prove theorems from the [MiniF2F](https://github.com/yangky11/miniF2F-lean4) benchmark.\n- `proofnetsharp_type_check.py`: type check theorems from the [ProofNet#](https://github.com/zhangir-azerbayev/ProofNet) benchmark.\n- `proofnetsharp_false_theorems.py`: find theorems that can be proven false from the [ProofNet#](https://github.com/zhangir-azerbayev/ProofNet) benchmark.\n- `proofnet_metric_beq_plus.py`: run a simple [BEq](https://openreview.net/forum?id=hUb2At2DsQ) checker on the ProofNet-Metric benchmark.\n- `improving_autoformalization_using_type_checking.py`: an implementation of the sampling method used in [Improving Autoformalization using Type Checking](https://arxiv.org/abs/2406.07222).\n\n## Usage\n\n### Default Lean version (latest available)\n\n```python\nfrom lean_interact import LeanREPLConfig, LeanServer\n\nconfig = LeanREPLConfig() # download and build Lean REPL\nserver = LeanServer(config) # start Lean REPL\nserver.run_code(\"theorem ex (n : Nat) : n = 5 \u2192 n = 5 := sorry\")\n```\n\n<details>\n<summary>Output</summary>\n\n```json\n{\"sorries\": [{\"proofState\": 0,\n \"pos\": {\"line\": 1, \"column\": 40},\n \"goal\": \"n : Nat\\n\u22a2 n = 5 \u2192 n = 5\",\n \"endPos\": {\"line\": 1, \"column\": 45}}],\n \"messages\": [{\"severity\": \"warning\",\n \"pos\": {\"line\": 1, \"column\": 8},\n \"endPos\": {\"line\": 1, \"column\": 10},\n \"data\": \"declaration uses 'sorry'\"}],\n \"env\": 0}\n```\n\n</details>\n\nYou can then iterate on the proof state by executing tactics:\n\n```python\nserver.run_tactic(\"intro h\", proof_state=0)\n```\n\n<details>\n<summary>Output</summary>\n\n```json\n{\"proofState\": 1, \"goals\": [\"n : Nat\\nh : n = 5\\n\u22a2 n = 5\"]}\n```\n\n</details>\n\n```python\nserver.run_tactic(\"exact h\", proof_state=1)\n```\n\n<details>\n<summary>Output</summary>\n\n```json\n{\"proofState\": 2, \"goals\": []}\n```\n\n</details>\n\nOr by running the entire proof:\n\n```python\nserver.run_proof(\"intro h\\nexact h\", proof_state=0)\n```\n\n<details>\n<summary>Output</summary>\n\n```json\n{\"proofState\": 3, \"goals\": []}\n```\n\n</details>\n\nYou can also iterate on the environment:\n\n```python\nserver.run_code(\"theorem ex2 (x : Nat) : x = 5 \u2192 x = 5 := by\\n exact ex x\", env=0)\n```\n\n<details>\n<summary>Output</summary>\n\n```json\n{\"env\": 1}\n```\n\n</details>\n\n> [!NOTE]\n> The initial invocation of `LeanREPLConfig` might take some time as it downloads and builds Lean REPL. Future executions with identical parameters will be significantly quicker due to caching.\n\n### Using a specific Lean version\n\n```python\nconfig = LeanREPLConfig(lean_version=\"v4.7.0\")\n```\n\n### Using an existing Lean project directory\n\n```python\nconfig = LeanREPLConfig(project_dir=\"path/to/your/project\")\n```\n\nYou can then use `run_code`, `run_tactic` and `run_file` as usual:\n\n```python\nserver = LeanServer(config)\nserver.run_file(\"file.lean\")\n```\n\n> [!IMPORTANT]\n> Ensure the project in `project_dir` has been *successfully* built with `lake build` before using the REPL.\n\n### Using a temporary project with dependencies\n\n```python\nconfig = LeanREPLConfig(lean_version=\"v4.7.0\", require=[LeanRequire(\n name=\"mathlib\",\n git=\"https://github.com/leanprover-community/mathlib4.git\",\n rev=\"v4.7.0\"\n)])\n```\n\nMathlib being a frequent requirement, a shortcut is available:\n\n```python\nconfig = LeanREPLConfig(lean_version=\"v4.7.0\", require=\"mathlib\")\n```\n\nYou can then use Mathlib:\n\n```python\nserver = LeanServer(config_readme_mathlib)\nserver.run_code(\"\"\"import Mathlib\ntheorem ex_mathlib (x : \u211d) (y : \u211a) :\\n ( Irrational x ) -> Irrational ( x + y ) := sorry\"\"\")\n```\n\n<details>\n<summary>Output</summary>\n\n```json\n{\"sorries\": [{\"proofState\": 0,\n \"pos\": {\"line\": 4, \"column\": 26},\n \"goal\": \"x : \u211d\\ny : \u211a\\n\u22a2 Irrational (x + \u2191y)\",\n \"endPos\": {\"line\": 4, \"column\": 31}}],\n \"messages\": [{\"severity\": \"warning\",\n \"pos\": {\"line\": 3, \"column\": 8},\n \"endPos\": {\"line\": 3, \"column\": 18},\n \"data\": \"declaration uses 'sorry'\"}],\n \"env\": 0}\n```\n\n</details>\n\n> [!NOTE]\n>\n> - Mathlib is a large library and may take some time to download and build.\n> - Mathlib, and other libraries, are not available for all Lean versions. An error will be raised if the Lean version you are using does not support Mathlib. You can always specify a different version with the `lean_version` parameter if you know a compatible version.\n> - A separate cache is used for each unique set of dependencies.\n\n## Advanced options\n\n### LeanServer\n\nTwo versions of Lean servers are available:\n\n- **`LeanServer`**: A wrapper around Lean REPL. Interact with it using `run_code`, `run_file`, and `run_tactic` methods.\n- **`AutoLeanServer`**: An experimental subclass of `LeanServer` monitoring memory usage to limit *out of memory* crashes in multiprocessing contexts. Additionally, since Lean REPL retains all environment and proof states, `AutoLeanServer` regularly clears the REPL's memory to prevent crashes. Use the `add_to_session_cache` attribute in various methods to prevent selected environment/proof states to be cleared.\n\n> [!TIP]\n>\n> - To run multiple requests in parallel, we recommend using multiprocessing with one `AutoLeanServer` instance per process.\n> - Make sure to instantiate `LeanREPLConfig` before starting the processes to avoid conflicts during Lean REPL's download and build.\n> - While `AutoLeanServer` can help prevent crashes, it is not a complete solution. If you encounter crashes, consider reducing the number of parallel processes or increasing the memory available to your system.\n\n### Helper Methods and Variables\n\n- `clear_cache()`: Removes all Lean REPL versions and temporary projects in the package cache. This can help resolve some issues. If it does, please open an issue.\n\n### Custom Lean REPL\n\nTo use a forked Lean REPL project, specify the git repository using the `repl_git` parameter in the `LeanREPLConfig`. Your fork should have a similar format to <https://github.com/augustepoiroux/repl>. For assistance, feel free to contact [us](mailto:auguste.poiroux@epfl.ch).\n",
"bugtrack_url": null,
"license": "MIT License Copyright (c) 2023 LeanDojo Team Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the \"Software\"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED \"AS IS\", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.",
"summary": "LeanInteract is a Python package that allows you to interact with the Lean theorem prover.",
"version": "0.1.0",
"project_urls": null,
"split_keywords": [
"lean",
" repl",
" autoformalization",
" theorem proving"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "aa25729f44390a5be36e75466865d7763a4c07f5a2ab1418f7edaa8bc4f4c19a",
"md5": "5c9a68b44c7885e688016257a01b4b01",
"sha256": "db5b5038c12127bd2ed0f8d6801d61b0727a378be7c44521a8f5b797d4ccccac"
},
"downloads": -1,
"filename": "lean_interact-0.1.0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "5c9a68b44c7885e688016257a01b4b01",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.10",
"size": 14771,
"upload_time": "2025-02-05T17:09:40",
"upload_time_iso_8601": "2025-02-05T17:09:40.790125Z",
"url": "https://files.pythonhosted.org/packages/aa/25/729f44390a5be36e75466865d7763a4c07f5a2ab1418f7edaa8bc4f4c19a/lean_interact-0.1.0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "5e3a3cc1aacbfe25a3b88d6007651dc0e4e1fe6db2f478082bd8727297466dd3",
"md5": "d6086f433610531e473b7e06654927d5",
"sha256": "6634fa75a9b1bbd6380b43ce2530c46be74ab1b077dc1b941375709e6d7f80a5"
},
"downloads": -1,
"filename": "lean_interact-0.1.0.tar.gz",
"has_sig": false,
"md5_digest": "d6086f433610531e473b7e06654927d5",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.10",
"size": 46361,
"upload_time": "2025-02-05T17:09:42",
"upload_time_iso_8601": "2025-02-05T17:09:42.352084Z",
"url": "https://files.pythonhosted.org/packages/5e/3a/3cc1aacbfe25a3b88d6007651dc0e4e1fe6db2f478082bd8727297466dd3/lean_interact-0.1.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-02-05 17:09:42",
"github": false,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"lcname": "lean-interact"
}
