Update itp-interface dependency version to 1.9.0

.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

.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

pyproject.toml

@@ -10,7 +10,7 @@ packages = ["src/copra"]
 
 [project]
 name = "copra-theorem-prover"
-version = "1.7.0"
+version = "1.9.0"
 authors = [
   { name="Amitayush Thakur", email="amitayush@utexas.edu" },
 ]
@@ -24,7 +24,7 @@ classifiers = [
 ]
 
 dependencies = [
-    "itp-interface>=1.6.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
@@ -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"

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

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"