[package]
authors.workspace = true
categories = ["development-tools"]
description = "MCP server hosting Lean 4 via a supervised lean-rs-worker child"
edition.workspace = true
keywords = ["lean", "lean4", "mcp", "theorem-proving"]
license.workspace = true
name = "lean-host-mcp"
readme = "README.md"
repository.workspace = true
rust-version.workspace = true
version.workspace = true

[lib]
name = "lean_host_mcp"
path = "src/lib.rs"

[[bin]]
name = "lean-host-mcp"
path = "src/main.rs"

[[bench]]
harness = false
name = "worker_roundtrip"

[[bench]]
harness = false
name = "worker_cold_spawn"

[[bench]]
harness = false
name = "module_query_roundtrip"

[[bench]]
harness = false
name = "multi_project_dispatch"

[dependencies]
anyhow = "1"
axum = { version = "0.8", default-features = false, features = ["http1", "tokio"] }
clap = { version = "4", features = ["derive", "env"] }
dirs = "6"
lru = "0.18"
parking_lot = "0.12"
regex = "1"
rmcp = { version = "1.7", features = [
  "macros",
  "schemars",
  "server",
  "transport-io",
  "transport-streamable-http-server",
] }
schemars = "1.2"
serde = { version = "1", features = ["derive"] }
serde_json = "1"
sha2 = "0.11"
# Throwaway working directory for the install-time worker smoke test (smoke.rs).
tempfile = "3"
thiserror = "2"
tokio = { version = "1", features = ["macros", "net", "rt-multi-thread", "signal", "sync", "time"] }
tokio-util = "0.7"
toml = "1"
tracing = "0.1"
tracing-subscriber = { version = "0.3", features = ["env-filter", "fmt"] }
uuid = { version = "1", features = ["v4"] }
walkdir = "2"

lean-rs-worker-parent = "0.1.20"
# Non-FFI facade over lean-rs-sys (metadata-only, no link directives): supplies
# the supported-toolchain window. Already in the parent's closure via
# lean-rs-worker-parent, so this direct dep adds no new linkage. The parent must
# stay free of libleanshared — see the link-set assertion in CLAUDE.md.
lean-toolchain = "0.1.20"

[dev-dependencies]
criterion = { version = "0.8", features = ["html_reports"] }
reqwest = { version = "0.13", default-features = false }
tokio = { version = "1", features = ["process"] }

[lints]
workspace = true
