Quickstart
# Getting Started with Side-by-Side Blueprint
Side-by-Side Blueprint (SBS) generates interactive documentation websites from Lean 4 formalization projects. It displays formal Lean proofs alongside LaTeX theorem statements, letting mathematicians verify that their formal code matches their intent.
## What You Get
- A **dashboard** summarizing project progress
- **Chapter pages** showing LaTeX statements side-by-side with Lean code
- An **interactive dependency graph** visualizing how theorems connect
- An optional **academic paper** with verification badges linking back to proofs
See live examples: [SBS-Test](https://e-vergo.github.io/SBS-Test/), [General Crystallographic Restriction](https://e-vergo.github.io/General_Crystallographic_Restriction/), [PrimeNumberTheoremAnd](https://e-vergo.github.io/PrimeNumberTheoremAnd/).
## Prerequisites
- **Lean 4** (v4.27.0 or later) with Lake build system
- A Lean project with mathematical declarations you want to document
## Step 1: Add SBS to Your Project
Add the `Dress` package to your `lakefile.toml`. Dress bundles the full SBS toolchain including the `@[blueprint]` attribute:
```toml
[[require]]
name = "Dress"
git = "https://github.com/e-vergo/Dress"
rev = "main"
```
## Step 2: Annotate Your Declarations
Import `Dress` in your Lean files and mark declarations with `@[blueprint]`:
```lean
import Dress
@[blueprint "thm:main"]
theorem mainTheorem : 2 + 2 = 4 := rfl
@[blueprint "lem:helper" (keyDeclaration := true, message := "Key lemma")]
lemma helperLemma : P := by sorry
```
Each declaration gets a unique label (like `"thm:main"`) that links it to the LaTeX document.
## Step 3: Write Your LaTeX Blueprint
Create a `blueprint/src/blueprint.tex` file describing your project's mathematical structure:
```latex
\documentclass{article}
\begin{document}
\chapter{Main Results}
\section{Core Theorem}
\begin{theorem}[Main Theorem]\label{thm:main}
We have $2 + 2 = 4$.
\end{theorem}
\begin{lemma}[Helper Lemma]\label{lem:helper}
Statement of the helper lemma.
\end{lemma}
\uses{thm:main}
\end{document}
```
Labels in the LaTeX document must match the labels in your `@[blueprint]` attributes.
## Step 4: Create Configuration
Create a `runway.json` in your project root:
```json
{
"title": "My Blueprint",
"projectName": "MyProject",
"blueprintTexPath": "blueprint/src/blueprint.tex",
"assetsDir": "../dress-blueprint-action/assets",
"githubUrl": "https://github.com/user/MyProject",
"baseUrl": "/"
}
```
The `projectName` must match the package name in your `lakefile.toml`.
## Step 5: Build and View
### Using GitHub Actions (Recommended)
Add this workflow to `.github/workflows/blueprint.yml`:
```yaml
name: Blueprint
on:
workflow_dispatch:
permissions:
contents: read
pages: write
id-token: write
jobs:
build:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: e-vergo/dress-blueprint-action@main
deploy:
needs: build
if: github.ref == 'refs/heads/main'
runs-on: ubuntu-latest
environment:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
steps:
- uses: actions/deploy-pages@v4
id: deployment
```
Trigger the workflow from the Actions tab. Your site deploys to GitHub Pages.
### Building Locally
If you have the toolchain repos cloned locally, build with:
```bash
BLUEPRINT_DRESS=1 lake build # Build project with artifact generation
lake build :blueprint # Generate blueprint facets
lake exe extract_blueprint graph # Generate dependency graph
lake exe runway build runway.json # Generate the site
```
The generated site appears in `.lake/build/runway/`. Open `index.html` in a browser.
## Optional: Add a Paper
To generate an academic paper with verification badges, add a `paper.tex` and set `"paperTexPath": "blueprint/src/paper.tex"` in `runway.json`. Use `\paperstatement{thm:main}` in your paper to embed theorem statements with links to the blueprint.
## Next Steps
- Read [Navigating a Blueprint Site](user-guide.md) to understand the generated output
- Read [Status Colors Explained](status-colors.md) to understand the progress indicators
- See the [dress-blueprint-action README](https://github.com/e-vergo/dress-blueprint-action) for advanced CI configuration