Overview
# Runway Module
Presentation layer for Lean mathematical blueprints. Consumes artifacts from Dress and generates an interactive multi-page HTML site.
## Architecture
```
Dress (highlighting, hovers, graphs) --> Runway (HTML generation) --> Interactive website
```
Runway is the final stage of the Side-by-Side Blueprint pipeline. It does not perform syntax highlighting, graph layout, or artifact capture -- those are handled by upstream dependencies (SubVerso, Dress). Runway reads precomputed artifacts and renders them into HTML pages.
## Module Map
| Module | File | Purpose |
|--------|------|---------|
| `Config` | `Config.lean` | Site configuration (`Config`, `ValidationConfig`) parsed from `runway.json` |
| `Graph` | `Graph.lean` | Rendering-focused graph types: `NodeStatus`, `Node`, `Edge`, `Graph` |
| `Site` | `Site.lean` | Site structure: `NodeInfo`, `ChapterInfo`, `SectionInfo`, `BlueprintSite`, `SiteBuilder` |
| `Render` | `Render.lean` | `RenderM` monad, dashboard rendering, node rendering, progress display |
| `Theme` | `Theme.lean` | Page templates, sidebar generation, placeholder replacement, `generateMultiPageSite` |
| `Templates` | `Templates.lean` | Reusable HTML template components |
| `DepGraph` | `DepGraph.lean` | Dependency graph page: SVG embedding, modals, toolbar, legend |
| `Paper` | `Paper.lean` | Paper HTML generation, `PaperMetadata` extraction, verification badges |
| `Pdf` | `Pdf.lean` | PDF compilation, compiler auto-detection, aux file cleanup |
| `Faq` | `Faq.lean` | FAQ page generation from collected README.md files |
| `Macros` | `Macros.lean` | MathJax macro extraction from LaTeX preamble |
| `DocGen4` | `DocGen4.lean` | doc-gen4 URL generation for API documentation links |
| `Validate` | `Validate.lean` | Declaration validation checks |
| `Traverse` | `Traverse.lean` | `TraverseM` monad for loading and accessing Dress artifacts |
| `Genre` | `Genre.lean` | Verso `Blueprint` genre definition |
| `Doc` | `Doc.lean` | Blueprint-specific Verso document extensions |
| `VersoPaper` | `VersoPaper.lean` | VersoPaper genre integration |
| `Assets` | `Assets.lean` | Asset copying utilities |
| `AvailableDocuments` | `AvailableDocuments.lean` | Document availability tracking for sidebar links |
| `Latex/` | directory | LaTeX lexer, parser, AST, and conversion (see `Latex/README.md`) |
| `Html/` | directory | HTML rendering from LaTeX AST (see `Html/README.md`) |
| `Dress/` | directory | Dress artifact loading and decoding (see `Dress/README.md`) |
## Generated Pages
| Page | File | Generator |
|------|------|-----------|
| Dashboard | `index.html` | `Render.renderDashboard` -- 2x2 grid: stats, key theorems, messages, project notes |
| Chapter pages | `chapter-*.html` | `Theme.generateMultiPageSite` -- LaTeX-driven chapter/section structure with side-by-side displays |
| Dependency graph | `dep_graph.html` | `DepGraph.fullPageGraph` -- pan/zoom SVG with node modals |
| Paper | `paper_tex.html` | `Paper.convertDocument` -- ar5iv-style academic paper with verification badges |
| PDF viewer | `pdf_tex.html` | `Pdf` -- embedded PDF viewer page |
| FAQ | `faq.html` | `Faq.generateFaqPage` -- collected README.md documentation |
## Key Entry Points
**`generateMultiPageSite`** in `Theme.lean` is the main site generation orchestrator. It:
1. Builds node and module lookup maps
2. Renders chapter pages with placeholder replacement
3. Generates dashboard, dependency graph, and FAQ pages
4. Copies CSS/JS assets from `assetsDir`
**`buildSiteFromArtifacts`** in `Main.lean` constructs the `BlueprintSite` from Dress artifacts, loading the manifest, graph files, and per-declaration HTML/hover data.
## Data Flow
```
runway.json --> Config
blueprint.tex --> Latex/Parser --> Array ChapterInfo
manifest.json --> StatusCounts, CheckResults, EnhancedManifest
dep-graph.svg --> SVG string (embedded in dep_graph.html)
dep-graph.json --> Graph data (for modals)
decl.tex --> TheoremMetadata (base64 fields decoded by Dress/Load)
|
v
BlueprintSite
|
+-----------+-----------+
| | |
v v v
index.html chapter-*.html dep_graph.html paper_tex.html faq.html
```
## Key Types
- **`Config`** (`Config.lean`): Site configuration parsed from `runway.json`. Required fields: `projectName`, `assetsDir`.
- **`NodeInfo`** (`Site.lean`): Everything needed to render a node -- label, status, statement/proof HTML, signature HTML, hover data, display number, metadata fields.
- **`ChapterInfo`** / **`SectionInfo`** (`Site.lean`): Chapter and section structure extracted from `blueprint.tex`.
- **`BlueprintSite`** (`Site.lean`): The complete site -- config, nodes, graph, chapters, precomputed stats, check results.
- **`SiteBuilder`** (`Site.lean`): Builder pattern for constructing a `BlueprintSite` incrementally.
- **`NodeStatus`** (`Graph.lean`): Six-status enum: `notReady`, `ready`, `sorry`, `proven`, `fullyProven`, `mathlibReady`.
- **`StatusCounts`** (`Site.lean`): Node counts by status, with backwards-compatible JSON parsing for legacy `stated`/`inMathlib` values.
## Theme System
The theme system in `Theme.lean` uses template type aliases:
- `Template`: `Config -> String -> Html -> Html` (page wrapper)
- `NodeTemplate`: renders individual node content
- `IndexTemplate`: renders chapter index/TOC
`primaryTemplateWithSidebar` is the main page wrapper. `isBlueprintPage` determines whether the sidebar chapter panel is shown (returns `false` for dashboard, `true` for chapter pages).
## Placeholder System
Two-pass placeholder replacement in `Theme.lean`:
1. **`buildNodeLookup`**: Creates a `label -> NodeInfo` map
2. **`buildModuleLookup`**: Creates a `moduleName -> Array NodeInfo` map
3. **`replacePlaceholders`**: Finds `\inputleanmodule{}` and `\inputleannode{}` placeholders in rendered HTML and replaces them with rendered node content
## FAQ Page and README Collection
The FAQ page (`Faq.lean`) algorithmically collects README.md files from toolchain repositories and user-defined documentation directories. It walks known repo paths (`Dress/Dress/`, `Runway/Runway/`, `dress-blueprint-action/`, `LeanArchitect/Architect/`) and their immediate subdirectories, collecting any README.md files it finds. These are rendered as collapsible sections grouped by repository.