Update Python environment setup and support Lean 4 v4.30.0

.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

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:
@@ -16,7 +18,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
@@ -28,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.
 

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" },
 ]

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")

src/itp_interface/lean/tactic_parser/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.30.0