docs_compiler/lib.rs
1//! docs-compiler: the composition CLI for the estate's docs crates
2//! (docs-core extension program, SPEC.md M3/M4).
3//!
4//! The pipeline is small and honest: scan a markdown document for the
5//! four directive kinds, resolve each one through the crate that owns it
6//! (`include-symbol` through docs-symbols, `witness` through
7//! docs-witness, `lean-check` through an out-of-process `lean` plus
8//! docs-proof, islands natively through docs-core), substitute the
9//! resulting raw HTML, and render the page with docs-core. Any failing
10//! directive fails the build with a typed error naming its source;
11//! nothing degrades to a silent placeholder.
12//!
13//! ```
14//! use docs_compiler::BuildContext;
15//!
16//! // No directives: the document flows through docs-core untouched.
17//! let html = docs_compiler::compile(
18//! "# Title\n\nSome *prose*.\n",
19//! &BuildContext::new("."),
20//! )
21//! .unwrap();
22//! assert!(html.contains("<h1>Title</h1>"));
23//! ```
24//!
25//! # Layer
26//!
27//! L3 - composition. Depends on docs-core (L2) and the capability
28//! crates (L0/L1); spawns `lean` as an external process (REQ-P1).
29
30#![deny(missing_docs)]
31#![forbid(unsafe_code)]
32
33mod directives;
34mod error;
35mod fences;
36
37pub use directives::{resolve, BuildContext};
38pub use error::CompilerError;
39pub use fences::{scan, Directive, DirectiveKind, Scanned};
40
41/// Compile one markdown document into a static HTML page.
42///
43/// Directive fences (`include-symbol`, `witness`, `lean-check`) resolve
44/// through the owning crate and become raw HTML; island fences and all
45/// other markdown render through docs-core (M1 contract unchanged).
46pub fn compile(source: &str, ctx: &BuildContext) -> Result<String, CompilerError> {
47 let scanned = scan(source);
48 let resolved = scanned.substitute(|d| resolve(d, ctx))?;
49 docs_core::render(&resolved, "/_assets").map_err(CompilerError::Render)
50}
51
52/// The crate's version, for callers that report it.
53pub const VERSION: &str = env!("CARGO_PKG_VERSION");