Add CI/CD: GitHub Actions workflow + ruff config

New .github/workflows/ci.yml with three jobs:
- lint: ruff check on every push/PR (fast, no project deps)
- test: pytest over the ~98-test suite on every push/PR
- deploy: on push to main only, pushes to the HF Space (gated on an
HF_TOKEN secret — skips cleanly if the secret isn't set)

Supporting changes to make the suite CI-green:
- ruff.toml: line-length 120; ignore E402 (sys.path.insert-before-import
is intentional in tests/scripts) and E741; exclude web/, data/, .claude/.
- Fixed test isolation: test_proof_agent.py and test_app_fuzz.py
permanently overwrote sys.modules["langgraph_agent"] with a mock and
never restored it, poisoning every later test file (31 failures in a
full run). They now restore sys.modules after importing their target.
- test_retriever_fuzz.py: force a fresh `retriever` import so a cached
real module from another test file can't shadow its mocks.
- test_lean_verifier.py: skipUnless(`lean` on PATH) so the 3 real-Lean
tests skip on CI runners instead of erroring.
- Updated stale assertions: proof_agent default model is now
llama-3.3-70b-versatile; retrieve() returns [] (not RuntimeError) when
no index exists.
- ruff --fix applied across src/scripts/tests (import sorting, trailing
whitespace, unused imports). Full suite: 98 passed locally.
- .gitignore for __pycache__, benchmark CSVs, caches.

.github/workflows/ci.yml

@@ -0,0 +1,70 @@
+name: CI
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+jobs:
+  lint:
+    name: Lint (ruff)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+      - name: Install ruff
+        run: pip install ruff
+      - name: ruff check
+        run: ruff check .
+
+  test:
+    name: Test (pytest)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+          cache: pip
+      - name: Install dependencies
+        run: |
+          python -m pip install --upgrade pip
+          pip install -r requirements.txt
+          pip install pytest
+      - name: Run pytest
+        # The 3 real-Lean tests in test_lean_verifier.py self-skip when no
+        # `lean` toolchain is on PATH (CI runners have none); the other ~95
+        # tests use mocks and run everywhere.
+        run: pytest tests/ -v
+
+  deploy:
+    name: Deploy to Hugging Face Spaces
+    needs: [lint, test]
+    # Only deploy on a real push to main — never on pull requests.
+    if: github.ref == 'refs/heads/main' && github.event_name == 'push'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check HF_TOKEN is configured
+        id: gate
+        run: |
+          if [ -n "${{ secrets.HF_TOKEN }}" ]; then
+            echo "ok=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "ok=false" >> "$GITHUB_OUTPUT"
+            echo "::notice::HF_TOKEN secret not set — skipping Hugging Face Spaces deploy."
+          fi
+      - name: Checkout (with Git LFS)
+        if: steps.gate.outputs.ok == 'true'
+        uses: actions/checkout@v4
+        with:
+          lfs: true
+          fetch-depth: 0
+      - name: Push to Hugging Face Spaces
+        if: steps.gate.outputs.ok == 'true'
+        run: |
+          git push --force \
+            "https://Ray5th:${{ secrets.HF_TOKEN }}@huggingface.co/spaces/Ray5th/lean4-helper" \
+            HEAD:main

.gitignore

@@ -0,0 +1,16 @@
+# Python
+__pycache__/
+*.py[cod]
+*.egg-info/
+.pytest_cache/
+.ruff_cache/
+
+# Claude Code
+.claude/
+
+# Benchmark run artifacts
+benchmark_*.csv
+benchmark_results.csv
+
+# OS
+.DS_Store

app.py

@@ -12,7 +12,6 @@ from langgraph_agent import LangGraphAgent
 from lean_verifier import LeanEnvironment
 from retriever import MathLibRetriever
 
-
 # ---------------------------------------------------------------------------
 # Cached heavyweight components.
 #

ruff.toml

@@ -0,0 +1,19 @@
+# Ruff configuration for lean4-helper.
+line-length = 120
+
+# Untracked / generated dirs that shouldn't be linted.
+exclude = [
+    "web",
+    ".claude",
+    "__pycache__",
+    "data",
+]
+
+[lint]
+# Default rule set (pyflakes F + pycodestyle E/W) plus import sorting.
+select = ["E", "F", "W", "I"]
+
+# E402 (module import not at top of file) is intentional throughout: test
+# files and scripts run `sys.path.insert(0, "src")` before importing local
+# modules. E741 (ambiguous name `l`) is a cosmetic nit we accept.
+ignore = ["E402", "E741"]

scripts/benchmark.py

@@ -225,8 +225,12 @@ def main():
     parser.add_argument("--index-dir", default=None,         help="Path to pre-built FAISS index")
     parser.add_argument("--output",  default="benchmark_results.csv", help="CSV output path")
     parser.add_argument("--verbose", action="store_true",    help="Print per-problem results")
-    parser.add_argument("--api-key", default=None,           help="API key for the chosen provider (Anthropic for Claude models). Falls back to ANTHROPIC_API_KEY / GROQ_API_KEY env.")
-    parser.add_argument("--problems-dir", default=None,      help="Use local .lean files in this directory instead of MiniF2F. Each file is one problem.")
+    parser.add_argument("--api-key", default=None,
+                        help="API key for the chosen provider (Anthropic for Claude models). "
+                             "Falls back to ANTHROPIC_API_KEY / GROQ_API_KEY env.")
+    parser.add_argument("--problems-dir", default=None,
+                        help="Use local .lean files in this directory instead of MiniF2F. "
+                             "Each file is one problem.")
     args = parser.parse_args()
 
     if args.problems_dir:

scripts/build_index.py

@@ -10,9 +10,9 @@ Optional flags:
     --max-files N         Limit to first N .lean files (useful for quick testing)
     --index-dir PATH      Where to save the index (default: data/mathlib_index)
 """
-import sys
-import os
 import argparse
+import os
+import sys
 
 sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), '..', 'src')))
 

scripts/run_agent.py

@@ -1,7 +1,7 @@
 #!/usr/bin/env python3
-import sys
-import os
 import argparse
+import os
+import sys
 
 sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), '..', 'src')))
 

src/langgraph_agent.py

@@ -3,12 +3,10 @@ import re
 from typing import List, TypedDict
 
 from langgraph.graph import END, StateGraph
-
 from lean_verifier import LeanEnvironment
 from rag_chain import RAGProofChain
 from retriever import MathLibRetriever
 
-
 # ---------------------------------------------------------------------------
 # State
 # ---------------------------------------------------------------------------

src/lean_verifier.py

@@ -1,7 +1,7 @@
 import threading
-from typing import Dict, Any, List
+from typing import Any, Dict
 
-from lean_interact import LeanREPLConfig, LeanServer, Command, TempRequireProject, LeanRequire
+from lean_interact import Command, LeanREPLConfig, LeanServer, TempRequireProject
 
 
 class LeanEnvironment:
@@ -16,7 +16,7 @@ class LeanEnvironment:
     def __init__(self, use_mathlib: bool = True, lean_version: str = "v4.8.0"):
         """
         Initializes the Lean environment.
-        
+
         Args:
             use_mathlib (bool): If True, configures a TempRequireProject with Mathlib.
                                 This may take a while to build on the first run.
@@ -28,7 +28,7 @@ class LeanEnvironment:
         if self.use_mathlib:
             # We use TempRequireProject with mathlib as specified in lean_interact documentation
             project = TempRequireProject(
-                lean_version=self.lean_version, 
+                lean_version=self.lean_version,
                 require="mathlib"
             )
             self.config = LeanREPLConfig(project=project)
@@ -74,20 +74,20 @@ class LeanEnvironment:
 
         errors = []
         goals = []
-        
+
         # Check for error or warning messages
         if hasattr(response, 'messages') and response.messages:
             for msg in response.messages:
                 if msg.severity in ['error', 'warning']:
                     # E.g., 'declaration uses 'sorry'' is a warning, but we might want to capture it
                     errors.append(msg.data)
-        
+
         # Check for open goals (sorries)
         if hasattr(response, 'sorries') and response.sorries:
             for sorry in response.sorries:
                 if sorry.goal:
                     goals.append(sorry.goal)
-                    
+
         is_success = len(errors) == 0 and len(goals) == 0
 
         return {

src/lmm_client.py

@@ -1,6 +1,7 @@
-from groq import Groq
 from typing import List, Optional
 
+from groq import Groq
+
 
 class LMMClient:
     """

src/mathlib_corpus.py

@@ -1,12 +1,11 @@
+import glob
 import os
 import re
-import glob
 from pathlib import Path
 from typing import List, Optional
 
 from langchain_core.documents import Document
 
-
 # Regex to capture optional docstring + declaration line
 _DECL_PATTERN = re.compile(
     r'(?:/--\s*(.*?)\s*-/)?\s*'               # optional /-- docstring -/

src/rag_chain.py

@@ -1,14 +1,14 @@
 import subprocess
 from typing import Any, Dict, List, Optional
 
+from langchain_anthropic import ChatAnthropic
 from langchain_core.documents import Document
 from langchain_core.language_models.chat_models import BaseChatModel
 from langchain_core.messages import AIMessage, BaseMessage, HumanMessage, SystemMessage
-from langchain_core.outputs import ChatGeneration, ChatResult
 from langchain_core.output_parsers import StrOutputParser
+from langchain_core.outputs import ChatGeneration, ChatResult
 from langchain_core.prompts import ChatPromptTemplate
 from langchain_groq import ChatGroq
-from langchain_anthropic import ChatAnthropic
 
 
 class ClaudeCliChat(BaseChatModel):

src/retriever.py

@@ -1,15 +1,13 @@
-import os
 from pathlib import Path
 from typing import List, Optional
 
+from langchain_classic.retrievers import ContextualCompressionRetriever, EnsembleRetriever
+from langchain_classic.retrievers.document_compressors import CrossEncoderReranker
+from langchain_community.cross_encoders import HuggingFaceCrossEncoder
 from langchain_community.retrievers import BM25Retriever
 from langchain_community.vectorstores import FAISS
-from langchain_community.cross_encoders import HuggingFaceCrossEncoder
-from langchain_classic.retrievers import EnsembleRetriever, ContextualCompressionRetriever
-from langchain_classic.retrievers.document_compressors import CrossEncoderReranker
-from langchain_huggingface import HuggingFaceEmbeddings
 from langchain_core.documents import Document
-
+from langchain_huggingface import HuggingFaceEmbeddings
 from mathlib_corpus import MathLibCorpus
 
 _DEFAULT_INDEX_DIR = Path(__file__).resolve().parent.parent / "data" / "mathlib_index"

tests/test_app_fuzz.py

@@ -13,7 +13,6 @@ We mock `langgraph_agent.LangGraphAgent` BEFORE importing `app` so no Lean,
 LLM, or FAISS infrastructure is needed.
 """
 
-import io
 import os
 import sys
 import tempfile
@@ -67,13 +66,24 @@ class _DummyAgent:
 
 
 _fake_lg_module.LangGraphAgent = _DummyAgent
-sys.modules["langgraph_agent"] = _fake_lg_module
 
 # Default to having a key set; individual tests override this.
 os.environ.setdefault("GROQ_API_KEY", "test-key")
 
+# Mock langgraph_agent only for the duration of importing `app`, then restore
+# sys.modules so this file doesn't poison the import for other test files.
+# app.py captures its own `LangGraphAgent` reference at import time; tests
+# patch `app.LangGraphAgent` directly afterward.
+_orig_langgraph_agent = sys.modules.get("langgraph_agent")
+sys.modules["langgraph_agent"] = _fake_lg_module
 import app  # noqa: E402   (must come after the mock above)
 
+if _orig_langgraph_agent is not None:
+    sys.modules["langgraph_agent"] = _orig_langgraph_agent
+else:
+    del sys.modules["langgraph_agent"]
+app.LangGraphAgent = _DummyAgent  # keep app bound to the dummy after restore
+
 
 # Sentinels for the fuzz corpus -----------------------------------------------
 EMPTY = ""

tests/test_lean_verifier.py

@@ -1,12 +1,20 @@
-import unittest
-import sys
 import os
+import shutil
+import sys
+import unittest
 
 # Add src to Python path
 sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), '..', 'src')))
 
 from lean_verifier import LeanEnvironment
 
