Gate literature_search by worker web-search capability

DOCS.md

@@ -86,7 +86,7 @@ When `lean_worker_tools` is enabled, sets up tool calling for workers:
 | Handler | What it does |
 |---------|-------------|
 | `_handle_spawn` | Run worker tasks in parallel via `ThreadPoolExecutor` (up to `--parallelism`). Each worker gets its task description with wikilinks resolved. Results pushed to output window. |
-| `_handle_literature_search` | Spawn a web-enabled worker (Claude CLI with `WebSearch` + `WebFetch` tools). Results fed back to planner. |
+| `_handle_literature_search` | Spawn a web-enabled worker (currently Claude CLI with `WebSearch` + `WebFetch` tools). Results fed back to planner. |
 | `_handle_read_items` | Fetch full content of requested repo items, push to output. |
 | `_handle_write_items` | Create/update/delete repo items. Items with `format="lean"` are auto-verified via `lake env lean`. |
 | `_handle_write_whiteboard` | Update the whiteboard without spawning workers. |
@@ -156,7 +156,7 @@ Archiving: Every call saved to `archive/calls/call_NNN.json` with full prompt, s
 - `chat()` method for multi-turn tool calling conversations
 - Same interface as `LLMClient` (web_search and json_schema ignored)
 - Cost always 0.0 (local model)
-- Automatically enforces `--isolation`
+- Automatically enforces `--isolation` because local/vLLM workers cannot execute planner-level web search
 
 **Key gotchas:**
 - `--json-schema` puts structured output in `raw["structured_output"]`, not `raw["result"]`

README.md

@@ -17,7 +17,7 @@ With `--lean-project`, workers get access to **lean_verify** (compile Lean 4 cod
 Modes:
 - **Interactive** (default): see each step's plan, accept or give feedback
 - **Autonomous** (`--autonomous`): runs hands-off until proof found or budget exhausted
-- **Isolation** (default) / **No-isolation** (`--no-isolation`): by default, workers have no web access. With `--no-isolation`, the planner can use `literature_search` to find relevant papers and results online
+- **Isolation** (default) / **No-isolation** (`--no-isolation`): by default, workers have no web access. With `--no-isolation`, the planner can use `literature_search` to find relevant papers and results online when the worker model supports web search (currently Claude workers)
 - **Formal verification** (`--lean-project`): proof attempts are verified via `lake env lean`, workers can verify code and search Lean libraries
 
 ## Requirements
@@ -102,7 +102,7 @@ openprover --theorem examples/addition.md \
 | `--conclude-after` | `0.99` | Fraction of budget that triggers conclusion phase (0.9-1.0) |
 | `--autonomous` | off | Run without human confirmation |
 | `-P, --parallelism` | `1` | Max parallel workers per step |
-| `--isolation` / `--no-isolation` | on | Isolation disables web access; use `--no-isolation` to enable `literature_search` |
+| `--isolation` / `--no-isolation` | on | Isolation disables web access; `--no-isolation` requires a web-search-capable worker model (`sonnet` or `opus`) |
 | `--give-up-after` | `0.5` | Fraction of budget before give_up is allowed |
 | `--lean-project` | | Path to Lean project with lakefile |
 | `--lean-theorem` | | Path to THEOREM.lean (requires `--lean-project`) |
@@ -208,4 +208,4 @@ If you find OpenProver helpful in your research cite simply as:
   publisher = {GitHub},
   url = {https://github.com/kripner/openprover}
 }
-```
+```

openprover/cli.py

@@ -11,6 +11,14 @@
 from openprover import __version__
 from .budget import Budget, parse_duration
 from .llm import LLMClient, HFClient, MistralClient
+from .model_caps import (
+    CLAUDE_MODELS,
+    HF_MODEL_MAP,
+    MISTRAL_MODEL_MAP,
+    TOOL_CAPABLE_MODELS,
+    VLLM_MODELS,
+    supports_web_search,
+)
 from .prover import Prover, slugify
 from .tui import TUI, HeadlessTUI
 
@@ -284,18 +292,6 @@ def _cmd_prove():
     (work_dir, theorem_text, lean_theorem_text, proof_md_text,
      mode, resuming, read_only) = _resolve_inputs(parser, args)
 
-    # Map short model names to backend-specific model IDs
-    HF_MODEL_MAP = {
-        "minimax-m2.5": "MiniMaxAI/MiniMax-M2.5",
-    }
-    MISTRAL_MODEL_MAP = {
-        "leanstral": "labs-leanstral-2603",
-    }
-    VLLM_MODELS = {"minimax-m2.5"}  # served via vLLM (standard OpenAI API)
-    MISTRAL_MODELS = {"leanstral"}  # Mistral Conversations API
-    CLAUDE_MODELS = {"sonnet", "opus"}
-    TOOL_CAPABLE_MODELS = VLLM_MODELS | CLAUDE_MODELS | MISTRAL_MODELS
-
     # ── On resume, load saved config and apply as defaults ──
     if resuming:
         saved = _load_run_config(work_dir)
@@ -392,9 +388,17 @@ def _cmd_prove():
                 f"got: {', '.join(non_claude)}"
             )
 
