lean_host_mcp/tools/
mod.rs

1//! Tool implementations.
2//!
3//! Public MCP calls enter through [`semantic`], the five-tool facade. The
4//! remaining modules are internal operation building blocks, split by what
5//! plumbing they share rather than one file per public tool:
6//!
7//! - [`declaration`]: `inspect_declaration`, the bounded single-declaration
8//!   proof-work inspection tool.
9//! - [`declaration_inventory`]: source-fresh and `.ilean`-backed declaration
10//!   listings for `lean_lookup(kind = "declarations")`.
11//! - [`proof_search`]: `search_for_proof`, the proof-agent retrieval tool
12//!   built from bounded proof-state and declaration-search calls.
13//! - [`proof_action`]: `try_proof_step` and `verify_declaration`, the
14//!   non-mutating proof action tools.
15//! - [`position`]: `proof_state` and `find_references`, backed by bounded
16//!   module queries from `lean-rs-worker`.
17
18use std::sync::Arc;
19
20pub(crate) mod changed_coverage;
21pub mod declaration;
22pub mod declaration_inventory;
23pub mod position;
24pub mod proof_action;
25pub mod proof_search;
26pub mod semantic;
27pub(crate) mod source_input;
28
29use crate::broker::ProjectBroker;
30
31/// Which field of the MCP tool result carries the serialized envelope.
32///
33/// The model reads `content` text; `structuredContent` serves code-mode /
34/// validating clients. `Text` (the default) emits the envelope once, as a
35/// `content` text block — the leanest shape for the proof-agent audience and
36/// the only one Claude Code reads. `Both` duplicates onto both fields for
37/// clients that want each.
38#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
39pub enum ResponseCarrier {
40    #[default]
41    Text,
42    Structured,
43    Both,
44}
45
46impl ResponseCarrier {
47    /// Parse the config/env spelling. Case-insensitive; returns `None` for an
48    /// unknown value so the caller can report it.
49    pub fn parse(value: &str) -> Option<Self> {
50        match value.trim().to_ascii_lowercase().as_str() {
51            "text" => Some(Self::Text),
52            "structured" => Some(Self::Structured),
53            "both" => Some(Self::Both),
54            _ => None,
55        }
56    }
57}
58
59/// How much operational telemetry the model-facing envelope carries.
60///
61/// `Quiet` (the default) keeps only proof-relevant content: it drops the
62/// `runtime` block (unless a restart/pressure signal is actionable), the
63/// manifest hash and full import list from `freshness`, and per-tool search /
64/// cache instrumentation. `Full` reproduces every field for debugging and
65/// observability tooling. Correctness and truncation signals are never gated.
66#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
67pub enum TelemetryVerbosity {
68    #[default]
69    Quiet,
70    Full,
71}
72
73impl TelemetryVerbosity {
74    /// Parse the config/env spelling. Case-insensitive; returns `None` for an
75    /// unknown value so the caller can report it.
76    pub fn parse(value: &str) -> Option<Self> {
77        match value.trim().to_ascii_lowercase().as_str() {
78            "quiet" => Some(Self::Quiet),
79            "full" => Some(Self::Full),
80            _ => None,
81        }
82    }
83
84    /// Whether the demoted telemetry fields should be serialized.
85    #[must_use]
86    pub fn is_full(self) -> bool {
87        matches!(self, Self::Full)
88    }
89}
90
91/// Server-wide output budget overrides.
92///
93/// When unset, each tool keeps its own built-in byte caps (inspection allows a
94/// larger per-field cap than the proof actions). When set, the value overrides
95/// every tool's default before clamping, replacing what used to be a per-call
96/// request argument.
97#[derive(Debug, Clone, Copy, Default)]
98pub struct OutputBudgetOverrides {
99    pub max_field_bytes: Option<u32>,
100    pub max_total_bytes: Option<u32>,
101    pub heartbeat_limit: Option<u64>,
102}
103
104/// Presentation knobs resolved once at startup and shared by every tool call.
105///
106/// They decide where the envelope rides, how much telemetry it carries, and the
107/// output byte/heartbeat budgets that were once per-call request arguments.
108#[derive(Debug, Clone, Copy, Default)]
109pub struct ToolConfig {
110    pub carrier: ResponseCarrier,
111    pub verbosity: TelemetryVerbosity,
112    pub output: OutputBudgetOverrides,
113}
114
115/// Shared state every tool handler reads.
116///
117/// Holds the broker and the resolved presentation [`ToolConfig`]; each tool
118/// calls a narrow broker operation for its semantic work instead of receiving
119/// a raw project actor handle.
120#[derive(Debug, Clone)]
121pub struct ToolContext {
122    pub broker: Arc<ProjectBroker>,
123    pub config: ToolConfig,
124}
125
126/// Imports passed to worker sessions: `Init` is the internal base
127/// environment, while the public freshness envelope records only the
128/// caller-supplied vector.
129pub(crate) fn session_imports(imports: Vec<String>) -> Vec<String> {
130    if imports.iter().any(|import| import == "Init") {
131        imports
132    } else {
133        let mut out = Vec::with_capacity(imports.len().saturating_add(1));
134        out.push("Init".to_owned());
135        out.extend(imports);
136        out
137    }
138}
lean_host_mcp/tools/mod.rs

lean_host_mcp/tools/
mod.rs
