Skip to content

Commit 615c69f

Browse files
amit9octamit9oct
authored
Merge pull request #58 from trishullab/feature/python_314_support
python 314 support and perf improvments for GIL free usage.
2 parents b3d42f5 + c81d8fb commit 615c69f

31 files changed

+2730
-3925
lines changed

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

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
name: Build, Package, and Test (Python 3.14 Free-Threading)
2+
3+
on:
4+
push:
5+
branches: [main]
6+
pull_request:
7+
branches: [main]
8+
9+
jobs:
10+
build-test-python314t:
11+
runs-on: ubuntu-latest
12+
container:
13+
image: coqorg/coq:8.18.0-ocaml-4.14.2-flambda
14+
options: --user 0 # Running as root; no sudo needed
15+
env:
16+
HOME: /root
17+
18+
steps:
19+
- name: Checkout repository
20+
uses: actions/checkout@v3
21+
with:
22+
submodules: true # Ensure submodules are checked out
23+
24+
- name: Install Miniconda
25+
shell: bash
26+
run: |
27+
apt-get update
28+
apt-get install -y wget
29+
wget https://repo.anaconda.com/miniconda/Miniconda3-latest-Linux-x86_64.sh -O /tmp/miniconda.sh
30+
bash /tmp/miniconda.sh -b -p $HOME/miniconda
31+
rm /tmp/miniconda.sh
32+
export PATH="$HOME/miniconda/bin:$PATH"
33+
conda init bash
34+
35+
- name: Create Python 3.14 free-threading conda environment
36+
shell: bash
37+
run: |
38+
export PATH="$HOME/miniconda/bin:$PATH"
39+
conda create -n py314-ft python=3.14 python-freethreading -c conda-forge -y
40+
41+
- name: Check Python version and GIL status
42+
shell: bash
43+
run: |
44+
export PATH="$HOME/miniconda/bin:$PATH"
45+
source $HOME/miniconda/bin/activate py314-ft
46+
python --version
47+
python -c "import sys; print('GIL disabled:', not sys._is_gil_enabled())"
48+
49+
- name: Upgrade pip and install build tools
50+
shell: bash
51+
run: |
52+
export PATH="$HOME/miniconda/bin:$PATH"
53+
source $HOME/miniconda/bin/activate py314-ft
54+
python -m pip install --upgrade pip
55+
pip install build==1.3.0 hatchling==1.27.0
56+
57+
- name: Build package with hatchling
58+
shell: bash
59+
run: |
60+
export PATH="$HOME/miniconda/bin:$PATH"
61+
source $HOME/miniconda/bin/activate py314-ft
62+
python -m build
63+
64+
- name: Install package
65+
shell: bash
66+
run: |
67+
export PATH="$HOME/miniconda/bin:$PATH"
68+
source $HOME/miniconda/bin/activate py314-ft
69+
pip install dist/*.whl
70+
71+
- name: Install Lean (elan) and prepare Lean REPL
72+
shell: bash
73+
run: |
74+
export PATH="$HOME/miniconda/bin:$PATH"
75+
source $HOME/miniconda/bin/activate py314-ft
76+
install-lean-repl
77+
source $HOME/.elan/env
78+
79+
- name: Build Lean REPL for itp-interface
80+
shell: bash
81+
run: |
82+
export PATH="$HOME/miniconda/bin:$PATH"
83+
source $HOME/miniconda/bin/activate py314-ft
84+
source $HOME/.elan/env
85+
install-itp-interface
86+
87+
- name: Check and Init opam version
88+
run: |
89+
opam --version
90+
opam init --disable-sandboxing --yes
91+
92+
- name: Install Coq
93+
run: |
94+
opam switch create simple_grp_theory 4.14.2
95+
opam switch simple_grp_theory
96+
eval $(opam env)
97+
opam repo add coq-released https://coq.inria.fr/opam/released
98+
opam pin add -y coq-lsp 0.1.8+8.18
99+
100+
- name: List repository files (debug step)
101+
run: find . -type f
102+
103+
- name: Run Simple Env Test
104+
shell: bash
105+
run: |
106+
export PATH="$HOME/miniconda/bin:$PATH"
107+
source $HOME/miniconda/bin/activate py314-ft
108+
eval $(opam env)
109+
source $HOME/.elan/env
110+
python src/test/simple_env_test.py
111+
112+
- name: Run Data Gen Test
113+
shell: bash
114+
run: |
115+
export PATH="$HOME/miniconda/bin:$PATH"
116+
source $HOME/miniconda/bin/activate py314-ft
117+
eval $(opam env)
118+
source $HOME/.elan/env
119+
python src/test/simple_data_gen_test.py

‎.gitignore‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -193,4 +193,4 @@ api_log.json
193193
temptodel*
194194

195195
.repo/
196-
.conda/
196+
.conda*

‎README.md‎

Lines changed: 28 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,22 +3,24 @@
33
[![PyPI downloads](https://img.shields.io/pypi/dm/itp-interface.svg)](https://pypi.org/project/itp-interface/)
44

55
# itp-interface
6-
Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving.
6+
Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving.
7+
8+
## 🎉 What's New
9+
10+
**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.
711

812
## Quick Setup for Lean 4:
913
1. Install itp-interface using the following command:
1014
```bash
1115
pip install itp-interface
1216
```
1317

14-
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.
18+
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.
1519
>NOTE: The Lean 4 version must match the version of the Lean 4 project you are working with.
1620
```bash
17-
export LEAN_VERSION="4.7.0-rc2"
1821
install-lean-repl
19-
# ^^ Change the LEAN_VERSION to the version of Lean 4 you are working with.
20-
# ^^^ Example: export LEAN_VERSION="4.15.0" to use Lean 4.15.0
21-
# itp-interface supports up to Lean 4.17.0
22+
# To use a different Lean version, set LEAN_VERSION before running:
23+
# export LEAN_VERSION="4.17.0" && install-lean-repl
2224
```
2325

2426
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"
4446

4547
4. Create a `Miniconda` environment and activate it.
4648

49+
### Python 3.14 Free-Threading Support (Optional)
50+
51+
For Python 3.14 with free-threading (GIL-free) support, create a conda environment using:
52+
```bash
53+
conda create -n py314-ft python=3.14 python-freethreading -c conda-forge
54+
conda activate py314-ft
55+
```
56+
57+
This enables true parallel execution for computational threads. You can verify free-threading is working by running:
58+
```bash
59+
python src/test/test_python314_threading.py
60+
```
61+
62+
**Note**: When using Python 3.14 free-threading:
63+
- Ray is not supported (Ray doesn't support Python 3.14 yet)
64+
- The interface will automatically fall back to thread-based parallelism using `ThreadPoolExecutor`
65+
- `psutil` is not available in free-threading builds, so memory logging is disabled
66+
- **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
67+
- The `run-itp-data-gen` command now auto-detects Python version and uses Hydra-free mode for Python 3.14+
68+
4769
5. Run the commands for installing the Lean 4 interface as mentioned in [Quick Setup for Lean 4](#quick-setup-for-lean-4).
4870

4971
6. Add the following to your `.bashrc` file for Lean:

‎pyproject.toml‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,13 @@ requires = [
55
build-backend = "hatchling.build"
66
[project]
77
name = "itp_interface"
8-
version = "1.1.12"
8+
version = "1.1.13"
99
authors = [
1010
{ name="Amitayush Thakur", email="[email protected]" },
1111
]
1212
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."
1313
readme = "README.md"
14-
requires-python = ">=3.9, <3.13"
14+
requires-python = ">=3.9"
1515
classifiers = [
1616
"Programming Language :: Python :: 3",
1717
"License :: OSI Approved :: MIT License",
@@ -25,7 +25,7 @@ dependencies = [
2525
"pexpect==4.8.0",
2626
"sexpdata==1.0.0",
2727
"pampy==0.3.0",
28-
"ray==2.36.0",
28+
"ray>=2.50.0; python_version<'3.14'",
2929
"pydantic>=2.10.6",
3030
"faiss-cpu>=1.6.1",
3131
"filelock==3.12.4",
@@ -38,12 +38,11 @@ dependencies = [
3838
"soundfile==0.12.1",
3939
"rank_bm25==0.2.2",
4040
"parglare==0.16.1",
41-
"psutil==5.9.8",
4241
"urllib3>=2.0.7",
4342
"mathlibtools==1.3.2",
4443
"pylspclient==0.0.3",
45-
"protobuf==3.20.3",
46-
"grpcio>=1.51.3"
44+
"protobuf==3.20.3; python_version<'3.14'",
45+
"grpcio>=1.51.3; python_version<'3.14'"
4746
]
4847

4948
[project.urls]
@@ -53,4 +52,4 @@ Issues = "https://github.com/trishullab/itp-interface/issues"
5352
[project.scripts]
5453
install-itp-interface = "itp_interface.main.install:install_itp_interface"
5554
install-lean-repl = "itp_interface.main.install:install_lean_repl"
56-
run-itp-data-gen = "itp_interface.main.run_tool:main"
55+
run-itp-data-gen = "itp_interface.main.run_tool_no_hydra:main"

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

Lines changed: 59 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,68 +1,95 @@
1-
{"version": 7,
1+
{"version": "1.1.0",
22
"packagesDir": ".lake/packages",
33
"packages":
4-
[{"url": "https://github.com/leanprover/std4",
4+
[{"url": "https://github.com/leanprover-community/mathlib4.git",
55
"type": "git",
66
"subDir": null,
7-
"rev": "e5306c3b0edefe722370b7387ee9bcd4631d6c17",
8-
"name": "std",
7+
"scope": "",
8+
"rev": "a0187b2361a9c9b82580bb0d68c25e16f9e96a9e",
9+
"name": "mathlib",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": null,
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/leanprover-community/plausible",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "leanprover-community",
18+
"rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805",
19+
"name": "plausible",
920
"manifestFile": "lake-manifest.json",
1021
"inputRev": "main",
1122
"inherited": true,
12-
"configFile": "lakefile.lean"},
13-
{"url": "https://github.com/leanprover-community/quote4",
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
1425
"type": "git",
1526
"subDir": null,
16-
"rev": "fd760831487e6835944e7eeed505522c9dd47563",
17-
"name": "Qq",
27+
"scope": "leanprover-community",
28+
"rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
29+
"name": "LeanSearchClient",
1830
"manifestFile": "lake-manifest.json",
19-
"inputRev": "master",
31+
"inputRev": "main",
2032
"inherited": true,
21-
"configFile": "lakefile.lean"},
22-
{"url": "https://github.com/leanprover-community/aesop",
33+
"configFile": "lakefile.toml"},
34+
{"url": "https://github.com/leanprover-community/import-graph",
2335
"type": "git",
2436
"subDir": null,
25-
"rev": "8be30c25e3caa06937feeb62f7ca898370f80ee9",
26-
"name": "aesop",
37+
"scope": "leanprover-community",
38+
"rev": "d768126816be17600904726ca7976b185786e6b9",
39+
"name": "importGraph",
2740
"manifestFile": "lake-manifest.json",
28-
"inputRev": "master",
41+
"inputRev": "main",
2942
"inherited": true,
30-
"configFile": "lakefile.lean"},
43+
"configFile": "lakefile.toml"},
3144
{"url": "https://github.com/leanprover-community/ProofWidgets4",
3245
"type": "git",
3346
"subDir": null,
34-
"rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
47+
"scope": "leanprover-community",
48+
"rev": "556caed0eadb7901e068131d1be208dd907d07a2",
3549
"name": "proofwidgets",
3650
"manifestFile": "lake-manifest.json",
37-
"inputRev": "v0.0.30",
51+
"inputRev": "v0.0.74",
3852
"inherited": true,
3953
"configFile": "lakefile.lean"},
40-
{"url": "https://github.com/leanprover/lean4-cli",
54+
{"url": "https://github.com/leanprover-community/aesop",
4155
"type": "git",
4256
"subDir": null,
43-
"rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
44-
"name": "Cli",
57+
"scope": "leanprover-community",
58+
"rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
59+
"name": "aesop",
4560
"manifestFile": "lake-manifest.json",
46-
"inputRev": "main",
61+
"inputRev": "master",
4762
"inherited": true,
48-
"configFile": "lakefile.lean"},
49-
{"url": "https://github.com/leanprover-community/import-graph.git",
63+
"configFile": "lakefile.toml"},
64+
{"url": "https://github.com/leanprover-community/quote4",
5065
"type": "git",
5166
"subDir": null,
52-
"rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
53-
"name": "importGraph",
67+
"scope": "leanprover-community",
68+
"rev": "2676cb5599c12c434daac781e2cea44e8105fc41",
69+
"name": "Qq",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "master",
72+
"inherited": true,
73+
"configFile": "lakefile.toml"},
74+
{"url": "https://github.com/leanprover-community/batteries",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
79+
"name": "batteries",
5480
"manifestFile": "lake-manifest.json",
5581
"inputRev": "main",
5682
"inherited": true,
57-
"configFile": "lakefile.lean"},
58-
{"url": "https://github.com/leanprover-community/mathlib4.git",
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover/lean4-cli",
5985
"type": "git",
6086
"subDir": null,
61-
"rev": "fe4454af900584467d21f4fd4fe951d29d9332a7",
62-
"name": "mathlib",
87+
"scope": "leanprover",
88+
"rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
89+
"name": "Cli",
6390
"manifestFile": "lake-manifest.json",
64-
"inputRev": null,
65-
"inherited": false,
66-
"configFile": "lakefile.lean"}],
91+
"inputRev": "main",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"}],
6794
"name": "lean4_proj",
6895
"lakeDir": ".lake"}

‎src/data/test/lean4_proj/lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.7.0-rc2
1+
leanprover/lean4:v4.24.0

0 commit comments

Comments
 (0)