[package]
name = "telltale-lean-bridge"
version = "3.0.0"
authors = ["Sam Hart <sam@hxrts.com>"]
edition = "2021"
description = "Lean verification bridge for Telltale session types"
readme = "../../README.md"
repository = "https://github.com/hxrts/telltale"
license = "MIT"
keywords = ["session-types", "verification", "lean", "multiparty"]
categories = ["development-tools", "concurrency"]

[[bin]]
name = "lean-bridge"
path = "src/bin/main.rs"
required-features = ["cli"]

[[bin]]
name = "lean-bridge-exporter"
path = "src/bin/exporter.rs"
required-features = ["exporter"]

[[bin]]
name = "golden"
path = "src/bin/golden.rs"
required-features = ["golden"]

[features]
default = ["runner"]
cli = ["clap"]
runner = ["telltale-theory"]  # Enable LeanRunner and EquivalenceChecker
exporter = ["telltale-choreography", "anyhow", "bpaf"]  # Enable choreography exporter
golden = ["clap", "anyhow", "runner"]  # Enable golden file management CLI

[dependencies]
telltale-types = { path = "../types", version = "3.0.0" }
telltale-theory = { path = "../theory", version = "3.0.0", optional = true }
serde = { workspace = true, features = ["derive"] }
serde_json = { workspace = true }
thiserror = { workspace = true }
clap = { version = "4.4", features = ["derive"], optional = true }
bpaf = { version = "0.9", features = ["derive"], optional = true }
tempfile = { workspace = true }
anyhow = { workspace = true, optional = true }
telltale-choreography = { path = "../choreography", version = "3.0.0", optional = true }
cfg-if = { workspace = true }

[dev-dependencies]
proptest = { workspace = true }
telltale-theory = { path = "../theory", version = "3.0.0" }
telltale-choreography = { path = "../choreography", version = "3.0.0" }
telltale-vm = { path = "../vm", version = "3.0.0", features = ["multi-thread"] }
tempfile = { workspace = true }
serde_json = { workspace = true }
tracing = { workspace = true }
