From 80c98aecbc554d1940bab47023f141ae57d7bd71 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Tue, 9 Jun 2026 09:47:48 -0500 Subject: [PATCH 1/6] Update itp-interface dependency version to 1.7.0 --- pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyproject.toml b/pyproject.toml index 31929b5..1cc7e60 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -24,7 +24,7 @@ classifiers = [ ] dependencies = [ - "itp-interface>=1.6.0", + "itp-interface>=1.7.0", "openai>=1.99.1", "tiktoken>=0.12.0", # Updated: 0.4.0 incompatible with Python 3.14t, needs PyO3 0.23+ for free-threading "sentencepiece>=0.2.0", # Updated: 0.1.99 lacks Python 3.14t wheels, 0.2.1 has cp314t support From 8c2f93132a48cac01b51adb2ab63f7c3f1428b1f Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 14 Jun 2026 14:39:35 -0500 Subject: [PATCH 2/6] Update CI workflow to include OPENAI_API_KEY and modify build steps --- .github/workflows/ci.yaml | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 40bbcc0..5cadc96 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -9,6 +9,8 @@ on: jobs: build-and-test: runs-on: ubuntu-latest + env: + OPENAI_API_KEY: ${{ secrets.OPENAI_API_KEY }} steps: - name: Checkout repository @@ -66,13 +68,8 @@ jobs: - name: Build the lean project run: | source $HOME/.elan/env - pushd data/test/lean4_proj && lake build && popd + pushd data/test/lean4_proj && lake exe cache get && lake build && popd - - name: Create secrets - run: | - mkdir -p .secrets - echo ${{ secrets.OPENAI }} | base64 -d > .secrets/openai_key.json - - name: Run CI setup tests (sequential) run: | source $HOME/.elan/env @@ -98,8 +95,3 @@ jobs: source $HOME/.elan/env export LEAN_VERSION="4.21.0" python src/tests/test_simple_cli.py - - - name: Remove secrets - run: | - rm -rf .secrets - ls -la From e3ea89bb30bcb9074b1e0c6faed6ecaa15d850a3 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 14 Jun 2026 14:41:04 -0500 Subject: [PATCH 3/6] Update GitHub Actions workflow to include API key Added OPENAI_API_KEY as an environment variable and removed secret handling steps. --- .../workflows/github-build-actions-python314t.yaml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/.github/workflows/github-build-actions-python314t.yaml b/.github/workflows/github-build-actions-python314t.yaml index 3be3180..6d8a646 100644 --- a/.github/workflows/github-build-actions-python314t.yaml +++ b/.github/workflows/github-build-actions-python314t.yaml @@ -9,6 +9,8 @@ on: jobs: build-test-python314t: runs-on: ubuntu-latest + env: + OPENAI_API_KEY: ${{ secrets.OPENAI_API_KEY }} steps: - name: Checkout repository @@ -98,11 +100,6 @@ jobs: source $HOME/.elan/env pushd data/test/lean4_proj && lake build && popd - - name: Create secrets - run: | - mkdir -p .secrets - echo ${{ secrets.OPENAI }} | base64 -d > .secrets/openai_key.json - - name: Run CI setup tests (sequential) shell: bash run: | @@ -144,8 +141,3 @@ jobs: source $HOME/miniconda/bin/activate py314-ft echo "Python 3.14t parallel execution uses threading (not multiprocessing)" python -c "import sys; print(f'Python: {sys.version_info.major}.{sys.version_info.minor}'); print(f'GIL enabled: {sys._is_gil_enabled()}'); print(f'Free-threading: {not sys._is_gil_enabled()}')" - - - name: Remove secrets - run: | - rm -rf .secrets - ls -la From 5b3ea3c66c21113c95dbd08c816677570b4b5313 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 14 Jun 2026 14:41:59 -0500 Subject: [PATCH 4/6] Bump version to 1.8.0 and update dependencies --- pyproject.toml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pyproject.toml b/pyproject.toml index 1cc7e60..d149cde 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -10,7 +10,7 @@ packages = ["src/copra"] [project] name = "copra-theorem-prover" -version = "1.7.0" +version = "1.8.0" authors = [ { name="Amitayush Thakur", email="amitayush@utexas.edu" }, ] @@ -24,7 +24,7 @@ classifiers = [ ] dependencies = [ - "itp-interface>=1.7.0", + "itp-interface>=1.8.0", "openai>=1.99.1", "tiktoken>=0.12.0", # Updated: 0.4.0 incompatible with Python 3.14t, needs PyO3 0.23+ for free-threading "sentencepiece>=0.2.0", # Updated: 0.1.99 lacks Python 3.14t wheels, 0.2.1 has cp314t support @@ -41,7 +41,7 @@ dependencies = [ [project.optional-dependencies] os_models = [ - "vllm>=0.11.0; python_version < '3.13'", # Optional: Open-source model support with vLLM (requires Python ≤ 3.12) + "vllm>=0.19.0; python_version < '3.13'", # Optional: Open-source model support with vLLM (requires Python ≤ 3.12) ] gpt_oss = [ "vllm==0.10.2" From ebb1f61754d1f72a8303f17cf98bf3a336156342 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 14 Jun 2026 15:56:50 -0500 Subject: [PATCH 5/6] Bump version to 1.9.0 and update itp-interface dependency to 1.9.0 --- pyproject.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyproject.toml b/pyproject.toml index d149cde..fc1134d 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -10,7 +10,7 @@ packages = ["src/copra"] [project] name = "copra-theorem-prover" -version = "1.8.0" +version = "1.9.0" authors = [ { name="Amitayush Thakur", email="amitayush@utexas.edu" }, ] @@ -24,7 +24,7 @@ classifiers = [ ] dependencies = [ - "itp-interface>=1.8.0", + "itp-interface>=1.9.0", "openai>=1.99.1", "tiktoken>=0.12.0", # Updated: 0.4.0 incompatible with Python 3.14t, needs PyO3 0.23+ for free-threading "sentencepiece>=0.2.0", # Updated: 0.1.99 lacks Python 3.14t wheels, 0.2.1 has cp314t support From afe100363124b0b40eed0eda68ff442129a06dd8 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 14 Jun 2026 16:03:24 -0500 Subject: [PATCH 6/6] Set ITP_DEP_PARSER_MEM_LIMIT environment variable to accommodate CI memory constraints --- src/tests/simple_copra_run.py | 1 + src/tests/test_simple_cli.py | 1 + 2 files changed, 2 insertions(+) diff --git a/src/tests/simple_copra_run.py b/src/tests/simple_copra_run.py index 534223a..8cb6fc4 100644 --- a/src/tests/simple_copra_run.py +++ b/src/tests/simple_copra_run.py @@ -14,6 +14,7 @@ def test_simple_copra_run(self): # Parse hydra configs from src/copra/main/config # Initialize Hydra and compose the config os.environ["LEAN_VERSION"] = "4.21.0" + os.environ["ITP_DEP_PARSER_MEM_LIMIT"] = "0.9" # CI runners have limited RAM; allow up to 90% parent_dir = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) root_dir = os.path.dirname(parent_dir) full_path = os.path.join(root_dir, "src/copra/main/config") diff --git a/src/tests/test_simple_cli.py b/src/tests/test_simple_cli.py index 609233d..ce67f39 100644 --- a/src/tests/test_simple_cli.py +++ b/src/tests/test_simple_cli.py @@ -14,6 +14,7 @@ def setUpClass(cls): # Set Lean version to match test project (optional, defaults to 4.24.0) # The test project uses 4.21.0 (see data/test/lean4_proj/lean-toolchain) os.environ["LEAN_VERSION"] = "4.21.0" + os.environ["ITP_DEP_PARSER_MEM_LIMIT"] = "0.9" # CI runners have limited RAM; allow up to 90% # Define test project paths cls.test_project = "data/test/lean4_proj"