Lean report

SK-62: Blueprint-to-Report Generator

Convert a Lean 4 project blueprint (extracted LaTeX nodes, dependency graphs, JSON metadata) into a publication-grade LaTeX report with natural language narrative, mathematical exposition, and visual dependency maps.

---

Routing

• USE FOR: converting a Lean 4 project blueprint into a publication-grade LaTeX report via the 6-stage INGEST → PLAN → NARRATE → ILLUSTRATE → ASSEMBLE → COMPILE pipeline; ingesting blueprint artifacts (LaTeX nodes, dependency DAG, JSON metadata); generating per-chapter mathematical prose with \leanref cross-references; producing TikZ dependency figures; running latexmk to PDF.
• DO NOT USE FOR: generating the blueprint itself (delegate to @lean-blueprint); writing one chapter without the pipeline (delegate to @lean-doc-improvement); reviewing a finished report (delegate to @lean-review-council); spec lifecycle (delegate to @lean-specification).
• TRIGGERS: blueprint to report, generate report, latex pdf, project-report.tex, narrate chapter, dependency figure, blueprint compile.

Workflow

1. Verify prerequisites (Part 12.1 below — blueprint artifacts exist, LaTeX toolchain present).
2. First-time: run Part 12.2 (INGEST → PLAN → NARRATE → ILLUSTRATE → ASSEMBLE → COMPILE). Each stage's contract is in the handbook (Parts 3–8).
3. Incremental: run Part 12.3 — re-blueprint, re-ingest, diff, narrate only changed chapters, recompile.
4. On compilation error consult Part 13 (Troubleshooting) below; on output-artifact question consult Part 14 below.
5. Handoff to @lean-doc-feedback once the PDF lands so the doc-sync skill can record the new artifact in the repository's tracking matrix.

Recovery & STOP

• STOP if \cref references emit "??" after two latexmk passes — the blueprint is out of sync; re-run INGEST per Part 12.3.
• STOP if narration drifts from Lean source (Part 13 final row) — the source changed after narration; re-run NARRATE for affected chapters only.
• STOP if the figures stage produces empty TikZ outputs — dot2tex is optional but required for dependency graphs; install or fall back to module-map-only figures.

Handoffs

• Predecessors: agent:gateway (top-level invocation), skill:lean-blueprint (produces the blueprint artifacts this skill consumes), skill:lean-doc-requirements (chapter-scope decisions).
• Successors: skill:lean-doc-feedback (record the PDF artifact + cross-references), skill:lean-doc-improvement (per-chapter post-narration edits), skill:lean-review-council (review the report for project-level coherence), skill:lean-enforcement (CI gate that confirms PDF builds on a clean checkout).

---

Detailed reference

Full pipeline content (Parts 1–11) lives in references/lean-report-handbook.md. Load that file when authoring or debugging stage internals; the SKILL.md only carries the dispatch contract and the high-frequency operational sections (Parts 12–14 kept inline below).

Section	Topic	Covers
Part 1	Inputs and Outputs	What this skill consumes / produces
Part 2	Pipeline Architecture	Six-stage DAG overview
Part 3	Stage 1 — INGEST	Blueprint artifact extraction
Part 4	Stage 2 — PLAN	Chapter outline + narrative arc derivation
Part 5	Stage 3 — NARRATE	Per-chapter prose generation rules
Part 5B	Lean 4.28 Features for Report Generation	Pin-relative Lean+Mathlib features
Part 6	Stage 4 — ILLUSTRATE	TikZ figure generation
Part 7	Stage 5 — ASSEMBLE	Master-document merging
Part 8	Stage 6 — COMPILE	latexmk pipeline + diagnostics
Part 9	Audit Integration	Tracking-matrix hooks
Part 10	Project-specific Configuration	Per-project tunables
Part 11	Integration with Gateway (SK-07)	Cross-skill dispatch

Part 12 — Execution Checklist

12.1 Prerequisites

