[package]
authors.workspace = true
categories = ["api-bindings"]
description = "Opinionated Rust host stack for embedding Lean 4 as a theorem-prover capability: typed sessions, kernel-check evidence handles, bounded MetaM services, progress, batching, and session pooling."
documentation = "https://docs.rs/lean-rs-host"
edition.workspace = true
include = [
  "!shims/**/.lake/**",
  "Cargo.toml",
  "LICENSE-APACHE",
  "LICENSE-MIT",
  "README.md",
  "benches/**/*.rs",
  "build.rs",
  "examples/**/*.rs",
  "shims/**/*.lean",
  "shims/**/c/**/*.c",
  "shims/**/lake-manifest.json",
  "shims/**/lakefile.lean",
  "shims/**/lean-toolchain",
  "src/**/*.rs",
  "tests/**/*.rs",
  "tests/compile_fail/**",
]
keywords = ["bindings", "embedding", "host", "lean", "lean4"]
license.workspace = true
name = "lean-rs-host"
readme = "README.md"
repository.workspace = true
rust-version.workspace = true
version.workspace = true

[dependencies]
lean-rs = { workspace = true }
lean-toolchain = { workspace = true }
serde = { workspace = true }
serde_json = { workspace = true }
tracing = { workspace = true }

[dev-dependencies]
criterion = { workspace = true }
# Examples under `examples/` install a `tracing_subscriber::fmt` sink so
# `RUST_LOG=lean_rs=info cargo run --example <name>` surfaces host spans. The
# workspace dependency stays lean for production builds; this dev override
# enables the example-only formatter/filter layers.
tracing-subscriber = { workspace = true, features = ["env-filter", "fmt"] }
trybuild = "1"

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

[package.metadata.docs.rs]
default-target = "x86_64-unknown-linux-gnu"
targets = []

[lints]
workspace = true

# `tests/compile_fail/*.rs` are driven by trybuild from
# `tests/compile_fail_surface.rs` via string-based `t.compile_fail(...)` calls,
# which cargo-shear cannot see statically.
[package.metadata.cargo-shear]
ignored-paths = ["tests/compile_fail/*.rs"]
