lean_ctx_server/tools/
ctx_proof.rs

1// SPDX-License-Identifier: Apache-2.0
2use std::path::Path;
3
4use lean_ctx::core::context_ir::{ContextIrV1, write_project_context_ir};
5use lean_ctx::core::context_proof::{ProofOptions, ProofSources, collect_v1, write_project_proof};
6
7pub fn handle_export(
8    project_root: &str,
9    format: Option<&str>,
10    write: bool,
11    filename: Option<&str>,
12    max_evidence: Option<usize>,
13    max_ledger_files: Option<usize>,
14    sources: ProofSources,
15) -> Result<String, String> {
16    let opts = ProofOptions {
17        max_evidence: max_evidence.unwrap_or(50),
18        max_ledger_files: max_ledger_files.unwrap_or(10),
19    };
20    let proof = collect_v1(sources, opts);
21    let ir = ContextIrV1::load();
22
23    let mut out = String::new();
24    let mut written: Option<String> = None;
25    let mut written_ir: Option<String> = None;
26    let mut written_architecture_json: Option<String> = None;
27    let mut written_architecture_html: Option<String> = None;
28    if write {
29        let root = Path::new(project_root);
30        let ts = chrono::Utc::now().format("%Y-%m-%d_%H%M%S").to_string();
31        let default_proof_name = format!("context-proof-v1_{ts}.json");
32        let ir_name = format!("context-ir-v1_{ts}.json");
33        let architecture_json_name = format!("architecture-overview-v1_{ts}.json");
34        let architecture_html_name = format!("architecture-overview-v1_{ts}.html");
35        let proof_name = filename.unwrap_or(default_proof_name.as_str());
36
37        let path = write_project_proof(root, &proof, Some(proof_name))?;
38        written = Some(path.to_string_lossy().to_string());
39
40        let ir_path = write_project_context_ir(root, &ir, Some(&ir_name))?;
41        written_ir = Some(ir_path.to_string_lossy().to_string());
42
43        // Architecture overview proof artifacts (JSON + HTML).
44        // Prefer fresh graph when possible (CI/proof reproducibility).
45        {
46            let status =
47                crate::tools::ctx_impact::handle("status", None, project_root, None, Some("json"));
48            let freshness = serde_json::from_str::<serde_json::Value>(&status)
49                .ok()
50                .and_then(|v| {
51                    v.get("freshness")
52                        .and_then(|f| f.as_str())
53                        .map(std::string::ToString::to_string)
54                })
55                .unwrap_or_else(|| "unknown".to_string());
56            if freshness != "fresh" {
57                let _ = crate::tools::ctx_impact::handle("build", None, project_root, None, None);
58            }
59
60            let arch_json = crate::tools::ctx_architecture::handle(
61                "overview",
62                None,
63                project_root,
64                Some("json"),
65            );
66
67            let proofs_dir = root.join(".lean-ctx").join("proofs");
68            std::fs::create_dir_all(&proofs_dir).map_err(|e| e.to_string())?;
69
70            let json_path = proofs_dir.join(&architecture_json_name);
71            let json_redacted = lean_ctx::core::redaction::redact_text(&arch_json);
72            lean_ctx::config_io::write_atomic(&json_path, &json_redacted)?;
73            written_architecture_json = Some(json_path.to_string_lossy().to_string());
74
75            let html = render_architecture_overview_html(&arch_json);
76            let html_path = proofs_dir.join(&architecture_html_name);
77            let html_redacted = lean_ctx::core::redaction::redact_text(&html);
78            lean_ctx::config_io::write_atomic(&html_path, &html_redacted)?;
79            written_architecture_html = Some(html_path.to_string_lossy().to_string());
80        }
81    }
82
83    match format.unwrap_or("json") {
84        "summary" => {
85            out.push_str("ContextProofV1 exported\n");
86            if let Some(p) = written {
87                out.push_str(&format!("path: {p}\n"));
88            }
89            if let Some(p) = written_ir {
90                out.push_str(&format!("context_ir_path: {p}\n"));
91            }
92            if let Some(p) = written_architecture_json {
93                out.push_str(&format!("architecture_overview_json_path: {p}\n"));
94            }
95            if let Some(p) = written_architecture_html {
96                out.push_str(&format!("architecture_overview_html_path: {p}\n"));
97            }
98            out.push_str(&format!("schema_version: {}\n", proof.schema_version));
99            out.push_str(&format!(
100                "project_root_hash: {}\n",
101                proof.project.project_root_hash.clone().unwrap_or_default()
102            ));
103            out.push_str(&format!("role: {}\n", proof.role.name));
104            out.push_str(&format!("profile: {}\n", proof.profile.name));
105            out.push_str(&format!(
106                "context_ir_schema_version: {}\n",
107                ir.schema_version
108            ));
109            out.push_str(&format!("context_ir_items: {}\n", ir.items.len()));
110        }
111        "both" => {
112            if let Some(p) = &written {
113                out.push_str(&format!("[proof_path: {p}]\n\n"));
114            }
115            if let Some(p) = &written_ir {
116                out.push_str(&format!("[context_ir_path: {p}]\n\n"));
117            }
118            if let Some(p) = &written_architecture_json {
119                out.push_str(&format!("[architecture_overview_json_path: {p}]\n\n"));
120            }
121            if let Some(p) = &written_architecture_html {
122                out.push_str(&format!("[architecture_overview_html_path: {p}]\n\n"));
123            }
124            out.push_str(&serde_json::to_string_pretty(&proof).map_err(|e| e.to_string())?);
125        }
126        _ => {
127            if let Some(p) = &written {
128                out.push_str(&format!("[proof_path: {p}]\n\n"));
129            }
130            if let Some(p) = &written_ir {
131                out.push_str(&format!("[context_ir_path: {p}]\n\n"));
132            }
133            if let Some(p) = &written_architecture_json {
134                out.push_str(&format!("[architecture_overview_json_path: {p}]\n\n"));
135            }
136            if let Some(p) = &written_architecture_html {
137                out.push_str(&format!("[architecture_overview_html_path: {p}]\n\n"));
138            }
139            out.push_str(&serde_json::to_string_pretty(&proof).map_err(|e| e.to_string())?);
140        }
141    }
142
143    Ok(out)
144}
145
146fn escape_html(s: &str) -> String {
147    let mut out = String::with_capacity(s.len());
148    for ch in s.chars() {
149        match ch {
150            '&' => out.push_str("&amp;"),
151            '<' => out.push_str("&lt;"),
152            '>' => out.push_str("&gt;"),
153            '"' => out.push_str("&quot;"),
154            '\'' => out.push_str("&#39;"),
155            _ => out.push(ch),
156        }
157    }
158    out
159}
160
161fn render_architecture_overview_html(json_payload: &str) -> String {
162    let escaped = escape_html(json_payload);
163    format!(
164        r#"<!doctype html>
165<html lang="en">
166<head>
167  <meta charset="utf-8" />
168  <meta name="viewport" content="width=device-width, initial-scale=1" />
169  <title>LeanCTX — Architecture Overview</title>
170  <style>
171    :root {{ color-scheme: light dark; }}
172    body {{ font-family: ui-sans-serif, system-ui, -apple-system, Segoe UI, Roboto, Arial, sans-serif; margin: 24px; }}
173    h1 {{ margin: 0 0 12px 0; }}
174    p  {{ margin: 0 0 18px 0; opacity: 0.8; }}
175    pre {{ padding: 16px; border-radius: 10px; overflow: auto; }}
176  </style>
177</head>
178<body>
179  <h1>Architecture Overview (JSON)</h1>
180  <p>Generated by LeanCTX proof export. Content is redacted-by-default for CI safety.</p>
181  <pre>{escaped}</pre>
182</body>
183</html>"#
184    )
185}
lean_ctx_server/tools/ctx_proof.rs

lean_ctx_server/tools/
ctx_proof.rs
