Crate lean_host_mcp 

Library surface for lean-host-mcp.

The MCP server is one binary, but its pieces are crate-public for integration tests and for downstream consumers who want to embed the handlers in their own transport (e.g. SSE instead of stdio).

Layout:

• envelope: the uniform {result, freshness, runtime, warnings, next_actions} wrapper every semantic tool returns.
• broker: ProjectBroker, the mediator that resolves a per-call project hint into typed operations on a private project runtime via the env / cwd-walk / config-default chain.
• project: private per-project actor runtime. Owns one supervised worker actor and the bounded module-query cache for one Lake project.
• projections: pure data-shuffle projection types and helpers from lean-rs-worker shapes into the wire shapes the MCP envelope carries.
• lake_meta: LakeProjectMeta, the minimal description of a Lake project that the private project runtime consumes.
• error: ServerError, the one error type tool handlers return.
• tools: tool implementations, grouped by proof workflow stage.
• server: rmcp glue.

Re-exports

pub use broker::BrokerConfig;

pub use broker::ProjectBroker;

pub use broker::ProjectHint;

pub use config_file::ConfigFile;

pub use envelope::Freshness;

pub use envelope::Response;

pub use envelope::ResponseStatus;

pub use envelope::RuntimeFacts;

pub use envelope::RuntimeFailure;

pub use error::Result;

pub use error::ServerError;

pub use lake_meta::LakeProjectMeta;

pub use projections::DeclarationFlags;

pub use projections::DeclarationInspection;

pub use projections::DeclarationInspectionResult;

pub use projections::DeclarationProofSearchFacts;

pub use projections::DeclarationRow;

pub use projections::DeclarationSearchFacts;

pub use projections::DeclarationSearchPruning;

pub use projections::DeclarationSearchResult;

pub use projections::DeclarationSearchTimings;

pub use projections::DeclarationSummary;

pub use projections::DeclarationVerificationFacts;

pub use projections::DeclarationVerificationResult;

pub use projections::Diagnostic;

pub use projections::ElabFailure;

pub use projections::ElabSuccess;

pub use projections::KernelOutcome;

pub use projections::KernelSummary;

pub use projections::MetaOutcome;

pub use projections::ModuleSourceSpan;

pub use projections::Position;

pub use projections::ProofActionDeclarationTarget;

pub use projections::ProofAttemptCandidate;

pub use projections::ProofAttemptEnvelope;

pub use projections::ProofAttemptResult;

pub use projections::RenderedText;

pub use projections::Severity;

pub use projections::SourceRange;

pub use server::LeanHostService;

pub use toolchain::ToolchainError;

pub use toolchain::ToolchainId;

pub use toolchain::WorkerBinary;

pub use tools::OutputBudgetOverrides;

pub use tools::ResponseCarrier;

pub use tools::TelemetryVerbosity;

pub use tools::ToolConfig;

Modules

broker

ProjectBroker: the mediator between MCP tool dispatch and the private per-project Lean runtime.

cli

CLI subcommand wiring.

config_file

Optional TOML config file holding every tunable knob.

config_schema

The one catalogue of every configuration knob.

envelope

The uniform response envelope every tool returns.

error

The one error type tool handlers return.

lake_meta

Description of a Lake project plus the discovery logic that builds one from a directory hint.

projections

Pure data-shuffle projections from lean-rs-worker types into the MCP-stable wire shapes.

server

rmcp server glue. Registers model-facing Lean tools and wires them to the tools module.

toolchain

Resolve a Lake project’s lean-toolchain pin to the matching per-toolchain worker binary on disk.

tools

Tool implementations.

Structs

ProjectRuntimeConfig

Runtime policy for one private project actor.