# 1. Verify blueprint exists
ls .lake/build/blueprint/library/*.tex   # extracted nodes
ls blueprint/web/index.html              # web build exists

# 2. Verify LaTeX toolchain
which latexmk pdflatex biber
kpsewhich tikz.sty pgfplots.sty cleveref.sty thmtools.sty

# 3. Verify optional tools
which dot2tex   # for dependency graph conversion (optional)

12.2 First-Time Generation

# 1. Create report directory structure
mkdir -p report/{chapters,front,back,figures,macros,build}

# 2. Run INGEST stage
python3 scripts/blueprint_to_report.py ingest \
  --blueprint-dir .lake/build/blueprint \
  --coverage docs/tracking/coverage_matrix.md \
  --output report/report_context.json

# 3. Run PLAN stage
python3 scripts/blueprint_to_report.py plan \
  --context report/report_context.json \
  --output report/report_plan.json

# 4. Run NARRATE stage (agent-driven, one chapter at a time)
# Each chapter: read plan → read module → generate prose
# See §5 for generation rules

# 5. Run ILLUSTRATE stage
python3 scripts/blueprint_to_report.py illustrate \
  --context report/report_context.json \
  --output-dir report/figures/

# 6. Run ASSEMBLE stage
# Merge all chapters into master document (see §7.1)

# 7. Run COMPILE stage
cd report && latexmk -pdf project-report.tex

12.3 Incremental Updates

After new theorems are proven:

# 1. Re-run blueprint (SK-61):
lake build :blueprint && leanblueprint all

# 2. Re-ingest:
python3 scripts/blueprint_to_report.py ingest --update

# 3. Identify changed chapters:
python3 scripts/blueprint_to_report.py diff \
  --old report/report_context.json \
  --new report/report_context_updated.json

# 4. Re-narrate affected chapters only

# 5. Recompile:
cd report && latexmk -pdf project-report.tex

---

Part 13 — Troubleshooting

Problem	Cause	Fix
No blueprint artifacts found	SK-61 not run	Run generate blueprint first
nodes.json missing	:blueprintJson not built	Run lake build :blueprintJson
LaTeX won't compile	Missing package	Install full TeX Live: tlmgr install <pkg>
Undefined \cref	cleveref not loaded	Add \usepackage{cleveref} after hyperref
Cross-references show "??"	Need 2nd pass	Run latexmk (auto-handles multi-pass)
Theorem count mismatch	Blueprint outdated	Rebuild blueprint, re-ingest
Margin notes overflow	Too many \leanref	Reduce to key theorems only
Figure won't render	Missing TikZ library	Add \usetikzlibrary{...}
Bibliography empty	.bib not found	Check \addbibresource path
PDF too large	Embedded high-res figures	Use \includegraphics[draft] for draft builds
Narration inconsistent with Lean	Source changed after narration	Re-run INGEST + NARRATE for affected chapters
Scaling notation unclear	Missing §scaling-convention	Ensure Ch 1 defines the $\times 100$ convention

---

Part 14 — Output Artifacts Summary

The complete report generation pipeline produces:

Artifact	Location	Purpose
Report context	report/report_context.json	Serialized ingestion data
Report plan	report/report_plan.json	Chapter outlines + narrative arcs
Chapter files	report/chapters/ch_*.tex	Per-module natural language chapters
Front matter	report/front/	Abstract, introduction
Back matter	report/back/	Appendices, bibliography
Figures	report/figures/	TikZ source + PDF figures
Macros	report/macros/common.tex	Shared LaTeX commands
Master document	report/project-report.tex	Top-level LaTeX source
Compiled PDF	report/build/project-report.pdf	Final output
Build log	report/build/project-report.log	Compilation diagnostics

---

See also

• ../../references/lean-report-handbook.md — Full pipeline encyclopaedia (extracted from this skill)
• ../lean-blueprint/SKILL.md — Produces the blueprint artifacts this skill consumes
• ../lean-doc-feedback/SKILL.md — Records the resulting PDF in the repository's doc-sync matrix
• ../lean-review-council/SKILL.md — Reviews the report for project-level coherence