docs_compiler/
directives.rs

1//! Directive resolution and static HTML emission.
2
3use std::path::{Path, PathBuf};
4
5use docs_proof::CertificateBuilder;
6use docs_symbols::Language;
7use docs_witness::{check, run, Assertions, WitnessConfig};
8
9use crate::error::CompilerError;
10use crate::fences::{Directive, DirectiveKind};
11
12/// The build context: directive file paths resolve against this root.
13#[derive(Debug, Clone)]
14pub struct BuildContext {
15    /// Repository/docs root (fence paths are relative to it).
16    pub root: PathBuf,
17}
18
19impl BuildContext {
20    /// A context rooted at `root`.
21    pub fn new(root: impl Into<PathBuf>) -> Self {
22        Self { root: root.into() }
23    }
24
25    fn read(&self, path: &str) -> Result<Vec<u8>, CompilerError> {
26        let full = self.root.join(path);
27        std::fs::read(&full).map_err(|source| CompilerError::Io {
28            path: path.to_string(),
29            source,
30        })
31    }
32
33    fn read_text(&self, path: &str) -> Result<String, CompilerError> {
34        let bytes = self.read(path)?;
35        String::from_utf8(bytes).map_err(|_| CompilerError::Io {
36            path: path.to_string(),
37            source: std::io::Error::new(std::io::ErrorKind::InvalidData, "file is not valid UTF-8"),
38        })
39    }
40}
41
42/// Resolve one directive fence to a raw HTML block.
43pub fn resolve(d: &Directive, ctx: &BuildContext) -> Result<String, CompilerError> {
44    match d.kind {
45        DirectiveKind::IncludeSymbol => include_symbol(d, ctx),
46        DirectiveKind::Witness => witness(d, ctx),
47        DirectiveKind::LeanCheck => lean_check(d, ctx),
48    }
49}
50
51/// `include-symbol file=... symbol=... [lang=rust]`
52fn include_symbol(d: &Directive, ctx: &BuildContext) -> Result<String, CompilerError> {
53    let file = d.require("file")?;
54    let symbol = d.require("symbol")?;
55    let lang = match d.attr("lang").unwrap_or("rust") {
56        "rust" => Language::Rust,
57        other => {
58            return Err(CompilerError::Attribute {
59                directive: "include-symbol",
60                reason: format!("unsupported language `{other}` (0.1 ships rust)"),
61            })
62        }
63    };
64    let source = ctx.read_text(file)?;
65    let span = docs_symbols::extract(&source, lang, symbol).map_err(CompilerError::Symbol)?;
66    Ok(format!(
67        "<figure class=\"docs-symbol\" data-anchor=\"{anchor}\"><figcaption>{file} :: {symbol}</figcaption><pre><code>{code}</code></pre></figure>",
68        anchor = span.anchor_id,
69        code = html_escape(&span.code),
70    ))
71}
72
73/// `witness wasm=... [fuel=...] [stdout_capacity=...] [assert_exit=...]
74/// [assert_stdout="..."]`
75fn witness(d: &Directive, ctx: &BuildContext) -> Result<String, CompilerError> {
76    let wasm_path = d.require("wasm")?;
77    let wasm = ctx.read(wasm_path)?;
78    let cfg = WitnessConfig {
79        fuel: d
80            .attr("fuel")
81            .and_then(|v| v.parse().ok())
82            .unwrap_or(docs_witness::DEFAULT_FUEL),
83        stdout_capacity: d
84            .attr("stdout_capacity")
85            .and_then(|v| v.parse().ok())
86            .unwrap_or(docs_witness::DEFAULT_STDOUT_CAPACITY),
87    };
88    let w = run(&wasm, &cfg).map_err(CompilerError::Witness)?;
89    let assertions = Assertions {
90        exit: d.attr("assert_exit").and_then(|v| v.parse().ok()),
91        stdout: d.attr("assert_stdout").map(str::to_string),
92    };
93    check(&w, &assertions).map_err(CompilerError::WitnessAssert)?;
94
95    Ok(format!(
96        "<div class=\"docs-witness\" data-exit=\"{exit}\" data-fuel=\"{fuel}\"><pre class=\"docs-witness-stdout\">{stdout}</pre></div>",
97        exit = w.exit,
98        fuel = w.fuel_consumed,
99        stdout = html_escape(&String::from_utf8_lossy(&w.stdout)),
100    ))
101}
102
103/// `lean-check file=... theorem=... toolchain=...`
104///
105/// Invokes `lean` out-of-process (REQ-P1: never linked). The kernel
106/// verdict is real or the build fails: nonzero exit, kernel errors, or
107/// `declaration uses 'sorry'` all fail; a passing run becomes a
108/// certificate whose self-verification guards against a stale record.
109fn lean_check(d: &Directive, ctx: &BuildContext) -> Result<String, CompilerError> {
110    let file = d.require("file")?;
111    let theorem = d.require("theorem")?.to_string();
112    let toolchain = d.require("toolchain")?.to_string();
113    let source = ctx.read_text(file)?;
114    let full_path = ctx.root.join(file);
115
116    let output = std::process::Command::new("lean")
117        .arg(&full_path)
118        .current_dir(ctx.root.join(file).parent().unwrap_or(Path::new(".")))
119        .output()
120        .map_err(|source| CompilerError::Lean {
121            theorem: theorem.clone(),
122            detail: format!("cannot spawn `lean` (is it on PATH?): {source}"),
123        })?;
124    let stderr = String::from_utf8_lossy(&output.stderr);
125    let stdout = String::from_utf8_lossy(&output.stdout);
126    // Lean 4.35 routes diagnostics to stdout and words the warning with
127    // backticks: `declaration uses `sorry``. Scan the combined output.
128    let diagnostics = format!("{stderr}{stdout}");
129    if !output.status.success() {
130        return Err(CompilerError::Lean {
131            theorem: theorem.clone(),
132            detail: format!(
133                "lean exited with {}: {}",
134                output.status,
135                first_lines(&diagnostics)
136            ),
137        });
138    }
139    if diagnostics.contains("declaration uses `sorry`") {
140        return Err(CompilerError::Lean {
141            theorem: theorem.clone(),
142            detail: "declaration uses `sorry` - not a kernel-verified proof".into(),
143        });
144    }
145
146    let certificate = CertificateBuilder::new(&theorem, &source, &toolchain).verified();
147    docs_proof::verify(&certificate, &source, &toolchain).map_err(|e| CompilerError::Lean {
148        theorem: theorem.clone(),
149        detail: e.to_string(),
150    })?;
151
152    Ok(format!(
153        "<span class=\"docs-proof\" data-theorem=\"{theorem}\">verified</span><script type=\"application/json\" data-proof-certificate>{badge}</script>",
154        badge = html_escape(&certificate.badge_json()),
155    ))
156}
157
158/// First few lines of a diagnostics blob, for error messages.
159fn first_lines(text: &str) -> String {
160    let collected: Vec<&str> = text
161        .lines()
162        .filter(|l| !l.trim().is_empty())
163        .take(3)
164        .collect();
165    collected.join(" | ")
166}
167
168/// Minimal HTML text escaping: `&`, `<`, `>`; blank-line guard included
169/// (an empty line inside a raw-HTML block would end the block in
170/// pulldown-cmark, so interior double newlines gain a zero-width entity
171/// line).
172fn html_escape(text: &str) -> String {
173    let escaped = text
174        .replace('&', "&amp;")
175        .replace('<', "&lt;")
176        .replace('>', "&gt;");
177    escaped.replace("\n\n", "\n&#10;\n")
178}
docs_compiler/directives.rs

docs_compiler/
directives.rs
