lean_rs_worker_protocol/lib.rs
1//! Wire protocol and shared value types for the `lean-rs` worker process
2//! boundary.
3//!
4//! This crate is the single definition of every shape that flows between a
5//! parent supervisor and a worker child process. It does not link
6//! `libleanshared`, so it can be consumed by alternative transports, fuzz
7//! harnesses, or recorders without pulling the Lean runtime. The parent
8//! supervisor ([`lean-rs-worker-parent`](https://docs.rs/lean-rs-worker-parent))
9//! and the child runtime
10//! ([`lean-rs-worker-child`](https://docs.rs/lean-rs-worker-child)) both
11//! depend on this crate and exchange framed messages defined here.
12//!
13//! ## Module map
14//!
15//! - [`types`] — `serde`-derived value types that appear in request and
16//! response bodies (elaboration options, kernel results, processed-file
17//! projections, capability metadata).
18//! - [`protocol`] — the length-delimited frame codec, [`protocol::Frame`]
19//! envelope, [`protocol::Message`] message variants, and the
20//! [`protocol::Request`] / [`protocol::Response`] / [`protocol::Diagnostic`]
21//! / [`protocol::ProgressTick`] / [`protocol::DataRow`] /
22//! [`protocol::StreamSummary`] / [`protocol::FatalExit`] payload types, plus
23//! [`protocol::write_frame`] and [`protocol::read_frame`].
24//!
25//! ## Stability
26//!
27//! Every public enum, and every public struct that is not externally
28//! constructed, is `#[non_exhaustive]` so additive evolution of the wire
29//! format does not require a semver-major bump. Struct shapes with public
30//! fields that downstream code legitimately constructs (currently [`protocol::DataRow`])
31//! remain exhaustive; adding a field there is a breaking change.
32
33pub mod protocol;
34pub mod types;
35
36#[cfg(feature = "harness")]
37pub mod harness;
38
39/// Version of the `lean-rs-worker-protocol` crate, matching `Cargo.toml`.
40pub const VERSION: &str = env!("CARGO_PKG_VERSION");