Add exposition website

.github/workflows/blueprint.yml

@@ -23,6 +23,10 @@ permissions:
   pull-requests: write    # Write access to pull requests
   actions: write          # Write access to GitHub Actions
 
+env:
+  LEAN_EXPOSITION_REPO: LeanMachineLearning/exposition
+  LEAN_EXPOSITION_REF: main
+
 jobs:
   build_project:
     runs-on: ubuntu-latest
@@ -55,6 +59,26 @@ jobs:
         run: |
           ./scripts/build_docs.sh
 
+      - name: Clone lean-exposition
+        run: |
+          git clone --depth 1 --branch "$LEAN_EXPOSITION_REF" \
+            "https://github.com/$LEAN_EXPOSITION_REPO" /tmp/lean-exposition
+
+      - name: Build exposition binary
+        run: |
+          cd /tmp/lean-exposition && lake build exposition
+          echo "EXPOSITION_BIN=/tmp/lean-exposition/.lake/build/bin/exposition" >> "$GITHUB_ENV"
+
+      - name: Build exposition documentation
+        run: |
+          lake env "$EXPOSITION_BIN" \
+            --root LeanMachineLearning \
+            --repo-url https://github.com/LeanMachineLearning/LML \
+            --output ./exposition \
+            --exclude-lib LMLTutorial
+          mkdir -p home_page/exposition
+          cp -r exposition/html-multi/* home_page/exposition
+
       - name: Compile blueprint and documentation
         uses: leanprover-community/docgen-action@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14
         with:

.gitignore

@@ -40,6 +40,7 @@ blueprint/src/web.pdf
 
 ## Website
 /home_page/
+/exposition/
 
 ## Tutorial and docs
 /LMLTutorial/.lake/

LMLTutorial/Front.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
 import LMLTutorial.Pages.BasicProbability
 import LMLTutorial.Pages.DefiningAlgorithm
 import LMLTutorial.Pages.Installation

LMLTutorial/Tutorial.lean

@@ -1,7 +1,14 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
 import VersoManual
-
 import LMLTutorial.Front
 
+set_option linter.style.header false
+set_option linter.style.setOption false
+
 open Verso.Genre.Manual Verso.Output.Html
 
 def extraHead : Array Verso.Output.Html := #[

LMLTutorial/static_files/style.css

@@ -3,6 +3,7 @@
   --accent-compl: #e8a0a0;
   --background: #fef9f9;
   --background-lighter: #fefcfc;
+  --verso-content-max-width: 60rem;
 }
 
 @font-face {