From 3762fc32b0c7823ec0a86c2ff16bb18ea20c5eec Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 31 May 2026 16:32:51 +0000 Subject: [PATCH 1/4] Update Python environment setup and support Lean 4 v4.30.0 --- .github/workflows/github-build-actions-python314t.yaml | 3 ++- README.md | 2 +- src/itp_interface/lean/tactic_parser/lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/github-build-actions-python314t.yaml b/.github/workflows/github-build-actions-python314t.yaml index b864c54..178fd43 100644 --- a/.github/workflows/github-build-actions-python314t.yaml +++ b/.github/workflows/github-build-actions-python314t.yaml @@ -39,7 +39,7 @@ jobs: shell: bash run: | export PATH="$HOME/miniconda/bin:$PATH" - conda create -n py314-ft python=3.14 python-freethreading -c conda-forge -y + conda create -n py314-ft python=3.14 python-freethreading pip -c conda-forge -y conda clean -all -y - name: Check Python version and GIL status @@ -55,6 +55,7 @@ jobs: run: | export PATH="$HOME/miniconda/bin:$PATH" source $HOME/miniconda/bin/activate py314-ft + mkdir -p /root/.docker && chmod 700 /root/.docker python -m pip install --upgrade pip pip install build==1.3.0 hatchling==1.27.0 pip cache purge diff --git a/README.md b/README.md index 52a586e..6093e5e 100644 --- a/README.md +++ b/README.md @@ -16,7 +16,7 @@ pip install itp-interface ``` 2. Run the following command to prepare the REPL for Lean 4. The default version is 4.24.0. You can change the version by setting the `LEAN_VERSION` environment variable. If no version is set, then 4.24.0 is used. ->NOTE: The Lean 4 version must match the version of the Lean 4 project you are working with. `itp-interface` **supports Lean 4 version >= 4.15.0 and <= 4.24.0**. (It has been tested till version 4.24.0, but might as well work for future versions too, if the future versions are completely backwards-compatible). +>NOTE: The Lean 4 version must match the version of the Lean 4 project you are working with. `itp-interface` **supports Lean 4 versions v4.15.0 through v4.30.0**. (It has been tested till version 4.30.0, but might as well work for future versions too, if the future versions are completely backwards-compatible). ```bash install-lean-repl diff --git a/src/itp_interface/lean/tactic_parser/lean-toolchain b/src/itp_interface/lean/tactic_parser/lean-toolchain index c00a535..af9e5d3 100644 --- a/src/itp_interface/lean/tactic_parser/lean-toolchain +++ b/src/itp_interface/lean/tactic_parser/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.24.0 +leanprover/lean4:v4.30.0 From 8ec8997604b51c190403e39d89f33402c817c57e Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 31 May 2026 16:38:40 +0000 Subject: [PATCH 2/4] Bump version to 1.6.0 in pyproject.toml --- pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyproject.toml b/pyproject.toml index c08ce53..0870b99 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -5,7 +5,7 @@ requires = [ build-backend = "hatchling.build" [project] name = "itp_interface" -version = "1.5.0" +version = "1.6.0" authors = [ { name="Amitayush Thakur", email="amitayush@utexas.edu" }, ] From e9503772dd875235fdc881485a05daae86b932e3 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 31 May 2026 16:40:07 +0000 Subject: [PATCH 3/4] =?UTF-8?q?Update=20README=20to=20highlight=20support?= =?UTF-8?q?=20for=20Lean=20v4.25=E2=80=93v4.30?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 6093e5e..92c7493 100644 --- a/README.md +++ b/README.md @@ -7,6 +7,8 @@ Generic interface for hooking up to any Interactive Theorem Prover (ITP) and col ## 🎉 What's New +**Lean v4.25–v4.30 Support** (May 2026) - `itp-interface` now supports Lean 4 versions v4.25.0 through v4.30.0, extending the previously supported range of v4.15–v4.24. + **Python 3.14 Free-Threading Support** (January 2025) - `itp-interface` now supports Python 3.14's experimental free-threading mode (GIL-free execution)! Experience true parallel proof search with up to 2.13x speedup on multi-core systems. The interface automatically detects your Python version and seamlessly falls back to thread-based parallelism when Ray is unavailable. See [Python 3.14 Free-Threading Support](#python-314-free-threading-support-optional) for details. ## Quick Setup for Lean 4: From 464ab69695de18ec22524de055ebe942cb55b5c1 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 31 May 2026 17:08:37 +0000 Subject: [PATCH 4/4] Update README and tactic parser to support LEAN_VERSION environment variable --- README.md | 4 ++++ src/itp_interface/lean/tactic_parser.py | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 92c7493..1d55d3d 100644 --- a/README.md +++ b/README.md @@ -30,6 +30,10 @@ install-lean-repl ```bash install-itp-interface ``` +>NOTE: `install-itp-interface` also respects the `LEAN_VERSION` environment variable to determine which Lean version to compile the tactic parser with. It defaults to `4.24.0` when not set. **Both `install-lean-repl` and `install-itp-interface` must use the same `LEAN_VERSION`** — mismatching versions will cause elaboration errors at runtime. If you set `LEAN_VERSION` for one, set it for both: +```bash +export LEAN_VERSION="4.30.0" && install-lean-repl && install-itp-interface +``` >NOTE: These steps are only tested on Linux. For Windows, you can use WSL. These steps will not setup the Coq interface. diff --git a/src/itp_interface/lean/tactic_parser.py b/src/itp_interface/lean/tactic_parser.py index fa0626e..da990dc 100644 --- a/src/itp_interface/lean/tactic_parser.py +++ b/src/itp_interface/lean/tactic_parser.py @@ -290,7 +290,7 @@ def get_path_to_tactic_parser_executable() -> str: return tactic_parser_bin_path def toolchain_version_and_env_version(): - lean_version_needed = os.getenv("LEAN_VERSION", None) + lean_version_needed = os.getenv("LEAN_VERSION", "4.24.0") tactic_parser_project = get_path_to_tactic_parser_project() # Check the version of the built parser toolchain_file = os.path.join(tactic_parser_project, "lean-toolchain")