lean_host_mcp/tools/
semantic.rs

1//! Public semantic MCP facade.
2//!
3//! The implementation modules keep the old, narrow operation names because
4//! they are useful internal building blocks. This module is the public boundary:
5//! five semantic tools, each with a small `kind` namespace, and one response
6//! shape (`data`, `errors`, `trust`).
7
8use std::borrow::Cow;
9use std::collections::BTreeMap;
10use std::path::Path;
11
12use schemars::{JsonSchema, Schema, SchemaGenerator};
13use serde::{Deserialize, Deserializer, Serialize, de::DeserializeOwned};
14use serde_json::{Map, Value, json};
15
16use crate::broker::{BrokerConfigSnapshot, ProjectHint};
17use crate::envelope::{FreshnessIdentity, Response, RuntimeFailure};
18use crate::error::{Result, ServerError, WorkerUnavailable};
19use crate::tools::{ResponseCarrier, TelemetryVerbosity, ToolContext};
20use crate::trust::{ArtifactKind, ArtifactTrust, TrustStatus, dedupe_artifacts};
21
22use super::changed_coverage::{self, ChangedCoverageRequest};
23use super::declaration::{self, InspectDeclarationRequest};
24use super::declaration_inventory::{self, DeclarationInventoryRequest};
25use super::position::{self, CommandTrialRequest, FileDiagnosticsRequest, FindReferencesRequest, ProofStateRequest};
26use super::proof_action::{self, LeanVerifyRequest, TryProofStepRequest};
27use super::proof_search::{self, SearchForProofRequest};
28
29#[derive(Debug, Clone, Deserialize, JsonSchema)]
30pub struct SemanticToolRequest {
31    /// Mode within this semantic tool family.
32    #[serde(default)]
33    pub kind: Option<String>,
34    /// Mode-specific fields. Unknown fields are passed to the selected mode's
35    /// typed request decoder.
36    #[serde(flatten)]
37    pub args: BTreeMap<String, Value>,
38}
39
40macro_rules! semantic_tool_request_wrapper {
41    ($name:ident, $schema_name:literal, $schema_fn:ident) => {
42        #[derive(Debug, Clone)]
43        pub struct $name(pub SemanticToolRequest);
44
45        impl $name {
46            pub fn into_inner(self) -> SemanticToolRequest {
47                self.0
48            }
49        }
50
51        impl<'de> Deserialize<'de> for $name {
52            fn deserialize<D>(deserializer: D) -> std::result::Result<Self, D::Error>
53            where
54                D: Deserializer<'de>,
55            {
56                SemanticToolRequest::deserialize(deserializer).map(Self)
57            }
58        }
59
60        impl JsonSchema for $name {
61            fn schema_name() -> Cow<'static, str> {
62                Cow::Borrowed($schema_name)
63            }
64
65            fn json_schema(_generator: &mut SchemaGenerator) -> Schema {
66                $schema_fn()
67            }
68        }
69    };
70}
71
72semantic_tool_request_wrapper!(LeanContextToolRequest, "LeanContextToolRequest", lean_context_schema);
73semantic_tool_request_wrapper!(LeanTrialToolRequest, "LeanTrialToolRequest", lean_trial_schema);
74semantic_tool_request_wrapper!(LeanLookupToolRequest, "LeanLookupToolRequest", lean_lookup_schema);
75semantic_tool_request_wrapper!(LeanStatusToolRequest, "LeanStatusToolRequest", lean_status_schema);
76
77impl SemanticToolRequest {
78    fn kind(&self) -> Option<&str> {
79        self.kind.as_deref().map(str::trim).filter(|kind| !kind.is_empty())
80    }
81}
82
83fn schema_from_value(value: Value) -> Schema {
84    match value {
85        Value::Object(map) => map.into(),
86        Value::Bool(value) => value.into(),
87        Value::Null | Value::Number(_) | Value::String(_) | Value::Array(_) => true.into(),
88    }
89}
90
91fn semantic_schema(title: &str, description: &str, variants: &[Value]) -> Schema {
92    let properties = top_level_semantic_properties(variants);
93    schema_from_value(json!({
94        "title": title,
95        "description": description,
96        "type": "object",
97        "properties": properties,
98        "additionalProperties": true,
99    }))
100}
101
102fn top_level_semantic_properties(variants: &[Value]) -> Value {
103    let mut properties = Map::new();
104    let mut kinds = Vec::new();
105    for variant in variants {
106        let Some(variant_properties) = variant.get("properties").and_then(Value::as_object) else {
107            continue;
108        };
109        for (name, schema) in variant_properties {
110            if name == "kind" {
111                collect_kind_values(schema, &mut kinds);
112                continue;
113            }
114            properties.entry(name.clone()).or_insert_with(|| schema.clone());
115        }
116    }
117    if !kinds.is_empty() {
118        let defaults_to_project = kinds.iter().any(|kind| kind.as_str() == Some("project"));
119        let mut kind_schema = json!({
120            "description": "Mode within this semantic tool family.",
121            "enum": kinds,
122        });
123        if defaults_to_project && let Value::Object(schema) = &mut kind_schema {
124            schema.insert("default".to_owned(), Value::String("project".to_owned()));
125        }
126        properties.insert("kind".to_owned(), kind_schema);
127    }
128    Value::Object(properties)
129}
130
131fn collect_kind_values(schema: &Value, kinds: &mut Vec<Value>) {
132    if let Some(kind) = schema.get("const") {
133        push_unique_kind(kinds, kind.clone());
134    }
135    if let Some(enum_values) = schema.get("enum").and_then(Value::as_array) {
136        for kind in enum_values {
137            push_unique_kind(kinds, kind.clone());
138        }
139    }
140}
141
142fn push_unique_kind(kinds: &mut Vec<Value>, kind: Value) {
143    if !kinds.contains(&kind) {
144        kinds.push(kind);
145    }
146}
147
148fn proof_position_selector_schema() -> Value {
149    json!({
150        "description": "Where in the declaration proof to inspect or edit. Omit for the pristine entry goal.",
151        "type": "object",
152        "properties": {
153            "kind": {
154                "enum": ["default", "index", "after_text"],
155                "description": "`default` uses the entry goal; `index` requires `index`; `after_text` requires `text` and accepts optional `occurrence`. For matched text, inspect returned `goals_before`/`goals_after`; not every substring is a proof-state boundary."
156            },
157            "index": { "type": "integer", "minimum": 0 },
158            "text": { "type": "string" },
159            "occurrence": { "type": "integer", "minimum": 0, "default": 0 }
160        },
161        "required": ["kind"],
162        "additionalProperties": false,
163        "examples": [
164            { "kind": "default" },
165            { "kind": "index", "index": 0 },
166            { "kind": "after_text", "text": "intro h", "occurrence": 0 }
167        ]
168    })
169}
170
171fn target_schema() -> Value {
172    json!({
173        "description": "Declaration inventory target. Use `kind: \"file\"` with `path`, or `kind: \"module\"` with `module`.",
174        "type": "object",
175        "properties": {
176            "kind": {
177                "enum": ["file", "module"],
178                "description": "`file` reads declarations from a Lean source file; `module` reads a Lean module using source when available and a fresh .ilean supplement/fallback when needed."
179            },
180            "path": { "type": "string", "description": "Path to a .lean file, relative to the project root unless absolute. Required when kind is `file`." },
181            "module": { "type": "string", "description": "Dotted Lean module name. Required when kind is `module`." }
182        },
183        "required": ["kind"],
184        "additionalProperties": false,
185        "examples": [
186            { "kind": "file", "path": "LeanRsFixture/ProofAgent.lean" },
187            { "kind": "module", "module": "LeanRsFixture.ProofAgent" }
188        ]
189    })
190}
191
192fn lean_context_schema() -> Schema {
193    semantic_schema(
194        "LeanContextToolRequest",
195        "Lean proof or term context. Select a mode with kind.",
196        &[json!({
197            "type": "object",
198            "description": "Read proof context at a declaration proof position.",
199            "required": ["kind", "file", "declaration"],
200            "properties": {
201                "kind": { "const": "proof_position" },
202                "file": { "type": "string", "description": "Path to a .lean file, relative to the project root unless absolute." },
203                "declaration": { "type": "string", "description": "Fully-qualified or file-local declaration name." },
204                "proof_position": proof_position_selector_schema(),
205                "project": { "type": ["string", "null"], "description": "Optional project-root override." }
206            },
207            "additionalProperties": false,
208            "examples": [semantic_example("lean_context", "proof_position").unwrap_or(Value::Null)]
209        })],
210    )
211}
212
213fn lean_trial_schema() -> Schema {
214    semantic_schema(
215        "LeanTrialToolRequest",
216        "Non-mutating Lean experiments. Select proof_step or command with kind.",
217        &[
218            json!({
219                "type": "object",
220                "description": "Try one or more proof snippets against an in-memory source snapshot.",
221                "required": ["kind", "file", "declaration"],
222                "properties": {
223                    "kind": { "const": "proof_step" },
224                    "file": { "type": "string" },
225                    "declaration": { "type": "string" },
226                    "proof_position": proof_position_selector_schema(),
227                    "snippet": { "type": ["string", "null"] },
228                    "snippets": { "type": "array", "items": { "type": "string" } },
229                    "project": { "type": ["string", "null"] }
230                },
231                "additionalProperties": false,
232                "examples": [semantic_example("lean_trial", "proof_step").unwrap_or(Value::Null)]
233            }),
234            json!({
235                "type": "object",
236                "description": "Run bounded Lean command text, such as #check or #print axioms.",
237                "required": ["kind", "commands"],
238                "properties": {
239                    "kind": { "const": "command" },
240                    "commands": { "type": "string" },
241                    "file": { "type": ["string", "null"], "description": "Optional source file whose contents precede the command." },
242                    "imports": { "type": "array", "items": { "type": "string" } },
243                    "project": { "type": ["string", "null"] }
244                },
245                "additionalProperties": false,
246                "examples": [semantic_example("lean_trial", "command").unwrap_or(Value::Null)]
247            }),
248        ],
249    )
250}
251
252fn lean_lookup_schema() -> Schema {
253    semantic_schema(
254        "LeanLookupToolRequest",
255        "Semantic lookup and discovery. Select a mode with kind.",
256        &[
257            json!({
258                "type": "object",
259                "description": "Inspect one declaration by name.",
260                "required": ["kind", "name"],
261                "properties": {
262                    "kind": { "const": "declaration" },
263                    "name": { "type": "string" },
264                    "file": { "type": ["string", "null"] },
265                    "imports": { "type": "array", "items": { "type": "string" } },
266                    "fields": {
267                        "description": "Optional field selection. Use an object of booleans or a string list naming fields to include.",
268                        "type": ["object", "array", "null"],
269                        "properties": {
270                            "source": { "type": "boolean", "default": true },
271                            "statement": { "type": "boolean", "default": true },
272                            "docstring": { "type": "boolean", "default": true },
273                            "attributes": { "type": "boolean", "default": true },
274                            "flags": { "type": "boolean", "default": true }
275                        },
276                        "items": {
277                            "enum": ["source", "statement", "type", "docstring", "docs", "attributes", "flags"]
278                        },
279                        "examples": [
280                            ["statement", "docstring"],
281                            { "statement": true, "docstring": true, "source": false, "attributes": false, "flags": false }
282                        ]
283                    },
284                    "raw_statement": { "type": "boolean" },
285                    "project": { "type": ["string", "null"] }
286                },
287                "additionalProperties": false,
288                "examples": [semantic_example("lean_lookup", "declaration").unwrap_or(Value::Null)]
289            }),
290            json!({
291                "type": "object",
292                "description": "List declarations in one source file or module.",
293                "required": ["kind", "target"],
294                "properties": {
295                    "kind": { "const": "declarations" },
296                    "target": target_schema(),
297                    "limit": { "type": ["integer", "null"], "minimum": 1, "maximum": 1000, "default": 200 },
298                    "project": { "type": ["string", "null"] }
299                },
300                "additionalProperties": false,
301                "examples": [semantic_example("lean_lookup", "declarations").unwrap_or(Value::Null)]
302            }),
303            json!({
304                "type": "object",
305                "description": "Map git hunks to declarations without verifying them.",
306                "required": ["kind"],
307                "properties": {
308                    "kind": { "const": "changed_coverage" },
309                    "base": { "type": ["string", "null"], "default": "HEAD" },
310                    "files": { "type": "array", "items": { "type": "string" } },
311                    "include_untracked": { "type": "boolean", "default": false },
312                    "project": { "type": ["string", "null"] }
313                },
314                "additionalProperties": false,
315                "examples": [semantic_example("lean_lookup", "changed_coverage").unwrap_or(Value::Null)]
316            }),
317            json!({
318                "type": "object",
319                "description": "Retrieve proof-search candidates from a file/declaration position or explicit goal text.",
320                "required": ["kind"],
321                "properties": {
322                    "kind": { "const": "proof_search" },
323                    "file": { "type": ["string", "null"] },
324                    "declaration": { "type": ["string", "null"] },
325                    "proof_position": proof_position_selector_schema(),
326                    "goal": { "type": ["string", "null"] },
327                    "type_text": { "type": ["string", "null"] },
328                    "imports": { "type": "array", "items": { "type": "string" } },
329                    "mode": { "enum": ["next_step", "exact", "apply", "rewrite", "simp"] },
330                    "limit": { "type": ["integer", "null"], "minimum": 1, "maximum": 20 },
331                    "project": { "type": ["string", "null"] }
332                },
333                "additionalProperties": false,
334                "examples": [semantic_example("lean_lookup", "proof_search").unwrap_or(Value::Null)]
335            }),
336            json!({
337                "type": "object",
338                "description": "Find semantic references to a fully-qualified Lean name.",
339                "required": ["kind", "name", "scope"],
340                "properties": {
341                    "kind": { "const": "references" },
342                    "name": { "type": "string" },
343                    "scope": { "enum": ["file", "project"] },
344                    "file": { "type": ["string", "null"], "description": "Required for file scope." },
345                    "files": { "type": "array", "items": { "type": "string" }, "description": "Optional file restriction for project scope." },
346                    "limit": { "type": ["integer", "null"], "minimum": 1 },
347                    "project": { "type": ["string", "null"] }
348                },
349                "additionalProperties": false,
350                "examples": [semantic_example("lean_lookup", "references").unwrap_or(Value::Null)]
351            }),
352        ],
353    )
354}
355
356fn lean_status_schema() -> Schema {
357    semantic_schema(
358        "LeanStatusToolRequest",
359        "Project/toolchain status and source diagnostics. Select a mode with kind; omitted kind defaults to project.",
360        &[
361            json!({
362                "type": "object",
363                "description": "Read cheap project, toolchain, worker, and artifact status without opening a worker.",
364                "properties": {
365                    "kind": { "const": "project", "default": "project" },
366                    "project": { "type": ["string", "null"], "description": "Optional project-root override." },
367                    "include": {
368                        "type": "array",
369                        "items": { "enum": ["toolchain", "worker", "artifacts"] },
370                        "description": "Sections to include. Omit for all sections."
371                    }
372                },
373                "additionalProperties": false,
374                "examples": [semantic_example("lean_status", "project").unwrap_or(Value::Null)]
375            }),
376            json!({
377                "type": "object",
378                "description": "Elaborate one source file and return bounded diagnostics.",
379                "required": ["kind", "file"],
380                "properties": {
381                    "kind": { "const": "file_diagnostics" },
382                    "file": { "type": "string" },
383                    "project": { "type": ["string", "null"] }
384                },
385                "additionalProperties": false,
386                "examples": [semantic_example("lean_status", "file_diagnostics").unwrap_or(Value::Null)]
387            }),
388        ],
389    )
390}
391
392fn semantic_example(tool: &str, kind: &str) -> Option<Value> {
393    match (tool, kind) {
394        ("lean_context", "proof_position") => Some(json!({
395            "kind": "proof_position",
396            "file": "LeanRsFixture/ProofActions.lean",
397            "declaration": "LeanRsFixture.ProofActions.stepTheorem",
398            "proof_position": { "kind": "default" }
399        })),
400        ("lean_trial", "proof_step") => Some(json!({
401            "kind": "proof_step",
402            "file": "LeanRsFixture/ProofActions.lean",
403            "declaration": "LeanRsFixture.ProofActions.stepTheorem",
404            "snippet": "trivial"
405        })),
406        ("lean_trial", "command") => Some(json!({
407            "kind": "command",
408            "imports": ["Init"],
409            "commands": "#check Nat.add\n#print axioms Nat.add_assoc"
410        })),
411        ("lean_verify", "targets") => Some(json!({
412            "targets": [{
413                "kind": "explicit",
414                "file": "LeanRsFixture/ProofActions.lean",
415                "declarations": ["LeanRsFixture.ProofActions.closedTheorem"]
416            }],
417            "allow_sorry": false,
418            "report_axioms": true
419        })),
420        ("lean_lookup", "declaration") => Some(json!({
421            "kind": "declaration",
422            "name": "Nat.add_zero",
423            "imports": ["Init"],
424            "fields": ["statement", "docstring"]
425        })),
426        ("lean_lookup", "declarations") => Some(json!({
427            "kind": "declarations",
428            "target": { "kind": "module", "module": "LeanRsFixture.ProofAgent" },
429            "limit": 200
430        })),
431        ("lean_lookup", "changed_coverage") => Some(json!({
432            "kind": "changed_coverage",
433            "base": "HEAD",
434            "files": ["LeanRsFixture/ProofActions.lean"],
435            "include_untracked": true
436        })),
437        ("lean_lookup", "proof_search") => Some(json!({
438            "kind": "proof_search",
439            "file": "LeanRsFixture/ProofAgent.lean",
440            "declaration": "LeanRsFixture.ProofAgent.miniRatDenominatorStep",
441            "mode": "next_step",
442            "limit": 10
443        })),
444        ("lean_lookup", "references") => Some(json!({
445            "kind": "references",
446            "name": "LeanRsFixture.ProofActions.closedTheorem",
447            "scope": "file",
448            "file": "LeanRsFixture/ProofActions.lean",
449            "limit": 20
450        })),
451        ("lean_status", "project") => Some(json!({
452            "kind": "project",
453            "include": ["toolchain", "worker", "artifacts"]
454        })),
455        ("lean_status", "file_diagnostics") => Some(json!({
456            "kind": "file_diagnostics",
457            "file": "LeanRsFixture/ProofActions.lean"
458        })),
459        _ => None,
460    }
461}
462
463fn semantic_examples(tool: &str, allowed: &[&str]) -> Option<Value> {
464    let examples = allowed
465        .iter()
466        .filter_map(|kind| semantic_example(tool, kind).map(|example| ((*kind).to_owned(), example)))
467        .collect::<serde_json::Map<_, _>>();
468    (!examples.is_empty()).then_some(Value::Object(examples))
469}
470
471#[derive(Debug, Clone, Serialize, JsonSchema)]
472pub struct SemanticTrust {
473    pub project_root: String,
474    pub session_id: String,
475    pub lean_toolchain: String,
476    #[serde(skip_serializing_if = "Vec::is_empty")]
477    pub artifacts: Vec<ArtifactTrust>,
478}
479
480impl SemanticTrust {
481    fn unknown() -> Self {
482        Self {
483            project_root: String::new(),
484            session_id: "request-invalid".to_owned(),
485            lean_toolchain: String::new(),
486            artifacts: Vec::new(),
487        }
488    }
489
490    fn from_parts(freshness: FreshnessIdentity, artifacts: Vec<ArtifactTrust>) -> Self {
491        Self {
492            project_root: freshness.project_root,
493            session_id: freshness.session_id,
494            lean_toolchain: freshness.lean_toolchain,
495            artifacts: dedupe_artifacts(artifacts),
496        }
497    }
498}
499
500impl From<FreshnessIdentity> for SemanticTrust {
501    fn from(freshness: FreshnessIdentity) -> Self {
502        Self::from_parts(freshness, Vec::new())
503    }
504}
505
506#[derive(Debug, Clone, Serialize, JsonSchema)]
507pub struct SemanticIssue {
508    pub code: String,
509    pub message: String,
510    #[serde(skip_serializing_if = "Option::is_none")]
511    pub severity: Option<String>,
512    #[serde(skip_serializing_if = "Option::is_none")]
513    pub next_action: Option<String>,
514    #[serde(skip_serializing_if = "Option::is_none")]
515    pub retryable: Option<bool>,
516    #[serde(skip_serializing_if = "Option::is_none")]
517    pub details: Option<Value>,
518}
519
520#[derive(Debug, Clone, Serialize, JsonSchema)]
521pub struct SemanticResponse<T>
522where
523    T: Serialize + JsonSchema,
524{
525    pub data: Option<T>,
526    pub errors: Vec<SemanticIssue>,
527    pub trust: SemanticTrust,
528}
529
530#[derive(Debug, Clone, Serialize, JsonSchema)]
531pub struct LeanStatusData {
532    pub kind: String,
533    pub project_root: String,
534    pub lean_toolchain: String,
535    pub include: Vec<String>,
536    pub worker_opened: bool,
537    #[serde(skip_serializing_if = "Option::is_none")]
538    pub worker: Option<WorkerStatusData>,
539    #[serde(skip_serializing_if = "Vec::is_empty")]
540    pub artifacts: Vec<ArtifactTrust>,
541    pub broker: BrokerConfigSnapshot,
542    pub output: OutputStatus,
543}
544
545#[derive(Debug, Clone, Serialize, JsonSchema)]
546pub struct WorkerStatusData {
547    pub opened: bool,
548    pub status: TrustStatus,
549    pub detail: String,
550}
551
552#[derive(Debug, Clone, Serialize, JsonSchema)]
553pub struct OutputStatus {
554    pub response_carrier: String,
555    pub telemetry_verbosity: String,
556}
557
558#[derive(Debug, Clone, Deserialize)]
559struct StatusRequest {
560    #[serde(default)]
561    project: Option<String>,
562    #[serde(default)]
563    include: Vec<StatusInclude>,
564}
565
566#[derive(Debug, Clone, Copy, PartialEq, Eq, Deserialize)]
567#[serde(rename_all = "snake_case")]
568enum StatusInclude {
569    Toolchain,
570    Worker,
571    Artifacts,
572}
573
574impl StatusInclude {
575    fn as_str(self) -> &'static str {
576        match self {
577            Self::Toolchain => "toolchain",
578            Self::Worker => "worker",
579            Self::Artifacts => "artifacts",
580        }
581    }
582}
583
584/// Proof/term context tool. Initial public mode: `proof_position`.
585///
586/// # Errors
587///
588/// Returns infrastructure failures only; invalid semantic modes are returned as
589/// structured semantic errors.
590pub async fn lean_context(ctx: &ToolContext, req: SemanticToolRequest) -> Result<SemanticResponse<Value>> {
591    match req.kind() {
592        Some("proof_position") => {
593            let request = match decode::<ProofStateRequest>(req, semantic_example("lean_context", "proof_position")) {
594                Ok(request) => request,
595                Err(response) => return Ok(*response),
596            };
597            from_tool_response(position::proof_state(ctx, request).await?, ctx.config.verbosity)
598        }
599        Some(kind) => Ok(invalid_kind("lean_context", kind, &["proof_position"])),
600        None => Ok(missing_kind("lean_context", &["proof_position"])),
601    }
602}
603
604/// Non-mutating Lean experiments.
605///
606/// # Errors
607///
608/// Returns infrastructure failures only; invalid semantic modes are returned as
609/// structured semantic errors.
610pub async fn lean_trial(ctx: &ToolContext, req: SemanticToolRequest) -> Result<SemanticResponse<Value>> {
611    match req.kind() {
612        Some("proof_step") => {
613            let request = match decode::<TryProofStepRequest>(req, semantic_example("lean_trial", "proof_step")) {
614                Ok(request) => request,
615                Err(response) => return Ok(*response),
616            };
617            from_tool_response(proof_action::try_proof_step(ctx, request).await?, ctx.config.verbosity)
618        }
619        Some("command") => {
620            let request = match decode::<CommandTrialRequest>(req, semantic_example("lean_trial", "command")) {
621                Ok(request) => request,
622                Err(response) => return Ok(*response),
623            };
624            from_tool_response(position::command_trial(ctx, request).await?, ctx.config.verbosity)
625        }
626        Some(kind) => Ok(invalid_kind("lean_trial", kind, &["proof_step", "command"])),
627        None => Ok(missing_kind("lean_trial", &["proof_step", "command"])),
628    }
629}
630
631/// Declaration verification for explicit, file-wide, and module-wide target groups.
632///
633/// # Errors
634///
635/// Returns infrastructure failures only; invalid semantic modes are returned as
636/// structured semantic errors.
637pub async fn lean_verify(ctx: &ToolContext, req: SemanticToolRequest) -> Result<SemanticResponse<Value>> {
638    match req.kind() {
639        None => {
640            let request = match decode::<LeanVerifyRequest>(req, semantic_example("lean_verify", "targets")) {
641                Ok(request) => request,
642                Err(response) => return Ok(*response),
643            };
644            lean_verify_targets(ctx, request).await
645        }
646        Some(kind) => Ok(invalid_kind("lean_verify", kind, &[])),
647    }
648}
649
650/// Declaration-verification entry point for the public MCP handler.
651///
652/// `lean_verify` is intentionally not kind-dispatched, but the MCP handler
653/// accepts raw JSON so malformed target groups can be reported through the same
654/// structured semantic envelope as the other public tools.
655///
656/// # Errors
657///
658/// Returns infrastructure failures only; malformed requests are structured
659/// semantic data.
660pub async fn lean_verify_raw(ctx: &ToolContext, value: Value) -> Result<SemanticResponse<Value>> {
661    if let Some(kind) = value
662        .get("kind")
663        .and_then(Value::as_str)
664        .map(str::trim)
665        .filter(|kind| !kind.is_empty())
666    {
667        return Ok(invalid_kind("lean_verify", kind, &[]));
668    }
669    let request = match decode_value::<LeanVerifyRequest>(value, semantic_example("lean_verify", "targets")) {
670        Ok(request) => request,
671        Err(response) => return Ok(*response),
672    };
673    lean_verify_targets(ctx, request).await
674}
675
676/// Typed declaration-verification entry point for the public MCP handler.
677///
678/// Unlike the kind-dispatched semantic families, `lean_verify` has no `kind`
679/// namespace: its top-level request is the target-group batch itself.
680///
681/// # Errors
682///
683/// Returns infrastructure failures only; per-declaration Lean failures remain
684/// structured semantic data.
685pub async fn lean_verify_targets(ctx: &ToolContext, request: LeanVerifyRequest) -> Result<SemanticResponse<Value>> {
686    from_tool_response(proof_action::verify_targets(ctx, request).await?, ctx.config.verbosity)
687}
688
689/// Semantic lookup and discovery.
690///
691/// Initial public modes: `declaration`, `declarations`, `changed_coverage`,
692/// `proof_search`, and `references`.
693///
694/// # Errors
695///
696/// Returns infrastructure failures only; invalid semantic modes are returned as
697/// structured semantic errors.
698pub async fn lean_lookup(ctx: &ToolContext, req: SemanticToolRequest) -> Result<SemanticResponse<Value>> {
699    match req.kind() {
700        Some("declaration") => {
701            let request = match decode::<InspectDeclarationRequest>(req, semantic_example("lean_lookup", "declaration"))
702            {
703                Ok(request) => request,
704                Err(response) => return Ok(*response),
705            };
706            from_tool_response(
707                declaration::inspect_declaration(ctx, request).await?,
708                ctx.config.verbosity,
709            )
710        }
711        Some("declarations") => {
712            let request =
713                match decode::<DeclarationInventoryRequest>(req, semantic_example("lean_lookup", "declarations")) {
714                    Ok(request) => request,
715                    Err(response) => return Ok(*response),
716                };
717            from_tool_response(
718                declaration_inventory::declaration_inventory(ctx, request).await?,
719                ctx.config.verbosity,
720            )
721        }
722        Some("changed_coverage") => {
723            let request =
724                match decode::<ChangedCoverageRequest>(req, semantic_example("lean_lookup", "changed_coverage")) {
725                    Ok(request) => request,
726                    Err(response) => return Ok(*response),
727                };
728            from_tool_response(
729                changed_coverage::changed_coverage(ctx, request).await?,
730                ctx.config.verbosity,
731            )
732        }
733        Some("proof_search") => {
734            let request = match decode::<SearchForProofRequest>(req, semantic_example("lean_lookup", "proof_search")) {
735                Ok(request) => request,
736                Err(response) => return Ok(*response),
737            };
738            from_tool_response(
739                proof_search::search_for_proof(ctx, request).await?,
740                ctx.config.verbosity,
741            )
742        }
743        Some("references") => {
744            let request = match decode::<FindReferencesRequest>(req, semantic_example("lean_lookup", "references")) {
745                Ok(request) => request,
746                Err(response) => return Ok(*response),
747            };
748            from_tool_response(position::find_references(ctx, request).await?, ctx.config.verbosity)
749        }
750        Some(kind) => Ok(invalid_kind(
751            "lean_lookup",
752            kind,
753            &[
754                "declaration",
755                "declarations",
756                "changed_coverage",
757                "proof_search",
758                "references",
759            ],
760        )),
761        None => Ok(missing_kind(
762            "lean_lookup",
763            &[
764                "declaration",
765                "declarations",
766                "changed_coverage",
767                "proof_search",
768                "references",
769            ],
770        )),
771    }
772}
773
774/// Cheap project/toolchain/config status. Does not open a worker.
775///
776/// # Errors
777///
778/// Returns Lake-project resolution failures. Invalid semantic modes are
779/// returned as structured semantic errors.
780pub async fn lean_status(ctx: &ToolContext, req: SemanticToolRequest) -> Result<SemanticResponse<Value>> {
781    let kind = req.kind().unwrap_or("project").to_owned();
782    match kind.as_str() {
783        "project" => {
784            let request = match decode::<StatusRequest>(req, semantic_example("lean_status", "project")) {
785                Ok(request) => request,
786                Err(response) => return Ok(*response),
787            };
788            let hint = ProjectHint::from_request(request.project);
789            let identity = ctx.broker.project_identity_without_worker(&hint, Vec::new())?;
790            let project_root = identity.freshness.project_root.clone();
791            let includes = status_includes(&request.include);
792            let mut artifacts = Vec::new();
793            let worker = includes.contains(&StatusInclude::Worker).then(|| WorkerStatusData {
794                opened: false,
795                status: TrustStatus::NotApplicable,
796                detail: "lean_status does not open a worker".to_owned(),
797            });
798            if worker.is_some() {
799                artifacts.push(ArtifactTrust::worker_toolchain_not_applicable(
800                    "lean_status did not open a worker to inspect runtime generation",
801                ));
802            }
803            if includes.contains(&StatusInclude::Artifacts) {
804                artifacts.extend(status_artifact_facts(Path::new(&project_root)));
805            }
806            let mut trust = SemanticTrust::from(Response::<()>::ok((), identity.freshness).freshness);
807            trust.artifacts.clone_from(&artifacts);
808            let data = LeanStatusData {
809                kind: "project".to_owned(),
810                project_root: trust.project_root.clone(),
811                lean_toolchain: trust.lean_toolchain.clone(),
812                include: includes
813                    .iter()
814                    .copied()
815                    .map(StatusInclude::as_str)
816                    .map(str::to_owned)
817                    .collect(),
818                worker_opened: false,
819                worker,
820                artifacts,
821                broker: ctx.broker.config_snapshot(),
822                output: OutputStatus {
823                    response_carrier: response_carrier_name(ctx.config.carrier).to_owned(),
824                    telemetry_verbosity: telemetry_verbosity_name(ctx.config.verbosity).to_owned(),
825                },
826            };
827            Ok(SemanticResponse {
828                data: Some(serde_json::to_value(data).map_err(|err| ServerError::Internal(err.to_string()))?),
829                errors: Vec::new(),
830                trust,
831            })
832        }
833        "file_diagnostics" => {
834            let request =
835                match decode::<FileDiagnosticsRequest>(req, semantic_example("lean_status", "file_diagnostics")) {
836                    Ok(request) => request,
837                    Err(response) => return Ok(*response),
838                };
839            from_tool_response(position::file_diagnostics(ctx, request).await?, ctx.config.verbosity)
840        }
841        other => Ok(invalid_kind("lean_status", other, &["project", "file_diagnostics"])),
842    }
843}
844
845pub(crate) fn from_worker_unavailable(info: &WorkerUnavailable) -> SemanticResponse<Value> {
846    let mut old = Response::<Value>::runtime_unavailable(info.failure(), info.freshness(), info.runtime.clone())
847        .with_trust_artifact(ArtifactTrust::worker_toolchain_unknown(
848            "worker runtime was unavailable for this request",
849        ));
850    old.drain_advisories();
851    from_runtime_response(old)
852}
853
854fn from_tool_response<T>(mut response: Response<T>, verbosity: TelemetryVerbosity) -> Result<SemanticResponse<Value>>
855where
856    T: Serialize + JsonSchema,
857{
858    response.drain_advisories();
859    if !verbosity.is_full() {
860        response.drop_telemetry();
861    }
862    let data = response
863        .result
864        .map(serde_json::to_value)
865        .transpose()
866        .map_err(|err| ServerError::Internal(err.to_string()))?;
867    let trust = SemanticTrust::from_parts(response.freshness, response.trust_artifacts);
868    let errors = semantic_issues(response.runtime_error, response.warnings, response.next_actions);
869    Ok(SemanticResponse { data, errors, trust })
870}
871
872fn from_runtime_response(response: Response<Value>) -> SemanticResponse<Value> {
873    let trust = SemanticTrust::from_parts(response.freshness, response.trust_artifacts);
874    let errors = semantic_issues(response.runtime_error, response.warnings, response.next_actions);
875    SemanticResponse {
876        data: response.result,
877        errors,
878        trust,
879    }
880}
881
882fn status_includes(include: &[StatusInclude]) -> Vec<StatusInclude> {
883    if include.is_empty() {
884        vec![
885            StatusInclude::Toolchain,
886            StatusInclude::Worker,
887            StatusInclude::Artifacts,
888        ]
889    } else {
890        include.to_vec()
891    }
892}
893
894fn status_artifact_facts(root: &Path) -> Vec<ArtifactTrust> {
895    let build_tree = root.join(".lake/build/lib/lean");
896    if build_tree.is_dir() {
897        let path = build_tree.to_string_lossy().into_owned();
898        vec![
899            ArtifactTrust::build_tree_unknown(path.clone(), ArtifactKind::Olean),
900            ArtifactTrust::build_tree_unknown(path, ArtifactKind::Ilean),
901        ]
902    } else {
903        vec![
904            ArtifactTrust::olean_project_missing_build(".lake/build/lib/lean is absent"),
905            ArtifactTrust::ilean_project_missing_build(),
906        ]
907    }
908}
909
910fn semantic_issues(
911    runtime_error: Option<RuntimeFailure>,
912    warnings: Vec<String>,
913    next_actions: Vec<String>,
914) -> Vec<SemanticIssue> {
915    let mut out = Vec::new();
916    if let Some(error) = runtime_error {
917        let retryable = error.retryable;
918        out.push(SemanticIssue {
919            code: "runtime_unavailable".to_owned(),
920            message: error.reason.clone(),
921            severity: Some("error".to_owned()),
922            next_action: None,
923            retryable: Some(retryable),
924            details: serde_json::to_value(error).ok(),
925        });
926    }
927    let mut next_actions = next_actions.into_iter();
928    for warning in warnings {
929        out.push(SemanticIssue {
930            code: "warning".to_owned(),
931            message: warning,
932            severity: Some("warning".to_owned()),
933            next_action: next_actions.next(),
934            retryable: None,
935            details: None,
936        });
937    }
938    out
939}
940
941fn decode<T>(req: SemanticToolRequest, example: Option<Value>) -> std::result::Result<T, Box<SemanticResponse<Value>>>
942where
943    T: DeserializeOwned,
944{
945    let value = Value::Object(req.args.into_iter().collect());
946    decode_value(value, example)
947}
948
949fn decode_value<T>(value: Value, example: Option<Value>) -> std::result::Result<T, Box<SemanticResponse<Value>>>
950where
951    T: DeserializeOwned,
952{
953    serde_json::from_value(value).map_err(|err| {
954        let has_example = example.is_some();
955        let details = example.map(|example| json!({ "example": example }));
956        Box::new(SemanticResponse {
957            data: None,
958            errors: vec![SemanticIssue {
959                code: "invalid_request".to_owned(),
960                message: err.to_string(),
961                severity: Some("error".to_owned()),
962                next_action: has_example.then(|| "Retry with a request shaped like `details.example`.".to_owned()),
963                retryable: Some(false),
964                details,
965            }],
966            trust: SemanticTrust::unknown(),
967        })
968    })
969}
970
971fn missing_kind(tool: &str, allowed: &[&str]) -> SemanticResponse<Value> {
972    SemanticResponse {
973        data: None,
974        errors: vec![SemanticIssue {
975            code: "missing_kind".to_owned(),
976            message: format!("{tool} requires `kind`; allowed: {}", allowed.join(", ")),
977            severity: Some("error".to_owned()),
978            next_action: Some("Choose one of the allowed modes; see `details.examples`.".to_owned()),
979            retryable: Some(false),
980            details: semantic_examples(tool, allowed).map(|examples| json!({ "examples": examples })),
981        }],
982        trust: SemanticTrust::unknown(),
983    }
984}
985
986fn invalid_kind(tool: &str, kind: &str, allowed: &[&str]) -> SemanticResponse<Value> {
987    let message = if allowed.is_empty() {
988        format!("{tool} does not support kind `{kind}`; omit `kind` for this tool")
989    } else {
990        format!("{tool} does not support kind `{kind}`; allowed: {}", allowed.join(", "))
991    };
992    SemanticResponse {
993        data: None,
994        errors: vec![SemanticIssue {
995            code: "invalid_kind".to_owned(),
996            message,
997            severity: Some("error".to_owned()),
998            next_action: (!allowed.is_empty())
999                .then(|| "Choose one of the allowed modes; see `details.examples`.".to_owned()),
1000            retryable: Some(false),
1001            details: semantic_examples(tool, allowed).map(|examples| json!({ "examples": examples })),
1002        }],
1003        trust: SemanticTrust::unknown(),
1004    }
1005}
1006
1007fn response_carrier_name(carrier: ResponseCarrier) -> &'static str {
1008    match carrier {
1009        ResponseCarrier::Text => "text",
1010        ResponseCarrier::Structured => "structured",
1011        ResponseCarrier::Both => "both",
1012    }
1013}
1014
1015fn telemetry_verbosity_name(verbosity: TelemetryVerbosity) -> &'static str {
1016    match verbosity {
1017        TelemetryVerbosity::Quiet => "quiet",
1018        TelemetryVerbosity::Full => "full",
1019    }
1020}
1021
1022#[cfg(test)]
1023#[allow(clippy::unwrap_used)]
1024mod tests {
1025    use super::*;
1026    use crate::broker::{BrokerConfig, ProjectBroker};
1027    use crate::envelope::Freshness;
1028    use crate::tools::ToolConfig;
1029    use crate::trust::{ArtifactKind, TrustScope};
1030
1031    fn make_lake_dir(root: &std::path::Path) -> std::path::PathBuf {
1032        let dir = root.join("status");
1033        std::fs::create_dir_all(&dir).unwrap();
1034        std::fs::write(dir.join("lakefile.lean"), "package status\nlean_lib Status\n").unwrap();
1035        std::fs::write(dir.join("lean-toolchain"), "leanprover/lean4:v4.31.0-rc2\n").unwrap();
1036        std::fs::write(dir.join("lake-manifest.json"), "{}\n").unwrap();
1037        dir.canonicalize().unwrap()
1038    }
1039
1040    fn freshness(root: &std::path::Path) -> Freshness {
1041        Freshness {
1042            project_root: root.to_string_lossy().into_owned(),
1043            project_hash: "hash".to_owned(),
1044            imports: vec!["Init".to_owned()],
1045            session_id: "test-session".to_owned(),
1046            lean_toolchain: "leanprover/lean4:v4.31.0-rc2".to_owned(),
1047            toolchain_advisories: Vec::new(),
1048        }
1049    }
1050
1051    #[tokio::test]
1052    async fn lean_status_does_not_open_worker_and_reports_trust_artifacts() {
1053        let tmp = tempfile::tempdir().unwrap();
1054        let root = make_lake_dir(tmp.path());
1055        let broker = ProjectBroker::new(BrokerConfig {
1056            config_default: None,
1057            env_default: Some(root.clone()),
1058            cwd: root,
1059            max_projects: BrokerConfig::default_max_projects(),
1060            idle_timeout: std::time::Duration::ZERO,
1061            semantic_permits: BrokerConfig::default_semantic_permits(),
1062            semantic_waiters: BrokerConfig::default_semantic_waiters(),
1063            semantic_admission_timeout: BrokerConfig::default_semantic_admission_timeout(),
1064            semantic_lock_dir: BrokerConfig::default_semantic_lock_dir(),
1065        });
1066        let ctx = ToolContext {
1067            broker: std::sync::Arc::clone(&broker),
1068            config: ToolConfig::default(),
1069        };
1070
1071        let response = lean_status(
1072            &ctx,
1073            SemanticToolRequest {
1074                kind: Some("project".to_owned()),
1075                args: BTreeMap::from([(
1076                    "include".to_owned(),
1077                    serde_json::json!(["toolchain", "worker", "artifacts"]),
1078                )]),
1079            },
1080        )
1081        .await
1082        .unwrap();
1083
1084        assert!(response.errors.is_empty());
1085        assert_eq!(response.trust.session_id, "metadata-only");
1086        assert!(response.trust.artifacts.iter().any(|artifact| {
1087            artifact.artifact == ArtifactKind::Worker
1088                && artifact.scope == TrustScope::Toolchain
1089                && artifact.status == TrustStatus::NotApplicable
1090        }));
1091        assert!(response.trust.artifacts.iter().any(|artifact| {
1092            artifact.artifact == ArtifactKind::Olean && artifact.status == TrustStatus::MissingBuild
1093        }));
1094        assert!(broker.resident_paths().is_empty());
1095        drop(ctx);
1096        drop(broker);
1097    }
1098
1099    #[test]
1100    fn quiet_telemetry_does_not_drop_trust_artifacts() {
1101        let tmp = tempfile::tempdir().unwrap();
1102        let response = Response::ok(serde_json::json!({"status": "ok"}), freshness(tmp.path()))
1103            .with_trust_artifact(ArtifactTrust::ilean_project_missing_build());
1104
1105        let semantic = from_tool_response(response, TelemetryVerbosity::Quiet).unwrap();
1106        let json = serde_json::to_value(&semantic).unwrap();
1107
1108        assert!(json.get("telemetry").is_none());
1109        assert_eq!(
1110            json.pointer("/trust/artifacts/0/artifact")
1111                .and_then(serde_json::Value::as_str),
1112            Some("ilean")
1113        );
1114        assert_eq!(
1115            json.pointer("/trust/artifacts/0/status")
1116                .and_then(serde_json::Value::as_str),
1117            Some("missing_build")
1118        );
1119    }
1120
1121    #[tokio::test]
1122    async fn semantic_surface_invalid_kind_is_payload_error() {
1123        let tmp = tempfile::tempdir().unwrap();
1124        let root = make_lake_dir(tmp.path());
1125        let broker = ProjectBroker::new(BrokerConfig {
1126            config_default: None,
1127            env_default: Some(root),
1128            cwd: tmp.path().to_path_buf(),
1129            max_projects: BrokerConfig::default_max_projects(),
1130            idle_timeout: std::time::Duration::ZERO,
1131            semantic_permits: BrokerConfig::default_semantic_permits(),
1132            semantic_waiters: BrokerConfig::default_semantic_waiters(),
1133            semantic_admission_timeout: BrokerConfig::default_semantic_admission_timeout(),
1134            semantic_lock_dir: BrokerConfig::default_semantic_lock_dir(),
1135        });
1136        let ctx = ToolContext {
1137            broker: std::sync::Arc::clone(&broker),
1138            config: ToolConfig::default(),
1139        };
1140
1141        let response = lean_context(
1142            &ctx,
1143            SemanticToolRequest {
1144                kind: Some("raw_hover".to_owned()),
1145                args: BTreeMap::new(),
1146            },
1147        )
1148        .await
1149        .unwrap();
1150
1151        assert!(response.data.is_none());
1152        let error = response.errors.first();
1153        assert!(matches!(error.map(|issue| issue.code.as_str()), Some("invalid_kind")));
1154        assert!(matches!(error.and_then(|issue| issue.retryable), Some(false)));
1155        drop(ctx);
1156        drop(broker);
1157    }
1158
1159    #[tokio::test]
1160    async fn invalid_request_error_carries_kind_example() {
1161        let tmp = tempfile::tempdir().unwrap();
1162        let root = make_lake_dir(tmp.path());
1163        let broker = ProjectBroker::new(BrokerConfig {
1164            config_default: None,
1165            env_default: Some(root),
1166            cwd: tmp.path().to_path_buf(),
1167            max_projects: BrokerConfig::default_max_projects(),
1168            idle_timeout: std::time::Duration::ZERO,
1169            semantic_permits: BrokerConfig::default_semantic_permits(),
1170            semantic_waiters: BrokerConfig::default_semantic_waiters(),
1171            semantic_admission_timeout: BrokerConfig::default_semantic_admission_timeout(),
1172            semantic_lock_dir: BrokerConfig::default_semantic_lock_dir(),
1173        });
1174        let ctx = ToolContext {
1175            broker: std::sync::Arc::clone(&broker),
1176            config: ToolConfig::default(),
1177        };
1178
1179        let response = lean_lookup(
1180            &ctx,
1181            SemanticToolRequest {
1182                kind: Some("declarations".to_owned()),
1183                args: BTreeMap::new(),
1184            },
1185        )
1186        .await
1187        .unwrap();
1188
1189        assert!(response.data.is_none());
1190        let error = response.errors.first().unwrap();
1191        assert_eq!(error.code, "invalid_request");
1192        assert_eq!(
1193            error.details.as_ref().and_then(|details| {
1194                details
1195                    .pointer("/example/target/kind")
1196                    .and_then(serde_json::Value::as_str)
1197            }),
1198            Some("module")
1199        );
1200        assert!(
1201            error
1202                .next_action
1203                .as_deref()
1204                .is_some_and(|action| action.contains("details.example"))
1205        );
1206        drop(ctx);
1207        drop(broker);
1208    }
1209
1210    #[tokio::test]
1211    async fn lean_verify_raw_invalid_target_group_is_payload_error() {
1212        let tmp = tempfile::tempdir().unwrap();
1213        let root = make_lake_dir(tmp.path());
1214        let broker = ProjectBroker::new(BrokerConfig {
1215            config_default: None,
1216            env_default: Some(root),
1217            cwd: tmp.path().to_path_buf(),
1218            max_projects: BrokerConfig::default_max_projects(),
1219            idle_timeout: std::time::Duration::ZERO,
1220            semantic_permits: BrokerConfig::default_semantic_permits(),
1221            semantic_waiters: BrokerConfig::default_semantic_waiters(),
1222            semantic_admission_timeout: BrokerConfig::default_semantic_admission_timeout(),
1223            semantic_lock_dir: BrokerConfig::default_semantic_lock_dir(),
1224        });
1225        let ctx = ToolContext {
1226            broker: std::sync::Arc::clone(&broker),
1227            config: ToolConfig::default(),
1228        };
1229
1230        let response = lean_verify_raw(
1231            &ctx,
1232            json!({
1233                "targets": [{
1234                    "kind": "bogus_group",
1235                    "file": "LeanRsFixture/ProofActions.lean"
1236                }]
1237            }),
1238        )
1239        .await
1240        .unwrap();
1241
1242        assert!(response.data.is_none());
1243        let error = response.errors.first().unwrap();
1244        assert_eq!(error.code, "invalid_request");
1245        assert!(error.message.contains("bogus_group"));
1246        assert_eq!(
1247            error.details.as_ref().and_then(|details| {
1248                details
1249                    .pointer("/example/targets/0/kind")
1250                    .and_then(serde_json::Value::as_str)
1251            }),
1252            Some("explicit")
1253        );
1254        assert!(matches!(error.retryable, Some(false)));
1255        drop(ctx);
1256        drop(broker);
1257    }
1258
1259    #[test]
1260    fn tool_catalog_documents_semantic_surface() {
1261        let catalog = include_str!("../../../../docs/tool-catalog.md");
1262        for tool in [
1263            "lean_context",
1264            "lean_trial",
1265            "lean_verify",
1266            "lean_lookup",
1267            "lean_status",
1268        ] {
1269            assert!(catalog.contains(tool), "catalog should document {tool}");
1270        }
1271        for phrase in [
1272            "Common Workflows",
1273            "Verify One Declaration With Axiom Reporting",
1274            "Tagged Request Shapes",
1275            "LEAN_HOST_MCP_RESPONSE_CARRIER=structured",
1276            "lean_trial",
1277            "lean_context",
1278            "lean_verify",
1279        ] {
1280            assert!(catalog.contains(phrase), "catalog should document {phrase}");
1281        }
1282        for old_heading in [
1283            "## `proof_state`",
1284            "## `search_for_proof`",
1285            "## `inspect_declaration`",
1286            "## `try_proof_step`",
1287            "## `verify_declaration`",
1288            "## `find_references`",
1289        ] {
1290            assert!(
1291                !catalog.contains(old_heading),
1292                "catalog must not keep old public section {old_heading}"
1293            );
1294        }
1295    }
1296}
lean_host_mcp/tools/semantic.rs

lean_host_mcp/tools/
semantic.rs
