[package]
authors.workspace = true
categories = ["api-bindings", "external-ffi-bindings"]
description = "Safe Rust bindings for Lean 4 interop: runtime initialization, object handles, typed ABI conversions, module loading, exported function calls, semantic handles, and callback handles."
documentation = "https://docs.rs/lean-rs"
edition.workspace = true
include = [
  "!shims/**/.lake/**",
  "Cargo.toml",
  "LICENSE-APACHE",
  "LICENSE-MIT",
  "README.md",
  "benches/**/*.rs",
  "build.rs",
  "examples/**/*.rs",
  "shims/**/c/**/*.c",
  "shims/**/*.lean",
  "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"
readme = "README.md"
repository.workspace = true
rust-version.workspace = true
version.workspace = true

[dependencies]
lean-toolchain = { workspace = true }
lean-rs-sys = { workspace = true }
libloading = "0.8"
# Symbol-table walk in `module::library` distinguishes Lean nullary-constant
# globals (compiled by Lake as persistent `lean_object*` data-section
# symbols) from callable functions. One-shot at `LeanLibrary::open` so the
# function-vs-global distinction stays invisible to callers of
# `LeanModule::exported`.
object = { version = "0.36", default-features = false, features = ["read", "std"] }
# Structured spans + events around runtime init, module load + dispatch,
# host session calls, and bulk/pool paths. No subscriber is installed by
# the crate; downstream consumers attach their own (or `DiagnosticCapture`
# for in-process tests). Cost is one atomic load per span entry when no
# subscriber is attached.
tracing = { workspace = true }
# `tracing-subscriber` powers `DiagnosticCapture` (always present, no
# feature gate). Only the `registry` plumbing is needed; the `fmt`
# stack is intentionally absent so downstream applications choose their
# own formatter.
tracing-subscriber = { workspace = true }

[features]
# Opens a narrow set of `pub(crate)` ABI decoders as `pub fn` entry
# points so the in-tree `fuzz/` crate (cargo-fuzz, nightly-only) can
# drive them with `lean-rs-sys`-constructed Lean-shaped inputs.
#
# This feature is **not** semver-stable: it is intentionally invisible
# in published documentation and is gated solely for fuzzing
# infrastructure. The exposed surface is the `lean_rs::abi::fuzz_entry`
# module; it is not re-exported at the crate root.
fuzzing = []

[dev-dependencies]
# Heap profiler for `examples/alloc_probe.rs`. Installs `dhat::Alloc` as the
# *Rust* global allocator; Lean's internal mimalloc (statically linked into
# `libleanrt.a`) is a separate allocator and unaffected. Dev-only — never
# pulled into the published library build.
dhat = "0.3"
# Criterion drives the steady-state hot-path and session-path baselines
# under `benches/`. Cold paths (runtime init, library open, module init)
# are once-per-process and live in `examples/cold_probe.rs` instead —
# see `docs/performance/baseline.md` for the rationale.
criterion = { workspace = true }
# Examples under `examples/` install a `tracing_subscriber::fmt`
# sink so `RUST_LOG=lean_rs=info cargo run --example <name>` surfaces
# the spans the crate emits. The workspace `tracing-subscriber` carries
# only `registry` + `std` (enough for `DiagnosticCapture`); the dev
# override layers `fmt` + `env-filter` on top so production builds don't
# pull either. Cargo unions the feature sets across the two declarations.
tracing-subscriber = { workspace = true, features = ["env-filter", "fmt"] }

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

[[example]]
name = "cold_probe"

[[example]]
name = "alloc_probe"

[lints]
workspace = true

[lib]
doctest = false