+# These tests drive a real Lean REPL + Mathlib. CI runners (and most dev
+# machines without elan) have no `lean` on PATH, so skip cleanly there
+# instead of erroring in setUpClass.
+LEAN_AVAILABLE = shutil.which("lean") is not None
+
+
+@unittest.skipUnless(LEAN_AVAILABLE, "Lean toolchain not installed (no `lean` on PATH)")
 class TestLeanVerifier(unittest.TestCase):
     @classmethod
     def setUpClass(cls):
@@ -34,7 +42,7 @@ theorem add_comm_test (n m : Nat) : n + m = m + n := by
 """
         result = self.lean_env.verify_proof(lean_code)
         self.assertEqual(result["status"], "failure")
-        self.assertTrue(any("type mismatch" in err or "application type mismatch" in err for err in result["errors"]), 
+        self.assertTrue(any("type mismatch" in err or "application type mismatch" in err for err in result["errors"]),
                         f"Expected type mismatch error, got: {result['errors']}")
 
     def test_incomplete_proof_sorry(self):
@@ -47,7 +55,7 @@ theorem my_incomplete_thm (n : Nat) : n = 5 → n = 5 := by
         result = self.lean_env.verify_proof(lean_code)
         self.assertEqual(result["status"], "failure")
         # Ensure it has an error indicating sorry
-        self.assertTrue(any("uses 'sorry'" in err for err in result["errors"]), 
+        self.assertTrue(any("uses 'sorry'" in err for err in result["errors"]),
                         f"Expected sorry warning/error, got: {result['errors']}")
         # Ensure it outputs the goal
         self.assertEqual(len(result["goals"]), 1)

tests/test_manual_bug_fixes.py

@@ -27,6 +27,7 @@ for _mod in ("lean_verifier", "retriever", "rag_chain"):
     sys.modules[_mod] = mock.MagicMock()
 
 import langgraph_agent
+
 importlib.reload(langgraph_agent)  # ensure regex/keyword changes are picked up
 _count_theorem_blocks = langgraph_agent._count_theorem_blocks
 _extract_lean_code = langgraph_agent._extract_lean_code
@@ -71,7 +72,7 @@ class TestCountTheoremBlocksKeywordFix(unittest.TestCase):
 
 
 class TestExtractLeanCodeFenceVariants(unittest.TestCase):
-    """
+    r"""
     `_extract_lean_code` used to do `text.split("```lean")[1]` which would
     leave a `4` at the start when the fence was `\`\`\`lean4` (a common LLM
     output). Now uses a regex that requires the lean tag to be terminated by
@@ -142,6 +143,7 @@ class TestProofAgentDefaultModel(unittest.TestCase):
         # Inspect the function default directly — avoids needing a working
         # LangGraphAgent mock chain.
         import inspect
+
         import proof_agent
 
         sig = inspect.signature(proof_agent.ProofAgent.__init__)

tests/test_problems_parse.py

@@ -9,7 +9,6 @@ No Lean install required - these tests only exercise text-level helpers:
     - _extract_lean_code (idempotent on raw .lean files with no fences)
 """
 