-    # Non-Claude models have no web search capability - force isolation
-    non_claude_models = {"minimax-m2.5", "leanstral"}
-    if planner_model in non_claude_models and not args.isolation:
+    # literature_search is executed by the worker backend, so web-search
+    # capability must be checked against the worker model rather than the
+    # planner model. Older runs may have saved --no-isolation with a local
+    # worker; correct those to isolation mode. For an explicit new
+    # --no-isolation request, fail fast with a clear error.
+    if not args.isolation and not supports_web_search(worker_model):
+        if _cli_flag_given("--no-isolation"):
+            parser.error(
+                "--no-isolation requires a web-search-capable worker model "
+                "(sonnet or opus)"
+            )
         args.isolation = True
 
     if args.headless:
@@ -427,13 +431,23 @@ def _cmd_prove():
 
     def _make_client(model_alias, archive_dir):
         if model_alias in MISTRAL_MODEL_MAP:
-            return MistralClient(MISTRAL_MODEL_MAP[model_alias], archive_dir,
-                                 answer_reserve=args.answer_reserve)
-        if model_alias in HF_MODEL_MAP:
-            return HFClient(HF_MODEL_MAP[model_alias], archive_dir,
-                            base_url=args.provider_url, answer_reserve=args.answer_reserve,
-                            vllm=model_alias in VLLM_MODELS)
-        return LLMClient(model_alias, archive_dir, effort=effective_effort)
+            client = MistralClient(
+                MISTRAL_MODEL_MAP[model_alias],
+                archive_dir,
+                answer_reserve=args.answer_reserve,
+            )
+        elif model_alias in HF_MODEL_MAP:
+            client = HFClient(
+                HF_MODEL_MAP[model_alias],
+                archive_dir,
+                base_url=args.provider_url,
+                answer_reserve=args.answer_reserve,
+                vllm=model_alias in VLLM_MODELS,
+            )
+        else:
+            client = LLMClient(model_alias, archive_dir, effort=effective_effort)
+        client.model_alias = model_alias
+        return client
 
     def make_planner_llm(archive_dir):
         return _make_client(planner_model, archive_dir)

openprover/model_caps.py

@@ -0,0 +1,24 @@
+"""Backend capability helpers shared across the CLI and prover."""
+
+HF_MODEL_MAP = {
+    "minimax-m2.5": "MiniMaxAI/MiniMax-M2.5",
+}
+MISTRAL_MODEL_MAP = {
+    "leanstral": "labs-leanstral-2603",
+}
+
+VLLM_MODELS = {"minimax-m2.5"}  # served via vLLM (standard OpenAI API)
+MISTRAL_MODELS = {"leanstral"}  # Mistral Conversations API
+CLAUDE_MODELS = {"sonnet", "opus"}
+TOOL_CAPABLE_MODELS = VLLM_MODELS | CLAUDE_MODELS | MISTRAL_MODELS
+
+
+def supports_web_search(model_alias: str) -> bool:
+    """Whether a worker model can execute literature_search with web access."""
+    return model_alias in CLAUDE_MODELS
+
+
+def llm_supports_web_search(llm) -> bool:
+    """Runtime web-search capability derived from the same model-alias rules."""
+    model_alias = getattr(llm, "model_alias", getattr(llm, "model", ""))
+    return supports_web_search(model_alias)

