From 44c409079da081ba78b8f72610f5fdfd6110b39d Mon Sep 17 00:00:00 2001 From: justincasher Date: Sun, 2 Aug 2026 17:24:31 -0400 Subject: [PATCH 1/2] Annotate MCP tools for directory review --- README.md | 2 ++ docs/mcp-server.md | 4 ++++ plugins/lean-explore/README.md | 3 +++ src/lean_explore/mcp/tools.py | 23 ++++++++++++++++------- tests/mcp/tools_test.py | 12 ++++++++++++ 5 files changed, 37 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 4065bc8..ba91509 100644 --- a/README.md +++ b/README.md @@ -70,6 +70,8 @@ limit, and clients sharing a public IP share the same budget. Agents should begin with the token-efficient `search_summary` tool, then use the per-field retrieval tools for the declarations they need. The older full-result `search` MCP tool is deprecated and remains only for compatibility. +All LeanExplore MCP tools are read-only and cannot modify Lean packages or +external systems. In Claude Code: diff --git a/docs/mcp-server.md b/docs/mcp-server.md index 5d04899..36443a1 100644 --- a/docs/mcp-server.md +++ b/docs/mcp-server.md @@ -125,6 +125,10 @@ compatibility alias. IDs returned from `search_summary` can be passed to the per-field getters to fetch exactly the field you need, which keeps token usage low. +All tools are annotated as read-only, non-destructive, and idempotent. They +operate only on LeanExplore's indexed corpus and cannot modify Lean packages or +external systems. + ### `search_summary`: the preferred starting point Returns only `id`, `name`, and a short description per hit. Use this first, diff --git a/plugins/lean-explore/README.md b/plugins/lean-explore/README.md index df506e0..04c2427 100644 --- a/plugins/lean-explore/README.md +++ b/plugins/lean-explore/README.md @@ -11,6 +11,9 @@ Agents should use `search_summary` to find declarations, then retrieve only the fields they need. The older full-result `search` tool is deprecated and retained only for backwards compatibility. +All tools are read-only. They search or retrieve records from LeanExplore's +indexed corpus and cannot modify Lean packages or external systems. + 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 diff --git a/src/lean_explore/mcp/tools.py b/src/lean_explore/mcp/tools.py index bce3eb5..711af8f 100644 --- a/src/lean_explore/mcp/tools.py +++ b/src/lean_explore/mcp/tools.py @@ -4,6 +4,7 @@ import logging from mcp.server.fastmcp import Context as MCPContext +from mcp.types import ToolAnnotations from typing_extensions import TypedDict from lean_explore.mcp.app import AppContext, BackendServiceType, mcp_app @@ -14,6 +15,13 @@ extract_bold_description, ) +READ_ONLY_TOOL_ANNOTATIONS = ToolAnnotations( + readOnlyHint=True, + destructiveHint=False, + idempotentHint=True, + openWorldHint=False, +) + class SearchResultSummaryDict(TypedDict, total=False): """Serialized SearchResultSummary for slim MCP search responses.""" @@ -194,6 +202,7 @@ async def _execute_backend_get_by_id( "per-field tools. This compatibility tool returns every field for every " "match and may consume substantially more context." ), + annotations=READ_ONLY_TOOL_ANNOTATIONS, meta={"deprecated": True, "replacement": "search_summary"}, ) async def search( @@ -252,7 +261,7 @@ async def search( return response.model_dump(exclude_none=True) -@mcp_app.tool() +@mcp_app.tool(annotations=READ_ONLY_TOOL_ANNOTATIONS) async def search_summary( ctx: MCPContext, query: str, @@ -325,7 +334,7 @@ async def search_summary( return summary_response.model_dump(exclude_none=True) -@mcp_app.tool() +@mcp_app.tool(annotations=READ_ONLY_TOOL_ANNOTATIONS) async def get_source_code( ctx: MCPContext, declaration_id: int, @@ -361,7 +370,7 @@ async def get_source_code( ) -@mcp_app.tool() +@mcp_app.tool(annotations=READ_ONLY_TOOL_ANNOTATIONS) async def get_source_link( ctx: MCPContext, declaration_id: int, @@ -397,7 +406,7 @@ async def get_source_link( ) -@mcp_app.tool() +@mcp_app.tool(annotations=READ_ONLY_TOOL_ANNOTATIONS) async def get_docstring( ctx: MCPContext, declaration_id: int, @@ -434,7 +443,7 @@ async def get_docstring( ) -@mcp_app.tool() +@mcp_app.tool(annotations=READ_ONLY_TOOL_ANNOTATIONS) async def get_description( ctx: MCPContext, declaration_id: int, @@ -470,7 +479,7 @@ async def get_description( ) -@mcp_app.tool() +@mcp_app.tool(annotations=READ_ONLY_TOOL_ANNOTATIONS) async def get_module( ctx: MCPContext, declaration_id: int, @@ -505,7 +514,7 @@ async def get_module( ) -@mcp_app.tool() +@mcp_app.tool(annotations=READ_ONLY_TOOL_ANNOTATIONS) async def get_dependencies( ctx: MCPContext, declaration_id: int, diff --git a/tests/mcp/tools_test.py b/tests/mcp/tools_test.py index d0075e3..52d5d09 100644 --- a/tests/mcp/tools_test.py +++ b/tests/mcp/tools_test.py @@ -112,6 +112,18 @@ async def test_search_is_advertised_as_deprecated(self): assert tool.description.startswith("DEPRECATED: Use search_summary") assert tool.meta == {"deprecated": True, "replacement": "search_summary"} + async def test_all_tools_are_annotated_as_read_only(self): + """Expose accurate safety hints required by plugin directories.""" + registered_tools = await mcp_app.list_tools() + + assert len(registered_tools) == 8 + for tool in registered_tools: + assert tool.annotations is not None + assert tool.annotations.readOnlyHint is True + assert tool.annotations.destructiveHint is False + assert tool.annotations.idempotentHint is True + assert tool.annotations.openWorldHint is False + @pytest.fixture def mock_context_with_backend(self): """Create a mock MCP context with a backend service.""" From 58674785e18876d8d0c2295a4f202e1961274517 Mon Sep 17 00:00:00 2001 From: justincasher Date: Sun, 2 Aug 2026 17:26:07 -0400 Subject: [PATCH 2/2] Prepare lean-explore 1.3.0 release --- CHANGELOG.md | 17 ++++++++++++++++- pyproject.toml | 2 +- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 70bb552..88c3b2a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,21 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 N/A +## [1.3.0] - 2026-08-02 + +### Added +- Public hosted MCP plugin configuration for Claude Code and Codex. +- Read-only safety annotations on every MCP tool for plugin-directory review. + +### Changed +- The remote API, CLI, and hosted MCP server no longer require an account or API key. +- MCP agents are directed to use `search_summary` followed by per-field retrieval tools. + +### Deprecated +- API-key arguments remain accepted but are ignored for backwards compatibility. +- The full-result MCP `search` tool remains available for backwards compatibility; + new integrations should use `search_summary`. + ## [1.2.1] - 2026-02-04 ### Added @@ -81,4 +96,4 @@ nightly data updates and dynamic package indexing. ## [0.2.2] - 2025-06-06 ### Changed -- Updated minimum Python requirement to `>=3.10`. \ No newline at end of file +- Updated minimum Python requirement to `>=3.10`. diff --git a/pyproject.toml b/pyproject.toml index 7ddc36b..82f43ce 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "setuptools.build_meta" [project] name = "lean-explore" -version = "1.2.1" +version = "1.3.0" authors = [ { name = "Justin Asher", email = "justinchadwickasher@gmail.com" }, ]