-import os
 import sys
 import unittest
 from pathlib import Path

tests/test_proof_agent.py

@@ -1,30 +1,38 @@
-import unittest
-import sys
 import os
-from unittest.mock import patch, MagicMock
+import sys
+import unittest
+from unittest.mock import MagicMock, patch
 
 # Add src to Python path
 sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), '..', 'src')))
 
-# Mock langgraph_agent.LangGraphAgent before importing proof_agent
+# Mock langgraph_agent.LangGraphAgent before importing proof_agent (so its
+# top-level `from langgraph_agent import LangGraphAgent` doesn't pull in the
+# heavy real module). Restore sys.modules afterward so this file doesn't
+# poison the langgraph_agent import for other test files in the same run.
+_orig_langgraph_agent = sys.modules.get('langgraph_agent')
 sys.modules['langgraph_agent'] = MagicMock()
 
-import proof_agent
 from proof_agent import ProofAgent
 
+if _orig_langgraph_agent is not None:
+    sys.modules['langgraph_agent'] = _orig_langgraph_agent
+else:
+    del sys.modules['langgraph_agent']
+
 
 class TestProofAgentConstructor(unittest.TestCase):
     def test_default_args_constructs_langgraph_agent_with_defaults(self):
         with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            agent = ProofAgent()