openprover/prover.py

@@ -14,6 +14,7 @@
 from .budget import Budget
 from .lean import LeanTheorem, LeanWorkDir, run_lean_check, lean_has_errors, WORKER_TOOLS, execute_worker_tool
 from .llm import Interrupted, LLMClient
+from .model_caps import llm_supports_web_search
 from .tui import TUI
 from .tui._colors import YELLOW, GREEN, RESET as _RESET
 
@@ -1437,6 +1438,18 @@ def _handle_literature_search(self, plan: dict, step_dir: Path,
             self._save_step_meta(step_dir, status="ok", action="literature_search",
                                  resp=planner_resp, error="Isolation mode")
             return "continue"
+        if not llm_supports_web_search(self.worker_llm):
+            msg = (
+                "Literature search is not available because the worker backend "
+                "does not support web search."
+            )
+            self.tui.log(msg, color="yellow")
+            self._push_output(msg)
+            self._save_step_meta(
+                step_dir, status="ok", action="literature_search",
+                resp=planner_resp, error="Worker backend has no web search support",
+            )
+            return "continue"
 
         query = plan.get("search_query", "")
         context = plan.get("search_context", "")

tests/test_cli_validation.py

@@ -0,0 +1,59 @@
+import importlib
+import sys
+from types import SimpleNamespace
+
+import pytest
+
+
+def _import_cli_with_stubbed_tty(monkeypatch: pytest.MonkeyPatch):
+    dummy_termios = SimpleNamespace(
+        TCSADRAIN=0,
+        tcgetattr=lambda *args, **kwargs: None,
+        tcsetattr=lambda *args, **kwargs: None,
+    )
+    dummy_tty = SimpleNamespace(setcbreak=lambda *args, **kwargs: None)
+    monkeypatch.setitem(sys.modules, "termios", dummy_termios)
+    monkeypatch.setitem(sys.modules, "tty", dummy_tty)
+    for name in [
+        "openprover.cli",
+        "openprover.prover",
+        "openprover.tui",
+        "openprover.tui.tui",
+    ]:
+        sys.modules.pop(name, None)
+    return importlib.import_module("openprover.cli")
+
+
+def test_no_isolation_requires_web_search_capable_worker(
+    monkeypatch: pytest.MonkeyPatch,
+    tmp_path,
+    capsys: pytest.CaptureFixture[str],
+):
+    theorem = tmp_path / "theorem.md"
+    theorem.write_text("Prove that 1 = 1.")
+
+    cli = _import_cli_with_stubbed_tty(monkeypatch)
+    monkeypatch.setattr(
+        cli.sys,
+        "argv",
+        [
+            "openprover",
+            "--theorem",
+            str(theorem),
+            "--planner-model",
+            "opus",
+            "--worker-model",
+            "minimax-m2.5",
+            "--no-isolation",
+            "--headless",
+            "--max-time",
+            "1s",
+        ],
+    )
+
+    with pytest.raises(SystemExit) as exc:
+        cli._cmd_prove()
+
+    assert exc.value.code == 2
+    err = capsys.readouterr().err
+    assert "--no-isolation requires a web-search-capable worker model" in err

tests/test_model_caps.py

@@ -0,0 +1,20 @@
+from types import SimpleNamespace
+
+from openprover.model_caps import llm_supports_web_search, supports_web_search
+
+
+def test_web_search_capability_matches_worker_backend():
+    assert supports_web_search("sonnet") is True
+    assert supports_web_search("opus") is True
+    assert supports_web_search("minimax-m2.5") is False
+    assert supports_web_search("leanstral") is False
+
+
+def test_llm_supports_web_search_uses_model_alias_when_present():
+    claude_like = SimpleNamespace(model_alias="sonnet", model="sonnet")
+    hf_like = SimpleNamespace(model_alias="minimax-m2.5", model="MiniMaxAI/MiniMax-M2.5")
+    legacy_claude = SimpleNamespace(model="opus")
+
+    assert llm_supports_web_search(claude_like) is True
+    assert llm_supports_web_search(hf_like) is False
+    assert llm_supports_web_search(legacy_claude) is True