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 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 diff --git a/pyproject.toml b/pyproject.toml index 31929b5..fc1134d 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.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" 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"