lean_host_mcp/tools/
mod.rs

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

lean_host_mcp/tools/
mod.rs
