diff --git a/.agents/plugins/marketplace.json b/.agents/plugins/marketplace.json new file mode 100644 index 0000000..68bbf04 --- /dev/null +++ b/.agents/plugins/marketplace.json @@ -0,0 +1,20 @@ +{ + "name": "lean-explore", + "interface": { + "displayName": "Lean Explore" + }, + "plugins": [ + { + "name": "lean-explore", + "source": { + "source": "local", + "path": "./plugins/lean-explore" + }, + "policy": { + "installation": "AVAILABLE", + "authentication": "ON_INSTALL" + }, + "category": "Developer Tools" + } + ] +} diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json new file mode 100644 index 0000000..26298b0 --- /dev/null +++ b/.claude-plugin/marketplace.json @@ -0,0 +1,16 @@ +{ + "name": "lean-explore", + "owner": { + "name": "Justin Asher", + "email": "justinchadwickasher@gmail.com" + }, + "description": "Plugins for searching Lean 4 declarations with LeanExplore.", + "plugins": [ + { + "name": "lean-explore", + "source": "./plugins/lean-explore", + "description": "Search Lean 4 declarations through the hosted LeanExplore MCP server.", + "version": "0.1.0" + } + ] +} diff --git a/README.md b/README.md index 045e0ec..b2d0534 100644 --- a/README.md +++ b/README.md @@ -56,6 +56,34 @@ lean-explore data fetch lean-explore mcp serve --backend local ``` +## Claude Code and Codex plugin + +The repository includes a plugin for both Claude Code and Codex. It connects to +the hosted MCP server, so it does not need a Python install, a local search +index, account, API key, or browser authorization. The tools are available as +soon as the plugin is installed. + +The hosted endpoint allows 30 POST requests per client IP in any 60-second +window. Protocol initialization and tool-discovery requests count toward the +limit, and clients sharing a public IP share the same budget. + +In Claude Code: + +```text +/plugin marketplace add justincasher/lean-explore +/plugin install lean-explore@lean-explore +/reload-plugins +``` + +In Codex: + +```bash +codex plugin marketplace add https://github.com/justincasher/lean-explore +codex plugin add lean-explore@lean-explore +``` + +Start a new Codex session after installation so the MCP tools are loaded. + ## Documentation Full docs live in the [`docs/`](docs/README.md) folder, or at [https://www.leanexplore.com/docs](https://www.leanexplore.com/docs). diff --git a/docs/README.md b/docs/README.md index e9386e5..7971e9f 100644 --- a/docs/README.md +++ b/docs/README.md @@ -29,7 +29,7 @@ LeanExplore has two backends and you pick one per task: | | **Remote API** | **Local backend** | |---|---|---| | Install | `pip install lean-explore` | `pip install lean-explore[local]` | -| Requires | API key | ~1 GB of data + a few GB of model weights | +| Requires | Network access | ~1 GB of data + a few GB of model weights | | Network | Required per query | Only for initial data fetch | | Use when | You want zero setup | You want offline, private, or tunable search | diff --git a/docs/api-client.md b/docs/api-client.md index ad596d9..18b3178 100644 --- a/docs/api-client.md +++ b/docs/api-client.md @@ -4,20 +4,13 @@ LeanExplore API. It ships with the base package: no PyTorch, no local indices, no data download required. -## Install and authenticate +## Install ```bash pip install lean-explore ``` -Get an API key from and set it as an -environment variable: - -```bash -export LEANEXPLORE_API_KEY="your-key-here" -``` - -Or pass it explicitly to the client constructor. +No account or API key is required. ## Quick start @@ -26,7 +19,7 @@ import asyncio from lean_explore.api import ApiClient async def main(): - client = ApiClient() # reads LEANEXPLORE_API_KEY + client = ApiClient() response = await client.search("prime number divisibility", limit=5) for result in response.results: @@ -46,7 +39,7 @@ ApiClient(api_key: str | None = None, timeout: float = 10.0) | Parameter | Default | Description | |---|---|---| -| `api_key` | `None` | API key. Falls back to `LEANEXPLORE_API_KEY` env var. Raises `ValueError` if neither is provided. | +| `api_key` | `None` | Deprecated compatibility argument. Accepted and ignored. | | `timeout` | `10.0` | HTTP timeout in seconds for every request. | The client hits `https://www.leanexplore.com/api/v2` by default. @@ -95,7 +88,7 @@ import asyncio from lean_explore.api import ApiClient async def main(): - client = ApiClient(api_key="sk-...", timeout=15.0) + client = ApiClient(timeout=15.0) response = await client.search( query="continuous function on a compact set", @@ -132,5 +125,4 @@ asyncio.run(main()) - [Data Models](./data-models.md): field reference for `SearchResult` and `SearchResponse`. -- [Configuration](./configuration.md): environment variables including - `LEANEXPLORE_API_KEY`. +- [Configuration](./configuration.md): environment variables and data paths. diff --git a/docs/cli.md b/docs/cli.md index f511f0e..79548ab 100644 --- a/docs/cli.md +++ b/docs/cli.md @@ -39,12 +39,8 @@ lean-explore search QUERY [OPTIONS] ### Requirements -`lean-explore search` uses the remote API. You must have `LEANEXPLORE_API_KEY` -set in your environment: - -```bash -export LEANEXPLORE_API_KEY="your-key-here" -``` +`lean-explore search` uses the public remote API. No account or API key is +required. ### Examples @@ -71,12 +67,11 @@ lean-explore mcp serve [OPTIONS] | Flag | Default | Description | |---|---|---| | `--backend`, `-b` | `api` | Backend to use: `api` or `local`. | -| `--api-key` | (none) | API key for the `api` backend. Overrides `LEANEXPLORE_API_KEY`. | +| `--api-key` | (none) | Deprecated compatibility option. Accepted and ignored. | ### Backends -- **`api`**: Delegates every query to the hosted LeanExplore API. Requires an - API key (via env var or `--api-key`). +- **`api`**: Delegates every query to the public hosted LeanExplore API. - **`local`**: Runs the full hybrid search pipeline on-device. Requires `pip install lean-explore[local]` and `lean-explore data fetch`. @@ -86,7 +81,7 @@ lean-explore mcp serve [OPTIONS] # Remote API (most users) lean-explore mcp serve --backend api -# Remote API with an inline key +# Legacy syntax remains valid; the value is ignored lean-explore mcp serve --backend api --api-key sk-... # Local, fully offline backend @@ -154,7 +149,7 @@ touch downloaded model weights; those live under `~/.cache/huggingface/`. All CLI commands follow standard conventions: - `0`: success -- non-zero: an error occurred (missing API key, failed download, etc.). +- non-zero: an error occurred (failed request, failed download, etc.). An error message is printed to stderr. ## See also diff --git a/docs/configuration.md b/docs/configuration.md index 2acf6f7..0da1e3e 100644 --- a/docs/configuration.md +++ b/docs/configuration.md @@ -8,9 +8,8 @@ live on disk, and how to override defaults. Configuration is centralized in ### Authentication -| Variable | Default | Used by | -|---|---|---| -| `LEANEXPLORE_API_KEY` | (required for API use) | `ApiClient`, `lean-explore search`, `lean-explore mcp serve --backend api` | +The public API, CLI search command, and stdio MCP API backend do not require +credentials. `LEANEXPLORE_API_KEY` is deprecated and ignored when present. ### Paths diff --git a/docs/getting-started.md b/docs/getting-started.md index 28f3827..7619b4b 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -26,18 +26,7 @@ pip install lean-explore This installs the CLI, the `ApiClient`, and the MCP server, roughly 50 MB of pure-Python and C-extension dependencies. No PyTorch. -### 2. Get an API key - -Sign up and generate a key at . Then export it: - -```bash -export LEANEXPLORE_API_KEY="your-key-here" -``` - -You can also add it to your shell profile (`~/.zshrc`, `~/.bashrc`) so it -persists between sessions. - -### 3. Run a search +### 2. Run a search ```bash lean-explore search "prime number divisibility" @@ -49,7 +38,7 @@ The first argument is the query. It can be a Lean declaration name, a partial name, or a natural-language description. The search engine handles both at once; you don't need to pick a mode. -### 4. (Optional) Run the MCP server +### 3. (Optional) Run the MCP server If you want to give Claude, Cursor, or another MCP client access to LeanExplore: diff --git a/docs/mcp-server.md b/docs/mcp-server.md index 799350f..c006762 100644 --- a/docs/mcp-server.md +++ b/docs/mcp-server.md @@ -12,6 +12,35 @@ This page covers: - [The tools](#the-tools) and their schemas - [Recommended agent workflow](#recommended-agent-workflow) +## Hosted plugin (Claude Code and Codex) + +The recommended setup is the repository's `lean-explore` plugin. It points at +`https://www.leanexplore.com/mcp`; no local executable, account, API key, +browser authorization, or model data is required. + +The hosted endpoint allows 30 POST requests per client IP in any 60-second +window. MCP initialization and tool-discovery requests count toward that +total, and clients behind the same NAT or proxy share the limit. When the +limit is reached, the server returns HTTP 429 with a `Retry-After` header. + +Claude Code: + +```text +/plugin marketplace add justincasher/lean-explore +/plugin install lean-explore@lean-explore +/reload-plugins +``` + +Codex: + +```bash +codex plugin marketplace add https://github.com/justincasher/lean-explore +codex plugin add lean-explore@lean-explore +``` + +The stdio server described below remains available for existing configurations +and for the fully local backend. + ## Running the server The server speaks MCP over stdio; your client launches it as a subprocess. @@ -23,7 +52,7 @@ You rarely invoke it directly except for debugging. lean-explore mcp serve --backend api ``` -Requires `LEANEXPLORE_API_KEY` in the environment, or pass `--api-key`: +No account or API key is required. The old option remains accepted as a no-op: ```bash lean-explore mcp serve --backend api --api-key sk-... @@ -55,10 +84,7 @@ on macOS): "mcpServers": { "lean-explore": { "command": "lean-explore", - "args": ["mcp", "serve", "--backend", "api"], - "env": { - "LEANEXPLORE_API_KEY": "your-key-here" - } + "args": ["mcp", "serve", "--backend", "api"] } } } @@ -84,8 +110,6 @@ Any client that accepts a command + args will work. Point it at the ### Troubleshooting -- **"API key required"**: set `LEANEXPLORE_API_KEY` in the `env` block (for - MCP clients that support it) or pass `--api-key` in `args`. - **"Essential data files for the local backend are missing"**: run `lean-explore data fetch` first. - **Tools do not appear in the client**: check the client's MCP logs. The diff --git a/openapi.yaml b/openapi.yaml index 497acf6..a9afd4c 100644 --- a/openapi.yaml +++ b/openapi.yaml @@ -7,8 +7,8 @@ info: Lean 4 declarations from indexed projects including Mathlib, PhysLean, FLT, and more. - Authentication is required via an API key provided as a Bearer token - in the Authorization header. + The API is public and does not require authentication. Legacy API-key + headers are accepted by the HTTP stack but have no effect. contact: name: Justin Asher email: justinchadwickasher@gmail.com @@ -28,14 +28,6 @@ servers: description: Production LeanExplore API Server components: - securitySchemes: - BearerAuth: - type: http - scheme: bearer - description: >- - API key provided as a Bearer token. - Example: `Authorization: Bearer YOUR_API_KEY` - schemas: SearchResult: type: object @@ -120,10 +112,7 @@ components: msg: type: string description: Human-readable error message. - example: "Invalid or missing API key" - -security: - - BearerAuth: [] + example: "Invalid request" paths: /search: @@ -162,14 +151,8 @@ paths: application/json: schema: $ref: '#/components/schemas/ApiError' - '401': - description: Unauthorized - Invalid or missing API key. - content: - application/json: - schema: - $ref: '#/components/schemas/ApiError' '429': - description: Too Many Requests - Rate limit exceeded. + description: Too Many Requests - Per-IP search limit of 30 requests per minute exceeded. content: application/json: schema: @@ -204,12 +187,6 @@ paths: application/json: schema: $ref: '#/components/schemas/SearchResult' - '401': - description: Unauthorized - Invalid or missing API key. - content: - application/json: - schema: - $ref: '#/components/schemas/ApiError' '404': description: Not Found - Declaration does not exist. content: @@ -217,7 +194,7 @@ paths: schema: $ref: '#/components/schemas/ApiError' '429': - description: Too Many Requests - Rate limit exceeded. + description: Too Many Requests - Per-IP declaration limit of 240 requests per minute exceeded. content: application/json: schema: diff --git a/plugins/lean-explore/.claude-plugin/plugin.json b/plugins/lean-explore/.claude-plugin/plugin.json new file mode 100644 index 0000000..57e9425 --- /dev/null +++ b/plugins/lean-explore/.claude-plugin/plugin.json @@ -0,0 +1,13 @@ +{ + "name": "lean-explore", + "version": "0.1.0", + "description": "Search Lean 4 declarations through the hosted LeanExplore MCP server.", + "author": { + "name": "Justin Asher", + "email": "justinchadwickasher@gmail.com" + }, + "homepage": "https://www.leanexplore.com/docs/mcp", + "repository": "https://github.com/justincasher/lean-explore", + "license": "Apache-2.0", + "keywords": ["lean", "lean4", "mathlib", "mcp", "theorem-proving"] +} diff --git a/plugins/lean-explore/.codex-plugin/plugin.json b/plugins/lean-explore/.codex-plugin/plugin.json new file mode 100644 index 0000000..44f506d --- /dev/null +++ b/plugins/lean-explore/.codex-plugin/plugin.json @@ -0,0 +1,39 @@ +{ + "name": "lean-explore", + "version": "0.1.0+codex.20260802171701", + "description": "Search Lean 4 declarations from Codex through the hosted LeanExplore MCP server.", + "author": { + "name": "Justin Asher", + "email": "justinchadwickasher@gmail.com", + "url": "https://github.com/justincasher" + }, + "homepage": "https://www.leanexplore.com/docs/mcp", + "repository": "https://github.com/justincasher/lean-explore", + "license": "Apache-2.0", + "keywords": [ + "lean", + "lean4", + "mathlib", + "mcp", + "theorem-proving" + ], + "interface": { + "displayName": "Lean Explore", + "shortDescription": "Search Lean declarations by name or meaning.", + "longDescription": "Connect Codex to LeanExplore's public hosted search for Mathlib and other Lean packages. No account, API key, browser authorization, or local search index is required.", + "developerName": "Justin Asher", + "category": "Developer Tools", + "capabilities": [ + "MCP", + "Lean declaration search" + ], + "websiteURL": "https://www.leanexplore.com/", + "privacyPolicyURL": "https://www.leanexplore.com/privacy-policy", + "termsOfServiceURL": "https://www.leanexplore.com/terms-of-service", + "defaultPrompt": [ + "Find Lean declarations relevant to this proof.", + "Search Mathlib for a theorem matching this goal." + ] + }, + "mcpServers": "./.mcp.json" +} diff --git a/plugins/lean-explore/.mcp.json b/plugins/lean-explore/.mcp.json new file mode 100644 index 0000000..21c820d --- /dev/null +++ b/plugins/lean-explore/.mcp.json @@ -0,0 +1,8 @@ +{ + "mcpServers": { + "lean-explore": { + "type": "http", + "url": "https://www.leanexplore.com/mcp" + } + } +} diff --git a/plugins/lean-explore/README.md b/plugins/lean-explore/README.md new file mode 100644 index 0000000..c916580 --- /dev/null +++ b/plugins/lean-explore/README.md @@ -0,0 +1,18 @@ +# LeanExplore plugin + +Search Lean 4 declarations from Claude Code or Codex through LeanExplore's +hosted public MCP server. There is no sign-in, browser authorization, or API +key to create, copy, or store, and the plugin does not download the local +search index. + +The MCP endpoint is `https://www.leanexplore.com/mcp`. + +The hosted endpoint allows 30 POST requests per client IP in any 60-second +window. MCP initialization and tool-discovery requests count toward the same +limit, and clients sharing a public IP share the budget. Limited requests +receive HTTP 429 with a `Retry-After` header. + +The Codex marketplace schema requires an authentication timing policy, so the +marketplace entry uses `ON_INSTALL`. This is lifecycle metadata only: the +plugin declares no credentials, and the server sends no authentication +challenge. diff --git a/pyproject.toml b/pyproject.toml index 4695ebb..7ddc36b 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -48,7 +48,8 @@ dependencies = [ "openai-agents>=0.0.16", # MCP Server Components - "mcp>=1.9.0", + # The current server uses the v1 FastMCP API. MCP 2.x is a breaking rewrite. + "mcp>=1.28.0,<2", # Utilities "tqdm>=4.60", @@ -150,4 +151,4 @@ known-first-party = ["lean_explore"] [tool.ruff.lint.pydocstyle] # Set the docstring convention to Google style. -convention = "google" \ No newline at end of file +convention = "google" diff --git a/src/lean_explore/api/client.py b/src/lean_explore/api/client.py index dd9464f..b23202a 100644 --- a/src/lean_explore/api/client.py +++ b/src/lean_explore/api/client.py @@ -1,7 +1,5 @@ """Client for interacting with the remote Lean Explore API.""" -import os - import httpx from lean_explore.config import Config @@ -11,30 +9,23 @@ class ApiClient: """Async client for the remote Lean Explore API. - This client handles making HTTP requests to the API, authenticating - with an API key, and parsing responses into SearchResult objects. + This client handles making HTTP requests to the public API and parsing + responses into SearchResult objects. The ``api_key`` argument is accepted + and ignored so existing integrations continue to start without changes. """ def __init__(self, api_key: str | None = None, timeout: float = 10.0): """Initialize the API client. Args: - api_key: The API key for authentication. If None, reads from - LEANEXPLORE_API_KEY environment variable. + api_key: Deprecated compatibility argument. It is ignored. timeout: Default timeout for HTTP requests in seconds. - - Raises: - ValueError: If no API key is provided and LEANEXPLORE_API_KEY is not set. """ + del api_key self.base_url: str = Config.API_BASE_URL - self.api_key: str = api_key or os.getenv("LEANEXPLORE_API_KEY", "") - if not self.api_key: - raise ValueError( - "API key required. Pass api_key parameter or set LEANEXPLORE_API_KEY " - "environment variable." - ) + self.api_key: str | None = None self.timeout: float = timeout - self._headers: dict[str, str] = {"Authorization": f"Bearer {self.api_key}"} + self._headers: dict[str, str] = {} async def search( self, diff --git a/src/lean_explore/cli/main.py b/src/lean_explore/cli/main.py index ca628a8..b79e01a 100644 --- a/src/lean_explore/cli/main.py +++ b/src/lean_explore/cli/main.py @@ -6,10 +6,10 @@ import asyncio import logging -import os import subprocess import sys +import httpx import typer from rich.console import Console @@ -69,17 +69,21 @@ async def _search_async( ) -> None: """Async implementation of search command.""" console = _get_console() - error_console = _get_console(use_stderr=True) - try: - client = ApiClient() - except ValueError as error: - logger.error("Failed to initialize API client: %s", error) - error_console.print(f"[bold red]Error: {error}[/bold red]") - raise typer.Exit(code=1) + client = ApiClient() console.print(f"Searching for: '{query_string}'...") - response = await client.search(query=query_string, limit=limit, packages=packages) + try: + response = await client.search( + query=query_string, + limit=limit, + packages=packages, + ) + except httpx.HTTPError as error: + logger.error("Remote search request failed: %s", error) + error_console = _get_console(use_stderr=True) + error_console.print(f"[red]Search failed:[/red] {error}") + raise typer.Exit(code=1) from error display_search_results(response, display_limit=limit, console=console) @@ -96,11 +100,11 @@ def mcp_serve_command( api_key_override: str | None = typer.Option( None, "--api-key", - help="API key to use if backend is 'api'. Overrides env var.", + help="Deprecated compatibility option. Its value is ignored.", ), ): """Launch the Lean Explore MCP (Model Context Protocol) server.""" - error_console = _get_console(use_stderr=True) + del api_key_override command_parts = [ sys.executable, @@ -110,18 +114,6 @@ def mcp_serve_command( backend.lower(), ] - if backend.lower() == "api": - effective_api_key = api_key_override or os.getenv("LEANEXPLORE_API_KEY") - if not effective_api_key: - logger.error("API key required for 'api' backend but not provided") - error_console.print( - "[bold red]API key required for 'api' backend.[/bold red]\n" - "Set LEANEXPLORE_API_KEY or use --api-key option." - ) - raise typer.Abort() - if api_key_override: - command_parts.extend(["--api-key", api_key_override]) - logger.info("Starting MCP server with backend: %s", backend.lower()) result = subprocess.run(command_parts, check=False) diff --git a/src/lean_explore/mcp/server.py b/src/lean_explore/mcp/server.py index d5ac12b..1678872 100644 --- a/src/lean_explore/mcp/server.py +++ b/src/lean_explore/mcp/server.py @@ -7,7 +7,7 @@ Command-line arguments: --backend {'api', 'local'} : Specifies the backend to use. (required) - --api-key TEXT : The API key, required if --backend is 'api'. + --api-key TEXT : Deprecated compatibility option; ignored. --log-level TEXT : Sets logging output level (e.g., INFO, WARNING, DEBUG). """ @@ -82,7 +82,7 @@ def _parse_arguments() -> argparse.Namespace: "--api-key", type=str, default=None, - help="API key for the remote API backend. Required if --backend is 'api'.", + help="Deprecated compatibility option. Its value is ignored.", ) parser.add_argument( "--log-level", @@ -172,8 +172,7 @@ def main() -> None: return except Exception as error: message = ( - "An unexpected error occurred while initializing" - f" LocalService: {error}" + f"An unexpected error occurred while initializing LocalService: {error}" ) _emit_critical_logrecord(message) logger.critical(message, exc_info=True) @@ -181,19 +180,14 @@ def main() -> None: return elif args.backend == "api": - if not args.api_key: - logger.error("--api-key is required when using the 'api' backend.") - sys.exit(1) - return try: from lean_explore.api import ApiClient - backend_service_instance = ApiClient(api_key=args.api_key) + backend_service_instance = ApiClient() logger.info("API client backend initialized successfully.") except Exception as error: message = ( - "An unexpected error occurred while initializing" - f" APIClient: {error}" + f"An unexpected error occurred while initializing APIClient: {error}" ) _emit_critical_logrecord(message) logger.critical(message, exc_info=True) diff --git a/tests/api/client_test.py b/tests/api/client_test.py index 308f8ff..881d0bc 100644 --- a/tests/api/client_test.py +++ b/tests/api/client_test.py @@ -17,29 +17,31 @@ class TestApiClientInit: """Tests for ApiClient initialization.""" def test_init_with_api_key_parameter(self): - """Test initialization with API key passed as parameter.""" + """Test that a legacy API key parameter is accepted and ignored.""" client = ApiClient(api_key="test-key-123") - assert client.api_key == "test-key-123" - assert client._headers["Authorization"] == "Bearer test-key-123" + assert client.api_key is None + assert client._headers == {} def test_init_with_env_variable(self): - """Test initialization with API key from environment variable.""" + """Test that a legacy API key environment variable is ignored.""" with patch.dict("os.environ", {"LEANEXPLORE_API_KEY": "env-key-456"}): client = ApiClient() - assert client.api_key == "env-key-456" + assert client.api_key is None + assert client._headers == {} def test_init_parameter_overrides_env(self): - """Test that parameter API key takes precedence over env variable.""" + """Test that all legacy API key inputs are ignored.""" with patch.dict("os.environ", {"LEANEXPLORE_API_KEY": "env-key"}): client = ApiClient(api_key="param-key") - assert client.api_key == "param-key" + assert client.api_key is None + assert client._headers == {} - def test_init_missing_api_key_raises(self): - """Test that missing API key raises ValueError.""" + def test_init_without_api_key(self): + """Test that no credentials are needed.""" with patch.dict("os.environ", {}, clear=True): - with patch("os.getenv", return_value=""): - with pytest.raises(ValueError, match="API key required"): - ApiClient() + client = ApiClient() + assert client.api_key is None + assert client._headers == {} def test_init_custom_timeout(self): """Test initialization with custom timeout.""" @@ -155,8 +157,8 @@ async def test_search_passes_parameters(self, client): assert call_args.kwargs["params"]["q"] == "test query" assert call_args.kwargs["params"]["limit"] == 25 - async def test_search_includes_auth_header(self, client): - """Test that search includes authorization header.""" + async def test_search_does_not_include_auth_header(self, client): + """Test that search does not send a legacy API key.""" mock_response = MagicMock() mock_response.json.return_value = {"results": []} mock_response.raise_for_status = MagicMock() @@ -171,8 +173,7 @@ async def test_search_includes_auth_header(self, client): await client.search(query="test") call_args = mock_async_client.get.call_args - assert "Authorization" in call_args.kwargs["headers"] - assert "Bearer" in call_args.kwargs["headers"]["Authorization"] + assert call_args.kwargs["headers"] == {} async def test_search_http_error(self, client): """Test that HTTP errors are propagated.""" @@ -290,8 +291,8 @@ async def test_get_by_id_http_error(self, client): with pytest.raises(httpx.HTTPStatusError): await client.get_by_id(declaration_id=42) - async def test_get_by_id_includes_auth_header(self, client): - """Test that get_by_id includes authorization header.""" + async def test_get_by_id_does_not_include_auth_header(self, client): + """Test that get_by_id does not send a legacy API key.""" mock_response = MagicMock() mock_response.status_code = 404 @@ -305,7 +306,7 @@ async def test_get_by_id_includes_auth_header(self, client): await client.get_by_id(declaration_id=1) call_args = mock_async_client.get.call_args - assert "Authorization" in call_args.kwargs["headers"] + assert call_args.kwargs["headers"] == {} async def test_get_by_id_correct_endpoint(self, client): """Test that get_by_id uses correct endpoint.""" diff --git a/tests/cli/main_test.py b/tests/cli/main_test.py index 620382a..44a982a 100644 --- a/tests/cli/main_test.py +++ b/tests/cli/main_test.py @@ -5,6 +5,7 @@ from unittest.mock import AsyncMock, MagicMock, patch +import httpx import pytest import typer from typer.testing import CliRunner @@ -95,43 +96,53 @@ async def test_search_command_with_packages(self, mock_api_client): query="test query", limit=5, packages=["Mathlib", "Std"] ) - async def test_search_command_api_key_error(self): - """Test search command when API key is missing.""" - with patch( - "lean_explore.cli.main.ApiClient", - side_effect=ValueError("API key required"), + async def test_search_command_reports_network_errors(self, mock_api_client): + """Remote request failures produce a concise stderr error and exit 1.""" + mock_api_client.search.side_effect = httpx.ConnectError("connection refused") + output_console = MagicMock() + error_console = MagicMock() + + with ( + patch("lean_explore.cli.main.ApiClient", return_value=mock_api_client), + patch( + "lean_explore.cli.main._get_console", + side_effect=[output_console, error_console], + ), + pytest.raises(typer.Exit) as exit_info, ): - with pytest.raises(typer.Exit) as exc_info: - await _search_async(query_string="test query", limit=5, packages=None) - assert exc_info.value.exit_code == 1 + await _search_async(query_string="test query", limit=5, packages=None) + + assert exit_info.value.exit_code == 1 + error_console.print.assert_called_once_with( + "[red]Search failed:[/red] connection refused" + ) class TestMcpServeCommand: """Tests for the MCP serve command.""" - def test_mcp_serve_missing_api_key(self): - """Test MCP serve fails without API key for api backend.""" - with patch.dict("os.environ", {}, clear=True): - # Remove any existing LEANEXPLORE_API_KEY - with patch("os.getenv", return_value=None): - result = runner.invoke(app, ["mcp", "serve", "--backend", "api"]) - assert result.exit_code != 0 + def test_mcp_serve_without_api_key(self): + """Test MCP API backend starts without credentials.""" + mock_result = MagicMock() + mock_result.returncode = 0 + + with patch("subprocess.run", return_value=mock_result) as mock_run: + result = runner.invoke(app, ["mcp", "serve", "--backend", "api"]) + assert result.exit_code == 0 + mock_run.assert_called_once() - def test_mcp_serve_with_api_key_env(self): - """Test MCP serve with API key from environment.""" + def test_mcp_serve_ignores_api_key_env(self): + """Test MCP serve ignores the legacy API key environment variable.""" mock_result = MagicMock() mock_result.returncode = 0 - with ( - patch("os.getenv", return_value="test-api-key"), - patch("subprocess.run", return_value=mock_result) as mock_run, - ): + with patch("subprocess.run", return_value=mock_result) as mock_run: result = runner.invoke(app, ["mcp", "serve", "--backend", "api"]) assert result.exit_code == 0 mock_run.assert_called_once() def test_mcp_serve_with_api_key_option(self): - """Test MCP serve with API key from command line option.""" + """Test MCP serve accepts and ignores the legacy API key option.""" mock_result = MagicMock() mock_result.returncode = 0 @@ -141,10 +152,9 @@ def test_mcp_serve_with_api_key_option(self): ) assert result.exit_code == 0 mock_run.assert_called_once() - # Check that --api-key was passed to subprocess call_args = mock_run.call_args[0][0] - assert "--api-key" in call_args - assert "my-key" in call_args + assert "--api-key" not in call_args + assert "my-key" not in call_args def test_mcp_serve_local_backend(self): """Test MCP serve with local backend (no API key needed).""" @@ -164,10 +174,7 @@ def test_mcp_serve_subprocess_failure(self): mock_result = MagicMock() mock_result.returncode = 1 - with ( - patch("os.getenv", return_value="test-api-key"), - patch("subprocess.run", return_value=mock_result), - ): + with patch("subprocess.run", return_value=mock_result): result = runner.invoke(app, ["mcp", "serve", "--backend", "api"]) assert result.exit_code == 1 diff --git a/tests/mcp/server_test.py b/tests/mcp/server_test.py index 4bf9076..bee4e19 100644 --- a/tests/mcp/server_test.py +++ b/tests/mcp/server_test.py @@ -77,17 +77,19 @@ def test_invalid_log_level_exits(self): class TestMainFunction: """Tests for the main function initialization logic.""" - def test_api_backend_missing_key_exits(self): - """Test that api backend without key exits with error.""" + def test_api_backend_without_key_starts(self): + """Test that the API backend starts without credentials.""" from lean_explore.mcp.server import main with ( patch.object(sys, "argv", ["server", "--backend", "api"]), - pytest.raises(SystemExit) as exc_info, + patch("lean_explore.api.ApiClient") as client_class, + patch("lean_explore.mcp.server.mcp_app.run") as run, ): main() - assert exc_info.value.code == 1 + client_class.assert_called_once_with() + run.assert_called_once_with(transport="stdio") def test_local_backend_missing_files_exits(self): """Test that local backend with missing files exits with error."""