Dress

# Dress Module Loads and decodes artifacts produced by the Dress build pipeline. These artifacts contain syntax-highlighted Lean code, hover tooltip data, and project metadata that Runway renders into HTML pages. ## Pipeline Position ``` Dress (upstream) --> .lake/build/dressed/ --> Dress/Load.lean --> NodeInfo, BlueprintSite ``` Dress writes artifacts during Lean elaboration (when `BLUEPRINT_DRESS=1` is set). Runway's Dress module reads these artifacts at site generation time. Runway never invokes Dress directly -- it only reads the files Dress produced. ## File ### `Load.lean` The single file in this module. Handles three concerns: base64 decoding, manifest parsing, and artifact loading. ### Base64 Decoding Several fields in the LaTeX artifacts are base64-encoded by Dress to safely embed HTML and JSON inside LaTeX commands. `Load.lean` provides: - `decodeBase64 (s : String) : Option ByteArray` -- Decodes a base64 string to bytes - `decodeBase64String (s : String) : Option String` -- Decodes to a UTF-8 string - `processMetadata (md : TheoremMetadata) : TheoremMetadata` -- Decodes all base64 fields in theorem metadata: `signatureHtml`, `proofHtml`, `hoverData`, `above`, `below` - `processBlock` / `processDocument` -- Recursively walks the AST and decodes all embedded Dress artifacts ### Manifest Parsing The `manifest.json` file is the primary data exchange format between Dress and Runway. It contains precomputed statistics, dashboard metadata, graph validation results, and node URL mappings. **`EnhancedManifest`** -- The main manifest type: - `stats`: Raw JSON for status counts (parsed separately as `StatusCounts` in `Site.lean`) - `keyDeclarations`: Node IDs marked with `keyDeclaration := true` - `messages`: Pairs of `(nodeId, message)` from `message := "..."` annotations - `priorityItems`: Nodes marked with `priorityItem := true` - `blockedItems`: Pairs of `(nodeId, reason)` from `blocked := "..."` annotations - `potentialIssues`: Pairs of `(nodeId, issue)` from `potentialIssue := "..."` annotations - `technicalDebt`: Pairs of `(nodeId, debt)` from `technicalDebt := "..."` annotations - `miscItems`: Pairs of `(nodeId, note)` from `misc := "..."` annotations - `nodeUrls`: HashMap mapping node IDs to their anchor URLs - `checks`: Graph validation results (`CheckResults`) **`loadEnhancedManifest (dressedDir : System.FilePath) : IO EnhancedManifest`** -- Reads and parses `manifest.json` from the Dress build directory. Returns an empty manifest if the file is missing or malformed. **Accessor methods** on `EnhancedManifest`: - `isKeyDeclaration`, `getMessage`, `getPriorityItem`, `getBlocked`, `getPotentialIssue`, `getTechnicalDebt`, `getMisc` -- Look up metadata by node ID ### Graph Validation Types **`CheckResults`** -- Results of Dress's graph validation: - `isConnected`: Whether the dependency graph is a single connected component - `numComponents` / `componentSizes`: Connected component analysis - `cycles`: Detected cycles (each as an array of node IDs) - `kernelVerified`: Whether all declarations pass kernel type-checking - `soundnessResults`: Array of `SoundnessResult` (name, passed, detail, url) - `coverage`: Blueprint coverage statistics (`CoverageResult`) **`CoverageResult`** -- Blueprint annotation coverage: - `totalDeclarations`: Eligible project-local declarations - `coveredDeclarations`: Declarations with `@[blueprint]` annotations - `coveragePercent`: Coverage as 0.0-100.0 - `uncovered`: Array of `UncoveredDecl` (name, moduleName, kind) ### Artifact Loading **`DeclArtifact`** -- Per-declaration artifact data: - `name`: Lean declaration name - `label`: Cross-reference label - `signatureHtml`, `proofHtml`, `hoverData`: Pre-rendered content - `position`: Source file location - `leanOk`, `mathLibOk`: Status flags **`loadArtifactJson`** -- Loads a module's artifact JSON from `.lake/build/dressed/{Module}.json`. **`extractArtifacts`** -- Extracts `DeclArtifact` records from loaded JSON. ## Artifact Directory Structure Dress writes artifacts to `.lake/build/dressed/`: ``` .lake/build/dressed/ {Module}/ {label}/ decl.tex # LaTeX with base64-encoded Dress fields decl.html # Lean code with syntax highlighting decl.json # Metadata (status, module, uses, etc.) decl.hovers.json # Hover tooltip data (Tippy.js format) dep-graph.json # Dependency graph nodes and edges dep-graph.svg # Pre-rendered SVG with Sugiyama layout manifest.json # Stats, validation results, dashboard metadata ``` ## Connection to Downstream Modules - **`Site.lean`** uses `CheckResults` in the `BlueprintSite` structure and parses `StatusCounts` from the manifest's `stats` field - **`Render.lean`** displays check results on the dashboard via `renderChecks` - **`DepGraph.lean`** loads the SVG and JSON graph files for the dependency graph page - **`Theme.lean`** uses manifest data to populate node metadata (key declarations, messages, blocked status, etc.)