lean_host_mcp/
lib.rs

1//! Library surface for `lean-host-mcp`.
2//!
3//! The MCP server is one binary, but its pieces are crate-public for
4//! integration tests and for downstream consumers who want to embed the
5//! handlers in their own transport (e.g. SSE instead of stdio).
6//!
7//! Layout:
8//!
9//! - [`envelope`]: the uniform
10//!   `{result, freshness, runtime, warnings, next_actions}` wrapper every
11//!   semantic tool returns.
12//! - [`broker`]: `ProjectBroker`, the mediator that resolves a per-call
13//!   project hint into typed operations on a private project runtime via the
14//!   env / cwd-walk / config-default chain.
15//! - `project`: private per-project actor runtime. Owns one supervised worker
16//!   actor and the bounded module-query cache for one Lake project.
17//! - [`projections`]: pure data-shuffle projection types and helpers from
18//!   `lean-rs-worker` shapes into the wire shapes the MCP envelope carries.
19//! - [`lake_meta`]: `LakeProjectMeta`, the minimal description of a Lake
20//!   project that the private project runtime consumes.
21//! - [`error`]: `ServerError`, the one error type tool handlers return.
22//! - [`tools`]: tool implementations, grouped by proof workflow stage.
23//! - [`server`]: rmcp glue.
24
25mod admission;
26pub mod broker;
27mod cache;
28pub mod cli;
29pub mod config_file;
30pub mod config_schema;
31mod diagnosis;
32pub mod envelope;
33pub mod error;
34mod ilean;
35pub mod lake_meta;
36mod project;
37pub mod projections;
38mod semantic_search;
39pub mod server;
40mod smoke;
41pub mod toolchain;
42pub mod tools;
43
44pub use broker::{BrokerConfig, ProjectBroker, ProjectHint};
45pub use config_file::ConfigFile;
46pub use envelope::{Freshness, Response, ResponseStatus, RuntimeFacts, RuntimeFailure};
47pub use error::{Result, ServerError};
48pub use lake_meta::LakeProjectMeta;
49pub use project::ProjectRuntimeConfig;
50pub use projections::{
51    DeclarationFlags, DeclarationInspection, DeclarationInspectionResult, DeclarationProofSearchFacts, DeclarationRow,
52    DeclarationSearchFacts, DeclarationSearchPruning, DeclarationSearchResult, DeclarationSearchTimings,
53    DeclarationSummary, DeclarationVerificationFacts, DeclarationVerificationResult, Diagnostic, ElabFailure,
54    ElabSuccess, KernelOutcome, KernelSummary, MetaOutcome, ModuleSourceSpan, Position, ProofActionDeclarationTarget,
55    ProofAttemptCandidate, ProofAttemptEnvelope, ProofAttemptResult, RenderedText, Severity, SourceRange,
56};
57pub use server::LeanHostService;
58pub use toolchain::{ToolchainError, ToolchainId, WorkerBinary};
59pub use tools::{OutputBudgetOverrides, ResponseCarrier, TelemetryVerbosity, ToolConfig};
lean_host_mcp/lib.rs

lean_host_mcp/
lib.rs
