|
1 | | -# Setting Up Verso-Blueprint |
| 1 | +# PQXDH Documentation Project |
2 | 2 |
|
3 | | -This guide explains how to set up Verso-Blueprint documentation for a Lean 4 project. |
| 3 | +Verso-Blueprint documentation for the PQXDH Lean 4 formalization. |
4 | 4 |
|
5 | | -## Prerequisites |
| 5 | +Built with [verso-blueprint](https://github.com/ejgallego/verso-blueprint) (v4.28.0), |
| 6 | +which extends [Verso](https://github.com/leanprover/verso) with blueprint-style |
| 7 | +rendering for mathematical formalizations. |
6 | 8 |
|
7 | | -- A working Lean 4 project with `lakefile.toml` |
8 | | -- `elan` installed |
| 9 | +## Dependencies |
9 | 10 |
|
10 | | -## Directory Structure |
| 11 | +The docs project (`docs/lakefile.toml`) depends on: |
11 | 12 |
|
12 | | -``` |
13 | | -your-project/ |
14 | | -├── lakefile.toml # Main project lakefile |
15 | | -├── lean-toolchain |
16 | | -├── YourLib/ # Your Lean source files |
17 | | -│ └── *.lean |
18 | | -└── docs/ |
19 | | - ├── lakefile.toml # Docs project lakefile |
20 | | - ├── lean-toolchain |
21 | | - ├── Main.lean |
22 | | - └── YourDocs/ # Documentation source files |
23 | | - └── *.lean |
24 | | -``` |
25 | | - |
26 | | -## Step 1: Set Up the Docs Project |
| 13 | +- **versoBlueprint** — documentation framework (fetched from git) |
| 14 | +- **PQXDH-lean** — the parent Lean library (via `path = ".."`) |
27 | 15 |
|
28 | | -Create `docs/lakefile.toml`: |
| 16 | +Transitive dependencies (`subverso`, Verso core) are resolved automatically |
| 17 | +by Lake from the verso-blueprint manifest. The main project lakefile does |
| 18 | +**not** need to list them. |
29 | 19 |
|
30 | | -```toml |
31 | | -name = "YourDocs" |
32 | | -defaultTargets = ["YourDocs", "docs"] |
| 20 | +## Building |
33 | 21 |
|
34 | | -[[require]] |
35 | | -name = "verso" |
36 | | -git = "https://github.com/leanprover/verso" |
37 | | -rev = "main" # or a specific commit |
38 | | - |
39 | | -[[lean_lib]] |
40 | | -name = "YourDocs" |
41 | | - |
42 | | -[[lean_exe]] |
43 | | -name = "docs" |
44 | | -root = "Main" |
45 | | -``` |
46 | | - |
47 | | -Create `docs/lean-toolchain` with the same Lean version as your main project. |
48 | | - |
49 | | -## Step 2: Build the Docs Project |
| 22 | +From the repository root (not from `docs/`): |
50 | 23 |
|
51 | 24 | ```bash |
52 | | -cd docs |
| 25 | +# Build the Lean library first |
53 | 26 | lake build |
54 | | -``` |
55 | | - |
56 | | -This will fetch Verso and its dependencies, including `subverso`. |
57 | | - |
58 | | -## Step 3: Add Subverso to the Main Project |
59 | | - |
60 | | -Look up the `subverso` commit from `docs/lake-manifest.json`: |
61 | | - |
62 | | -```bash |
63 | | -grep -A2 '"name": "subverso"' docs/lake-manifest.json |
64 | | -``` |
65 | | - |
66 | | -Add `subverso` (not `verso`) to your main project's `lakefile.toml`: |
67 | | - |
68 | | -```toml |
69 | | -[[require]] |
70 | | -name = "subverso" |
71 | | -git = "https://github.com/leanprover/subverso" |
72 | | -rev = "<commit-from-lake-manifest>" |
73 | | -``` |
74 | 27 |
|
75 | | -## Step 4: Build the Main Project |
| 28 | +# Build the documentation executable |
| 29 | +lake -d docs build |
76 | 30 |
|
77 | | -Build with `--keep-toolchain` to prevent the lean-toolchain from updating to subverso's version: |
78 | | - |
79 | | -```bash |
80 | | -lake build --keep-toolchain |
| 31 | +# Generate HTML and serve locally |
| 32 | +./scripts/build-blueprint.sh |
| 33 | +python3 -m http.server 8080 -d _out/blueprint |
81 | 34 | ``` |
82 | 35 |
|
83 | | -## Step 5: Configure Example Project Path |
| 36 | +Then open http://localhost:8080. |
84 | 37 |
|
85 | | -In your documentation Lean files, set the `verso.exampleProject` option to point to your main project: |
| 38 | +## Project structure |
86 | 39 |
|
87 | | -```lean |
88 | | -set_option verso.exampleProject "." |
89 | 40 | ``` |
90 | | - |
91 | | -The path is relative to the workspace root when running `lake -d docs build` from the main project directory. |
92 | | - |
93 | | -## Building Documentation |
94 | | - |
95 | | -From the main project root: |
96 | | - |
97 | | -```bash |
98 | | -lake -d docs build docs |
| 41 | +docs/ |
| 42 | +├── lakefile.toml # Depends on versoBlueprint + parent project |
| 43 | +├── lean-toolchain # Must match parent (v4.28.0) |
| 44 | +├── lake-manifest.json # Pinned dependency versions |
| 45 | +├── Main.lean # Entry point: CSS, JS, blueprint config |
| 46 | +├── PQXDHDocs.lean # Top-level document definition |
| 47 | +└── PQXDHDocs/ |
| 48 | + ├── Contents.lean # Imports all chapters, opens Verso namespaces |
| 49 | + ├── SourceBlock.lean # Custom code block: extracts proof bodies from source |
| 50 | + ├── DocDH.lean # Diffie-Hellman |
| 51 | + ├── DocKDF.lean # Key Derivation Function |
| 52 | + ├── DocAEAD.lean # Authenticated Encryption |
| 53 | + ├── DocKEM.lean # Key Encapsulation Mechanism |
| 54 | + ├── DocX3DH.lean # X3DH Protocol (includes PermDraws + PassiveSecrecy) |
| 55 | + ├── DocPermDraws.lean # perm_draws Tactic (subsection of X3DH) |
| 56 | + ├── DocX3DHPassiveSecrecy.lean # Passive Message Secrecy (subsection of X3DH) |
| 57 | + ├── DocPQXDH.lean # PQXDH Protocol |
| 58 | + └── DocSecurityDefs.lean # Security Definitions and Assumptions |
99 | 59 | ``` |
100 | 60 |
|
101 | | -Or create a build script (e.g., `scripts/build-blueprint.sh`): |
102 | | - |
103 | | -```bash |
104 | | -#!/usr/bin/env bash |
105 | | -set -euo pipefail |
106 | | - |
107 | | -cd "$(dirname "$0")/.." |
108 | | - |
109 | | -out_root="${1:-_out/blueprint}" |
110 | | -mkdir -p "$out_root" |
| 61 | +## How it works |
111 | 62 |
|
112 | | -lake -d docs build docs |
113 | | -"docs/.lake/build/bin/docs" --output "$out_root" |
114 | | - |
115 | | -echo "Output: $(readlink -f "$out_root")" |
116 | | -``` |
| 63 | +- Each `Doc*.lean` file is a Verso document chapter using `#doc (Manual)` blocks. |
| 64 | +- Definitions and theorems use `(lean := "DeclarationName")` to link prose |
| 65 | + to Lean declarations, which Verso resolves at elaboration time. |
| 66 | +- Proof bodies are extracted via `` ```source DeclarationName `` blocks |
| 67 | + (implemented in `SourceBlock.lean`), which read the actual source file |
| 68 | + and display the proof text. |
| 69 | +- Cross-references between chapters use `{uses "tag"}[]` where tags are |
| 70 | + defined by `:::definition` and `:::theorem` blocks. |
117 | 71 |
|
118 | | -## Serving the Documentation |
119 | | - |
120 | | -```bash |
121 | | -python3 -m http.server 8080 -d _out/blueprint |
122 | | -``` |
| 72 | +## Lean version |
123 | 73 |
|
124 | | -Then open http://localhost:8080 in your browser. |
| 74 | +Both the library and docs must use the same Lean toolchain. Currently |
| 75 | +`leanprover/lean4:v4.28.0`, matching Mathlib and verso-blueprint. |
0 commit comments