python 314 support and perf improvments for GIL free usage.

.github/workflows/github-build-actions-python314t.yaml

@@ -0,0 +1,119 @@
+name: Build, Package, and Test (Python 3.14 Free-Threading)
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+jobs:
+  build-test-python314t:
+    runs-on: ubuntu-latest
+    container:
+      image: coqorg/coq:8.18.0-ocaml-4.14.2-flambda
+      options: --user 0  # Running as root; no sudo needed
+    env:
+      HOME: /root
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v3
+        with:
+          submodules: true  # Ensure submodules are checked out
+
+      - name: Install Miniconda
+        shell: bash
+        run: |
+          apt-get update
+          apt-get install -y wget
+          wget https://repo.anaconda.com/miniconda/Miniconda3-latest-Linux-x86_64.sh -O /tmp/miniconda.sh
+          bash /tmp/miniconda.sh -b -p $HOME/miniconda
+          rm /tmp/miniconda.sh
+          export PATH="$HOME/miniconda/bin:$PATH"
+          conda init bash
+
+      - name: Create Python 3.14 free-threading conda environment
+        shell: bash
+        run: |
+          export PATH="$HOME/miniconda/bin:$PATH"
+          conda create -n py314-ft python=3.14 python-freethreading -c conda-forge -y
+
+      - name: Check Python version and GIL status
+        shell: bash
+        run: |
+          export PATH="$HOME/miniconda/bin:$PATH"
+          source $HOME/miniconda/bin/activate py314-ft
+          python --version
+          python -c "import sys; print('GIL disabled:', not sys._is_gil_enabled())"
+
+      - name: Upgrade pip and install build tools
+        shell: bash
+        run: |
+          export PATH="$HOME/miniconda/bin:$PATH"
+          source $HOME/miniconda/bin/activate py314-ft
+          python -m pip install --upgrade pip
+          pip install build==1.3.0 hatchling==1.27.0
+
+      - name: Build package with hatchling
+        shell: bash
+        run: |
+          export PATH="$HOME/miniconda/bin:$PATH"
+          source $HOME/miniconda/bin/activate py314-ft
+          python -m build
+
+      - name: Install package
+        shell: bash
+        run: |
+          export PATH="$HOME/miniconda/bin:$PATH"
+          source $HOME/miniconda/bin/activate py314-ft
+          pip install dist/*.whl
+
+      - name: Install Lean (elan) and prepare Lean REPL
+        shell: bash
+        run: |
+          export PATH="$HOME/miniconda/bin:$PATH"
+          source $HOME/miniconda/bin/activate py314-ft
+          install-lean-repl
+          source $HOME/.elan/env
+
+      - name: Build Lean REPL for itp-interface
+        shell: bash
+        run: |
+          export PATH="$HOME/miniconda/bin:$PATH"
+          source $HOME/miniconda/bin/activate py314-ft
+          source $HOME/.elan/env
+          install-itp-interface
+
+      - name: Check and Init opam version
+        run: |
+          opam --version
+          opam init --disable-sandboxing --yes
+
+      - name: Install Coq
+        run: |
+          opam switch create simple_grp_theory 4.14.2
+          opam switch simple_grp_theory
+          eval $(opam env)
+          opam repo add coq-released https://coq.inria.fr/opam/released
+          opam pin add -y coq-lsp 0.1.8+8.18
+
+      - name: List repository files (debug step)
+        run: find . -type f
+
+      - name: Run Simple Env Test
+        shell: bash
+        run: |
+          export PATH="$HOME/miniconda/bin:$PATH"
+          source $HOME/miniconda/bin/activate py314-ft
+          eval $(opam env)
+          source $HOME/.elan/env
+          python src/test/simple_env_test.py
+
+      - name: Run Data Gen Test
+        shell: bash
+        run: |
+          export PATH="$HOME/miniconda/bin:$PATH"
+          source $HOME/miniconda/bin/activate py314-ft
+          eval $(opam env)
+          source $HOME/.elan/env
+          python src/test/simple_data_gen_test.py

.gitignore

@@ -193,4 +193,4 @@ api_log.json
 temptodel*
 
 .repo/
-.conda/
+.conda*

README.md

@@ -3,22 +3,24 @@
 [![PyPI downloads](https://img.shields.io/pypi/dm/itp-interface.svg)](https://pypi.org/project/itp-interface/)
 
 # itp-interface
-Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving. 
+Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving.
+
+## 🎉 What's New
+
+**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:
 1. Install itp-interface using the following command:
 ```bash
 pip install itp-interface
 ```
 
-2. Run the following command to prepare the REPL for Lean 4. The default version is 4.7.0-rc2. You can change the version by setting the `LEAN_VERSION` environment variable. If no version is set, then 4.7.0-rc2 is used. However, the itp-interface supports up to Lean 4.17.0.
+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.
 ```bash
-export LEAN_VERSION="4.7.0-rc2"
 install-lean-repl
-# ^^ Change the LEAN_VERSION to the version of Lean 4 you are working with.
-# ^^^ Example: export LEAN_VERSION="4.15.0" to use Lean 4.15.0
-# itp-interface supports up to Lean 4.17.0
+# To use a different Lean version, set LEAN_VERSION before running:
+# export LEAN_VERSION="4.17.0" && install-lean-repl
 ```
 
 3. Run the following command to build the REPL for Lean 4. Make sure that `lean --version` returns the correct version before running the command below. If not then check if `$HOME/.elan/bin` is in your path. Recommended to run `source $HOME/.elan/env` before running the command below.
@@ -44,6 +46,26 @@ export PATH="/home/$USER/.opam/default/bin:$PATH"
 
 4. Create a `Miniconda` environment and activate it.
 
+### Python 3.14 Free-Threading Support (Optional)
+
+For Python 3.14 with free-threading (GIL-free) support, create a conda environment using:
+```bash
+conda create -n py314-ft python=3.14 python-freethreading -c conda-forge
+conda activate py314-ft
+```
+
+This enables true parallel execution for computational threads. You can verify free-threading is working by running:
+```bash
+python src/test/test_python314_threading.py
+```
+
+**Note**: When using Python 3.14 free-threading:
+- Ray is not supported (Ray doesn't support Python 3.14 yet)
+- The interface will automatically fall back to thread-based parallelism using `ThreadPoolExecutor`
+- `psutil` is not available in free-threading builds, so memory logging is disabled
+- **Isabelle/PISA is not supported** - grpcio and protobuf are not compatible with Python 3.14's free-threading mode. Use Python < 3.14 for Isabelle support
+- The `run-itp-data-gen` command now auto-detects Python version and uses Hydra-free mode for Python 3.14+
+
 5. Run the commands for installing the Lean 4 interface as mentioned in [Quick Setup for Lean 4](#quick-setup-for-lean-4).
 
 6. Add the following to your `.bashrc` file for Lean:

pyproject.toml

@@ -5,13 +5,13 @@ requires = [
 build-backend = "hatchling.build"
 [project]
 name = "itp_interface"
-version = "1.1.12"
+version = "1.1.13"
 authors = [
   { name="Amitayush Thakur", email="[email protected]" },
 ]
 description = "Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving."
 readme = "README.md"
-requires-python = ">=3.9, <3.13"
+requires-python = ">=3.9"
 classifiers = [
     "Programming Language :: Python :: 3",
     "License :: OSI Approved :: MIT License",
@@ -25,7 +25,7 @@ dependencies = [
     "pexpect==4.8.0",
     "sexpdata==1.0.0",
     "pampy==0.3.0",
-    "ray==2.36.0",
+    "ray>=2.50.0; python_version<'3.14'",
     "pydantic>=2.10.6",
     "faiss-cpu>=1.6.1",
     "filelock==3.12.4",
@@ -38,12 +38,11 @@ dependencies = [
     "soundfile==0.12.1",
     "rank_bm25==0.2.2",
     "parglare==0.16.1",
-    "psutil==5.9.8",
     "urllib3>=2.0.7",
     "mathlibtools==1.3.2",
     "pylspclient==0.0.3",
-    "protobuf==3.20.3",
-    "grpcio>=1.51.3"
+    "protobuf==3.20.3; python_version<'3.14'",
+    "grpcio>=1.51.3; python_version<'3.14'"
 ]
 
 [project.urls]
@@ -53,4 +52,4 @@ Issues = "https://github.com/trishullab/itp-interface/issues"
 [project.scripts]
 install-itp-interface = "itp_interface.main.install:install_itp_interface"
 install-lean-repl = "itp_interface.main.install:install_lean_repl"
-run-itp-data-gen = "itp_interface.main.run_tool:main"
+run-itp-data-gen = "itp_interface.main.run_tool_no_hydra:main"

src/data/test/lean4_proj/lake-manifest.json

@@ -1,68 +1,95 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "e5306c3b0edefe722370b7387ee9bcd4631d6c17",
-   "name": "std",
+   "scope": "",
+   "rev": "a0187b2361a9c9b82580bb0d68c25e16f9e96a9e",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
-   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
-   "name": "Qq",
+   "scope": "leanprover-community",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "8be30c25e3caa06937feeb62f7ca898370f80ee9",
-   "name": "aesop",
+   "scope": "leanprover-community",
+   "rev": "d768126816be17600904726ca7976b185786e6b9",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "scope": "leanprover-community",
+   "rev": "556caed0eadb7901e068131d1be208dd907d07a2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.74",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
-   "name": "Cli",
+   "scope": "leanprover-community",
+   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
-   "name": "importGraph",
+   "scope": "leanprover-community",
+   "rev": "2676cb5599c12c434daac781e2cea44e8105fc41",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "fe4454af900584467d21f4fd4fe951d29d9332a7",
-   "name": "mathlib",
+   "scope": "leanprover",
+   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "lean4_proj",
  "lakeDir": ".lake"}

src/data/test/lean4_proj/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0-rc2
+leanprover/lean4:v4.24.0