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).

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

Part 14 — Output Artifacts Summary

The complete report generation pipeline produces:

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