From 2cf70eb6bba1604bb9d0c0632442fa93d757091c Mon Sep 17 00:00:00 2001 From: KellyJDavis Date: Sat, 29 Nov 2025 12:00:11 +0100 Subject: [PATCH] docs: fix incorrect CLI commands, flags, and API examples MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This commit fixes numerous documentation errors to ensure all examples and command references accurately reflect the actual implementation: CLI Commands: - Change `http start` to `http serve` (correct command name) - Change `mcp start` to `mcp serve` (correct command name) - Fix default port from 8000 to 8001 for HTTP server - Fix default host from 127.0.0.1 to localhost for HTTP server - Fix default limit from 10 to 5 for search command CLI Flags: - Change `--pkg` to `--package` (or `-p`) for search command - Remove non-existent `--log-level` from mcp serve command - Fix chat command flags: use `--backend`, `--lean-api-key`, `--debug` instead of non-existent `--model` and `--api-key` CLI Subcommands: - Remove non-existent `configure show` and `configure reset` subcommands - Remove non-existent `data list` and `data status` subcommands - Document actual subcommands: `configure api-key`, `configure openai-key`, `data fetch`, `data clean` API Examples: - Fix field access: `results.items` → `results.results` - Fix field name: `item.informal_name` → `item.informal_description` - Fix method name: `get_citations()` → `get_dependencies()` - Update all port references from 8000 to 8001 HTTP Server Documentation: - Fix endpoint: `/api/v1/citations/{item_id}` → `/api/v1/statement_groups/{group_id}/dependencies` - Update response JSON examples to match actual API structure MCP Server Documentation: - Fix tool names: remove incorrect `lean_explore_` prefixes - Use correct tool names: `search`, `get_by_id`, `get_dependencies` - Fix parameter names to match actual tool signatures All documentation now accurately reflects the codebase implementation. --- docs/examples.md | 40 +++++++------- docs/getting-started/configuration.md | 26 +++++---- docs/getting-started/quickstart.md | 20 +++---- docs/index.md | 6 +-- docs/user-guide/api-client.md | 46 ++++++++-------- docs/user-guide/cli.md | 76 ++++++++++++--------------- docs/user-guide/http-server.md | 41 ++++++++------- docs/user-guide/local-search.md | 11 ++-- docs/user-guide/mcp-server.md | 29 +++++----- 9 files changed, 145 insertions(+), 150 deletions(-) diff --git a/docs/examples.md b/docs/examples.md index e195493..e057500 100644 --- a/docs/examples.md +++ b/docs/examples.md @@ -12,9 +12,10 @@ async def main(): client = Client(api_key="your-api-key") results = await client.search("natural numbers") - for item in results.items[:5]: + for item in results.results[:5]: print(f"{item.primary_declaration.lean_name}") - print(f" {item.informal_name}") + if item.informal_description: + print(f" {item.informal_description}") print() asyncio.run(main()) @@ -34,8 +35,8 @@ async def main(): package_filters=["Mathlib", "Batteries"] ) - print(f"Found {len(results.items)} results in Mathlib and Batteries") - for item in results.items: + print(f"Found {len(results.results)} results in Mathlib and Batteries") + for item in results.results: print(f"- {item.primary_declaration.lean_name}") asyncio.run(main()) @@ -60,8 +61,8 @@ async def main(): for result in results: print(f"\nQuery: {result.query}") - print(f"Results: {len(result.items)}") - for item in result.items[:3]: + print(f"Results: {len(result.results)}") + for item in result.results[:3]: print(f" - {item.primary_declaration.lean_name}") asyncio.run(main()) @@ -78,15 +79,16 @@ async def main(): # Search first search_results = await client.search("Nat") - if search_results.items: - first_result = search_results.items[0] + if search_results.results: + first_result = search_results.results[0] - # Get citations - citations = await client.get_citations(first_result.id) + # Get dependencies (citations) + dependencies = await client.get_dependencies(first_result.id) - print(f"Citations for {first_result.primary_declaration.lean_name}:") - for citation in citations.citations: - print(f" - {citation.lean_name}") + if dependencies: + print(f"Dependencies for {first_result.primary_declaration.lean_name}:") + for citation in dependencies.citations: + print(f" - {citation.primary_declaration.lean_name}") asyncio.run(main()) ``` @@ -104,8 +106,8 @@ async def main(): # Search results = await service.search("natural numbers") - print(f"Found {len(results.items)} results") - for item in results.items[:5]: + print(f"Found {len(results.results)} results") + for item in results.results[:5]: print(f"- {item.primary_declaration.lean_name}") asyncio.run(main()) @@ -119,12 +121,12 @@ from lean_explore.api.client import Client async def main(): # Connect to local server - client = Client(base_url="http://localhost:8000") + client = Client(base_url="http://localhost:8001") # Use as normal results = await client.search("natural numbers") - for item in results.items: + for item in results.results: print(item.primary_declaration.lean_name) asyncio.run(main()) @@ -142,7 +144,7 @@ async def main(): try: results = await client.search("natural numbers") - print(f"Found {len(results.items)} results") + print(f"Found {len(results.results)} results") except httpx.HTTPStatusError as e: print(f"HTTP error: {e.response.status_code}") print(f"Response: {e.response.text}") @@ -168,7 +170,7 @@ async def main(): ) results = await client.search("natural numbers") - print(f"Found {len(results.items)} results") + print(f"Found {len(results.results)} results") asyncio.run(main()) ``` diff --git a/docs/getting-started/configuration.md b/docs/getting-started/configuration.md index a92f07e..88d28a8 100644 --- a/docs/getting-started/configuration.md +++ b/docs/getting-started/configuration.md @@ -14,18 +14,16 @@ leanexplore configure api-key YOUR_API_KEY The API key is stored in your user configuration directory and will be used for all API requests. -### View Current Configuration +### OpenAI API Key -```bash -leanexplore configure show -``` - -### Reset Configuration +Set your OpenAI API key for chat functionality: ```bash -leanexplore configure reset +leanexplore configure openai-key YOUR_OPENAI_API_KEY ``` +The OpenAI API key is stored in your user configuration directory and will be used for chat sessions. + ## Environment Variables You can also configure Lean Explore using environment variables: @@ -41,7 +39,7 @@ export LEAN_EXPLORE_API_KEY=your-api-key For local servers or custom endpoints: ```bash -export LEAN_EXPLORE_BASE_URL=http://localhost:8000 +export LEAN_EXPLORE_BASE_URL=http://localhost:8001 ``` ## Python Configuration @@ -104,30 +102,30 @@ service = Service( ```bash # Use remote API backend -leanexplore http start --backend api --api-key YOUR_API_KEY +leanexplore http serve --backend api --api-key YOUR_API_KEY # Use local backend -leanexplore http start --backend local +leanexplore http serve --backend local ``` ### Port and Host ```bash # Custom port -leanexplore http start --backend local --port 8080 +leanexplore http serve --backend local --port 8080 # Custom host -leanexplore http start --backend local --host 0.0.0.0 +leanexplore http serve --backend local --host 0.0.0.0 ``` ## MCP Server Configuration ```bash # API backend -leanexplore mcp start --backend api --api-key YOUR_API_KEY +leanexplore mcp serve --backend api --api-key YOUR_API_KEY # Local backend -leanexplore mcp start --backend local +leanexplore mcp serve --backend local ``` ## Configuration Files diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index 7519d4b..cdc2f6f 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -25,7 +25,7 @@ leanexplore configure api-key YOUR_API_KEY Filter results to specific packages: ```bash -leanexplore search "monoid" --pkg Mathlib --pkg Batteries +leanexplore search "monoid" --package Mathlib --package Batteries ``` ## Using Python API @@ -44,8 +44,10 @@ async def main(): results = await client.search("natural numbers") # Print results - for item in results.items[:5]: # Top 5 results - print(f"{item.primary_declaration.lean_name}: {item.informal_name}") + for item in results.results[:5]: # Top 5 results + lean_name = item.primary_declaration.lean_name + informal = item.informal_description or "No description" + print(f"{lean_name}: {informal}") asyncio.run(main()) ``` @@ -65,7 +67,7 @@ async def main(): for result in results: print(f"Query: {result.query}") - print(f"Found {len(result.items)} results\n") + print(f"Found {len(result.results)} results\n") asyncio.run(main()) ``` @@ -79,21 +81,21 @@ asyncio.run(main()) leanexplore data fetch # Start the server -leanexplore http start --backend local +leanexplore http serve --backend local ``` -The server will be available at `http://localhost:8000`. +The server will be available at `http://localhost:8001`. ### Query the Local Server ```bash -curl "http://localhost:8000/api/v1/search?q=natural+numbers" +curl "http://localhost:8001/api/v1/search?q=natural+numbers" ``` Or use the Python client with a custom base URL: ```python -client = Client(base_url="http://localhost:8000") +client = Client(base_url="http://localhost:8001") results = await client.search("natural numbers") ``` @@ -102,7 +104,7 @@ results = await client.search("natural numbers") The MCP (Model Context Protocol) server allows AI agents to interact with Lean Explore: ```bash -leanexplore mcp start --backend api --api-key YOUR_API_KEY +leanexplore mcp serve --backend api --api-key YOUR_API_KEY ``` ## Next Steps diff --git a/docs/index.md b/docs/index.md index d552d14..93d4ae4 100644 --- a/docs/index.md +++ b/docs/index.md @@ -51,7 +51,7 @@ leanexplore search "natural numbers" leanexplore configure api-key YOUR_API_KEY # Start local HTTP server -leanexplore http start --backend local +leanexplore http serve --backend local ``` ### Python API @@ -67,10 +67,10 @@ results = await client.search("natural numbers") ```bash # Start server -leanexplore http start --backend local +leanexplore http serve --backend local # Query via HTTP -curl "http://localhost:8000/api/v1/search?q=natural+numbers" +curl "http://localhost:8001/api/v1/search?q=natural+numbers" ``` ## Documentation Structure diff --git a/docs/user-guide/api-client.md b/docs/user-guide/api-client.md index a5ad60b..873a2ac 100644 --- a/docs/user-guide/api-client.md +++ b/docs/user-guide/api-client.md @@ -13,7 +13,7 @@ from lean_explore.api.client import Client client = Client(api_key="your-api-key") # With custom base URL (for local servers) -client = Client(base_url="http://localhost:8000") +client = Client(base_url="http://localhost:8001") # Both API key and custom URL client = Client( @@ -31,8 +31,8 @@ async def main(): client = Client(api_key="your-api-key") results = await client.search("natural numbers") - print(f"Found {len(results.items)} results") - for item in results.items: + print(f"Found {len(results.results)} results") + for item in results.results: print(f"- {item.primary_declaration.lean_name}") asyncio.run(main()) @@ -49,7 +49,7 @@ async def main(): for result in results: print(f"Query: {result.query}") - print(f"Results: {len(result.items)}\n") + print(f"Results: {len(result.results)}\n") asyncio.run(main()) ``` @@ -68,7 +68,7 @@ async def main(): package_filters=["Mathlib", "Batteries"] ) - for item in results.items: + for item in results.results: print(f"{item.primary_declaration.lean_name}") asyncio.run(main()) @@ -82,14 +82,16 @@ async def main(): # Search first search_results = await client.search("natural numbers") - first_result = search_results.items[0] - - # Get citations for a result - citations = await client.get_citations(first_result.id) - - print(f"Citations for {first_result.primary_declaration.lean_name}:") - for citation in citations.citations: - print(f"- {citation.lean_name}") + if search_results.results: + first_result = search_results.results[0] + + # Get dependencies (citations) for a result + dependencies = await client.get_dependencies(first_result.id) + + if dependencies: + print(f"Dependencies for {first_result.primary_declaration.lean_name}:") + for citation in dependencies.citations: + print(f"- {citation.primary_declaration.lean_name}") asyncio.run(main()) ``` @@ -123,38 +125,34 @@ results: APISearchResponse = await client.search("query") # Access properties results.query # The search query -results.items # List of APISearchResultItem +results.results # List of APISearchResultItem ``` ### APISearchResultItem ```python -item = results.items[0] +item = results.results[0] # Primary declaration item.primary_declaration.lean_name -item.primary_declaration.decl_type # Informal description -item.informal_name item.informal_description # Statement group ID item.id -# Score -item.score ``` ### APICitationsResponse ```python -citations = await client.get_citations(item_id) +dependencies = await client.get_dependencies(item_id) -# List of citations -for citation in citations.citations: - print(citation.lean_name) - print(citation.decl_type) +# List of dependencies (citations) +if dependencies: + for citation in dependencies.citations: + print(citation.primary_declaration.lean_name) ``` ## Configuration diff --git a/docs/user-guide/cli.md b/docs/user-guide/cli.md index f4e4e22..5a56ac5 100644 --- a/docs/user-guide/cli.md +++ b/docs/user-guide/cli.md @@ -21,8 +21,8 @@ leanexplore search QUERY [OPTIONS] ``` **Options:** -- `--pkg, -p`: Filter by package name (can be specified multiple times) -- `--limit, -n`: Maximum number of results (default: 10) +- `--package, -p`: Filter by package name (can be specified multiple times) +- `--limit, -n`: Maximum number of results (default: 5) **Examples:** @@ -31,10 +31,10 @@ leanexplore search QUERY [OPTIONS] leanexplore search "natural numbers" # Search with package filter -leanexplore search "monoid" --pkg Mathlib +leanexplore search "monoid" --package Mathlib # Multiple package filters -leanexplore search "group" --pkg Mathlib --pkg Batteries +leanexplore search "group" --package Mathlib --package Batteries # Limit results leanexplore search "topology" --limit 5 @@ -50,21 +50,17 @@ leanexplore configure COMMAND **Subcommands:** -- `api-key KEY`: Set API key for remote API -- `show`: Display current configuration -- `reset`: Reset configuration to defaults +- `api-key`: Set API key for remote API (prompts if not provided) +- `openai-key`: Set OpenAI API key for chat functionality (prompts if not provided) **Examples:** ```bash -# Set API key +# Set API key (will prompt if not provided) leanexplore configure api-key YOUR_API_KEY -# View configuration -leanexplore configure show - -# Reset configuration -leanexplore configure reset +# Set OpenAI API key (will prompt if not provided) +leanexplore configure openai-key YOUR_OPENAI_API_KEY ``` ### HTTP Server @@ -72,26 +68,26 @@ leanexplore configure reset Start a local HTTP server: ```bash -leanexplore http start [OPTIONS] +leanexplore http serve [OPTIONS] ``` **Options:** -- `--backend`: Backend type (`api` or `local`) +- `--backend, -b`: Backend type (`api` or `local`, default: `local`) - `--api-key`: API key (required for `api` backend) -- `--host`: Host to bind to (default: `127.0.0.1`) -- `--port`: Port to bind to (default: `8000`) +- `--host`: Host to bind to (default: `localhost`) +- `--port`: Port to bind to (default: `8001`) **Examples:** ```bash # Start with API backend -leanexplore http start --backend api --api-key YOUR_API_KEY +leanexplore http serve --backend api --api-key YOUR_API_KEY # Start with local backend -leanexplore http start --backend local +leanexplore http serve --backend local # Custom host and port -leanexplore http start --backend local --host 0.0.0.0 --port 8080 +leanexplore http serve --backend local --host 0.0.0.0 --port 8080 ``` ### MCP Server @@ -99,22 +95,21 @@ leanexplore http start --backend local --host 0.0.0.0 --port 8080 Start the Model Context Protocol server: ```bash -leanexplore mcp start [OPTIONS] +leanexplore mcp serve [OPTIONS] ``` **Options:** -- `--backend`: Backend type (`api` or `local`) +- `--backend, -b`: Backend type (`api` or `local`, default: `api`) - `--api-key`: API key (required for `api` backend) -- `--log-level`: Logging level (default: `INFO`) **Examples:** ```bash # Start with API backend -leanexplore mcp start --backend api --api-key YOUR_API_KEY +leanexplore mcp serve --backend api --api-key YOUR_API_KEY # Start with local backend -leanexplore mcp start --backend local +leanexplore mcp serve --backend local ``` ### Data Management @@ -128,8 +123,7 @@ leanexplore data COMMAND **Subcommands:** - `fetch`: Download local data files -- `list`: List available data toolchains -- `status`: Check data status +- `clean`: Remove all downloaded local data toolchains **Examples:** @@ -137,11 +131,8 @@ leanexplore data COMMAND # Fetch local data leanexplore data fetch -# List available toolchains -leanexplore data list - -# Check data status -leanexplore data status +# Clean all downloaded data +leanexplore data clean ``` ### Chat @@ -153,21 +144,24 @@ leanexplore chat [OPTIONS] ``` **Options:** -- `--model`: Model to use (default: `gpt-4`) -- `--backend`: Backend type (`api` or `local`) -- `--api-key`: API key (required for `api` backend) +- `--backend, -lb`: Backend type (`api` or `local`, default: `api`) +- `--lean-api-key`: API key for Lean Explore (if `api` backend, overrides env var/config) +- `--debug`: Enable detailed debug logging **Examples:** ```bash -# Start chat session +# Start chat session (uses API backend by default) leanexplore chat -# Use specific model -leanexplore chat --model gpt-4-turbo - # Use local backend leanexplore chat --backend local + +# Use API backend with explicit API key +leanexplore chat --backend api --lean-api-key YOUR_API_KEY + +# Enable debug logging +leanexplore chat --debug ``` ## Global Options @@ -188,10 +182,10 @@ leanexplore search "natural numbers" # 3. Start local server leanexplore data fetch -leanexplore http start --backend local +leanexplore http serve --backend local # 4. Query the server -curl "http://localhost:8000/api/v1/search?q=natural+numbers" +curl "http://localhost:8001/api/v1/search?q=natural+numbers" ``` ## Next Steps diff --git a/docs/user-guide/http-server.md b/docs/user-guide/http-server.md index 58782ee..b9dea09 100644 --- a/docs/user-guide/http-server.md +++ b/docs/user-guide/http-server.md @@ -7,7 +7,7 @@ Run a local HTTP server that provides the same API as the remote Lean Explore se ### Using API Backend ```bash -leanexplore http start --backend api --api-key YOUR_API_KEY +leanexplore http serve --backend api --api-key YOUR_API_KEY ``` This starts a server that proxies requests to the remote API. @@ -19,14 +19,14 @@ This starts a server that proxies requests to the remote API. leanexplore data fetch # Start server with local backend -leanexplore http start --backend local +leanexplore http serve --backend local ``` ### Custom Configuration ```bash # Custom host and port -leanexplore http start --backend local --host 0.0.0.0 --port 8080 +leanexplore http serve --backend local --host 0.0.0.0 --port 8080 ``` ## API Endpoints @@ -46,7 +46,7 @@ GET /api/v1/search?q=QUERY&pkg=PACKAGE **Example:** ```bash -curl "http://localhost:8000/api/v1/search?q=natural+numbers" +curl "http://localhost:8001/api/v1/search?q=natural+numbers" ``` **Response:** @@ -54,43 +54,44 @@ curl "http://localhost:8000/api/v1/search?q=natural+numbers" ```json { "query": "natural numbers", - "items": [ + "results": [ { "id": 123, "primary_declaration": { - "lean_name": "Nat", - "decl_type": "structure" + "lean_name": "Nat" }, - "informal_name": "Natural numbers", - "informal_description": "...", - "score": 0.95 + "informal_description": "..." } ] } ``` -### Get Citations +### Get Dependencies ```bash -GET /api/v1/citations/{item_id} +GET /api/v1/statement_groups/{group_id}/dependencies ``` **Example:** ```bash -curl "http://localhost:8000/api/v1/citations/123" +curl "http://localhost:8001/api/v1/statement_groups/123/dependencies" ``` **Response:** ```json { + "source_group_id": 123, "citations": [ { - "lean_name": "Nat.add", - "decl_type": "def" + "id": 456, + "primary_declaration": { + "lean_name": "Nat.add" + } } - ] + ], + "count": 1 } ``` @@ -102,7 +103,7 @@ You can use the Python client with a local server: from lean_explore.api.client import Client # Connect to local server -client = Client(base_url="http://localhost:8000") +client = Client(base_url="http://localhost:8001") # Use as normal results = await client.search("natural numbers") @@ -112,9 +113,9 @@ results = await client.search("natural numbers") The server provides OpenAPI documentation at: -- Swagger UI: `http://localhost:8000/docs` -- ReDoc: `http://localhost:8000/redoc` -- OpenAPI JSON: `http://localhost:8000/openapi.json` +- Swagger UI: `http://localhost:8001/docs` +- ReDoc: `http://localhost:8001/redoc` +- OpenAPI JSON: `http://localhost:8001/openapi.json` ## Backend Comparison diff --git a/docs/user-guide/local-search.md b/docs/user-guide/local-search.md index 2baa082..b33c9a6 100644 --- a/docs/user-guide/local-search.md +++ b/docs/user-guide/local-search.md @@ -23,7 +23,7 @@ This downloads: Check that data is available: ```bash -leanexplore data status +# Data status can be checked by attempting to use the local backend ``` ## Using Local Backend @@ -31,8 +31,7 @@ leanexplore data status ### CLI ```bash -# Search using local backend -leanexplore search "natural numbers" --backend local +# Search using local backend (CLI always uses API backend, use HTTP server for local) ``` ### Python API @@ -47,7 +46,7 @@ service = Service() results = await service.search("natural numbers") # Process results -for item in results.items: +for item in results.results: print(item.primary_declaration.lean_name) ``` @@ -55,13 +54,13 @@ for item in results.items: ```bash # Start server with local backend -leanexplore http start --backend local +leanexplore http serve --backend local ``` Then query via HTTP: ```bash -curl "http://localhost:8000/api/v1/search?q=natural+numbers" +curl "http://localhost:8001/api/v1/search?q=natural+numbers" ``` ## Configuration diff --git a/docs/user-guide/mcp-server.md b/docs/user-guide/mcp-server.md index 3b6bae9..9372fee 100644 --- a/docs/user-guide/mcp-server.md +++ b/docs/user-guide/mcp-server.md @@ -11,7 +11,7 @@ MCP is a protocol that enables AI assistants to access external tools and data s ### Using API Backend ```bash -leanexplore mcp start --backend api --api-key YOUR_API_KEY +leanexplore mcp serve --backend api --api-key YOUR_API_KEY ``` ### Using Local Backend @@ -21,13 +21,13 @@ leanexplore mcp start --backend api --api-key YOUR_API_KEY leanexplore data fetch # Start MCP server -leanexplore mcp start --backend local +leanexplore mcp serve --backend local ``` ### Custom Logging ```bash -leanexplore mcp start --backend local --log-level DEBUG +leanexplore mcp serve --backend local ``` ## Available Tools @@ -46,10 +46,11 @@ Search for Lean declarations using natural language queries. ```json { - "name": "lean_explore_search", + "name": "search", "arguments": { "query": "natural numbers", - "package_filters": ["Mathlib"] + "package_filters": ["Mathlib"], + "limit": 10 } } ``` @@ -59,33 +60,33 @@ Search for Lean declarations using natural language queries. Retrieve detailed information about a specific statement group. **Parameters:** -- `statement_group_id` (integer, required): The ID of the statement group +- `group_id` (integer or list of integers, required): The ID(s) of the statement group(s) **Example:** ```json { - "name": "lean_explore_get_statement_group", + "name": "get_by_id", "arguments": { - "statement_group_id": 123 + "group_id": 123 } } ``` -### Get Citations +### Get Dependencies -Get declarations that cite a specific statement group. +Get dependencies (citations) for a specific statement group. **Parameters:** -- `statement_group_id` (integer, required): The ID of the statement group +- `group_id` (integer or list of integers, required): The ID(s) of the statement group(s) **Example:** ```json { - "name": "lean_explore_get_citations", + "name": "get_dependencies", "arguments": { - "statement_group_id": 123 + "group_id": 123 } } ``` @@ -101,7 +102,7 @@ Add to your Claude Desktop configuration: "mcpServers": { "lean-explore": { "command": "leanexplore", - "args": ["mcp", "start", "--backend", "api", "--api-key", "YOUR_API_KEY"] + "args": ["mcp", "serve", "--backend", "api", "--api-key", "YOUR_API_KEY"] } } }