+            ProofAgent()
             MockLangGraphAgent.assert_called_once_with(
-                model_name="qwen3-vl:4b",
+                model_name="llama-3.3-70b-versatile",
                 max_retries=5,
             )
 
     def test_custom_model_name_forwarded(self):
         with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            agent = ProofAgent(model_name="custom-model:7b")
+            ProofAgent(model_name="custom-model:7b")
             MockLangGraphAgent.assert_called_once_with(
                 model_name="custom-model:7b",
                 max_retries=5,
@@ -32,15 +40,15 @@ class TestProofAgentConstructor(unittest.TestCase):
 
     def test_custom_max_retries_forwarded(self):
         with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            agent = ProofAgent(max_retries=10)
+            ProofAgent(max_retries=10)
             MockLangGraphAgent.assert_called_once_with(
-                model_name="qwen3-vl:4b",
+                model_name="llama-3.3-70b-versatile",
                 max_retries=10,
             )
 
     def test_all_custom_args_forwarded(self):
         with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            agent = ProofAgent(model_name="other-model:13b", max_retries=3)
+            ProofAgent(model_name="other-model:13b", max_retries=3)
             MockLangGraphAgent.assert_called_once_with(
                 model_name="other-model:13b",
                 max_retries=3,

tests/test_retriever_fuzz.py

@@ -104,7 +104,11 @@ _patchers = [
 for p in _patchers:
     p.start()
 
-# Now safe to import the module under test.
+# Force a fresh import: another test file in the same run may have already
+# imported the real `retriever` (e.g. via `app`), which would shadow our
+# mocked dependencies. Dropping it from sys.modules makes the import below
+# re-run with the patchers active.
+sys.modules.pop("retriever", None)
 import retriever  # noqa: E402
 
 # Re-bind the locally imported names inside `retriever` to our fakes, because
@@ -181,13 +185,14 @@ class RetrieveQueryFuzzTests(unittest.TestCase):
 
 
 class RetrieveLazyLoadTests(unittest.TestCase):
-    """`retrieve()` should lazily call `_load()` when no retriever exists."""
+    """`retrieve()` should degrade gracefully when no index is present."""
 
-    def test_retrieve_without_built_index_raises_runtime_error(self):
+    def test_retrieve_without_built_index_returns_empty(self):
+        # The retriever skips RAG (returns []) rather than raising when no
+        # FAISS index exists, so the agent can still run LLM-only.
         with tempfile.TemporaryDirectory() as tmp:
             r = retriever.MathLibRetriever(index_dir=tmp)
-            with self.assertRaises(RuntimeError):
-                r.retrieve("query")
+            self.assertEqual(r.retrieve("query"), [])
 
 
 class InitFuzzTests(unittest.TestCase):

tests/test_state_machine_fuzz.py

@@ -7,8 +7,8 @@ Covers:
 - make_verify_node(lean_env): behavior with mocked verifier.
 """
 
-import sys
 import os
+import sys
 import unittest
 from unittest.mock import MagicMock, patch
 
@@ -16,13 +16,12 @@ from unittest.mock import MagicMock, patch
 sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), '..', 'src')))
 sys.path.insert(0, 'src')
 
-from langgraph.graph import END
-
 import langgraph_agent
+from langgraph.graph import END
 from langgraph_agent import (
-    should_continue,
     make_generate_node,
     make_verify_node,
+    should_continue,
 )