Prepare public MCP directory submission and 1.3.0 release

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`.
+- Updated minimum Python requirement to `>=3.10`.

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:
 

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,

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

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" },
 ]

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,

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."""