Move the TODO board to its own page

.github/workflows/refresh-homepage-data.yml

@@ -40,6 +40,6 @@ jobs:
           fi
           git config user.name "github-actions[bot]"
           git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
-          git add data/homepage.json index.html
+          git add data/homepage.json index.html todos.html
           git commit -m "chore: refresh homepage data"
           git push

README.md

@@ -8,6 +8,7 @@ Edit Markdown files in `content/`, not the generated root HTML files.
 
 - `content/index.md` builds `index.html`
 - `content/roadmap.md` builds `roadmap.html`
+- `content/todos.md` builds `todos.html`
 - `content/contribute.md` builds `contribute.html`
 
 After editing Markdown, rebuild the HTML:

content/index.md

@@ -7,13 +7,7 @@ intro: false
 
 # Statlib
 
-[Statlib](https://github.com/stat-lib/statlib) is an open community that aims to support the verification of classical, contemporary, and emerging research in mathematical statistics; its vision and goals are shaped by the whole community. Browse the open formalization work below, or join the discussion in our [Zulip channel](https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib).
-
-## Open formalization work {#todos .todo-section}
-
-Statements marked `TODO` in Statlib are collected here automatically. They are concrete starting points for contributors and are not compiled declarations yet.
-
-[[todo-board]]
+[Statlib](https://github.com/stat-lib/statlib) is an open community that aims to support the verification of classical, contemporary, and emerging research in mathematical statistics; its vision and goals are shaped by the whole community. Please check out our contributors [below](#activity). Interested in joining us? Visit our [Zulip channel](https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib).
 
 ## Community activity {#activity .people}
 

content/todos.md

@@ -0,0 +1,12 @@
+---
+title: Open formalization work — Statlib
+description: Lean theorem statements currently open for contribution in Statlib.
+script: homepage.js
+intro: true
+---
+
+# Open formalization work
+
+These theorem statements are preserved as structured `TODO` comments in Statlib rather than compiled declarations. Each item links to its exact source location and is a concrete starting point for contributors.
+
+[[todo-board]]

contribute.html

@@ -15,6 +15,7 @@
     <a href="index.html">About</a>
     <a href="tutorial/index.html">Tutorial</a>
     <a href="roadmap.html">Roadmap</a>
+    <a href="todos.html">TODOs</a>
     <a href="contribute.html" class="active">Contribute</a>
     <a href="governance.html">Governance</a>
   </div>

governance.html

@@ -16,6 +16,7 @@
     <a href="index.html">About</a>
     <a href="tutorial/index.html">Tutorial</a>
     <a href="roadmap.html">Roadmap</a>
+    <a href="todos.html">TODOs</a>
     <a href="contribute.html">Contribute</a>
     <a href="governance.html" class="active">Governance</a>
   </div>

index.html

@@ -16,6 +16,7 @@
     <a href="index.html" class="active">About</a>
     <a href="tutorial/index.html">Tutorial</a>
     <a href="roadmap.html">Roadmap</a>
+    <a href="todos.html">TODOs</a>
     <a href="contribute.html">Contribute</a>
     <a href="governance.html">Governance</a>
   </div>
@@ -24,14 +25,7 @@
 <main>
   <div class="wrap">
     <h1>Statlib</h1>
-    <p><a href="https://github.com/stat-lib/statlib" target="_blank" rel="noopener">Statlib</a> is an open community that aims to support the verification of classical, contemporary, and emerging research in mathematical statistics; its vision and goals are shaped by the whole community. Browse the open formalization work below, or join the discussion in our <a href="https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib" target="_blank" rel="noopener">Zulip channel</a>.</p>
-    <section id="todos" class="todo-section">
-    <h2>Open formalization work</h2>
-    <p>Statements marked <code>TODO</code> in Statlib are collected here automatically. They are concrete starting points for contributors and are not compiled declarations yet.</p>
-    <div id="todo-board" class="data-board" aria-live="polite" aria-busy="true">
-    <p class="data-status">Loading open statements…</p>
-    </div>
-    </section>
+    <p><a href="https://github.com/stat-lib/statlib" target="_blank" rel="noopener">Statlib</a> is an open community that aims to support the verification of classical, contemporary, and emerging research in mathematical statistics; its vision and goals are shaped by the whole community. Please check out our contributors <a href="#activity">below</a>. Interested in joining us? Visit our <a href="https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib" target="_blank" rel="noopener">Zulip channel</a>.</p>
     <section id="activity" class="people">
     <h2>Community activity</h2>
     <p>Activity is refreshed from GitHub on a schedule and served as a stable snapshot.</p>

roadmap.html

@@ -16,6 +16,7 @@
     <a href="index.html">About</a>
     <a href="tutorial/index.html">Tutorial</a>
     <a href="roadmap.html" class="active">Roadmap</a>
+    <a href="todos.html">TODOs</a>
     <a href="contribute.html">Contribute</a>
     <a href="governance.html">Governance</a>
   </div>

todos.html

@@ -0,0 +1,38 @@
+<!doctype html>
+<html lang="en">
+<head>
+<meta charset="utf-8">
+<meta name="viewport" content="width=device-width, initial-scale=1">
+<title>Open formalization work — Statlib</title>
+<meta name="description" content="Lean theorem statements currently open for contribution in Statlib.">
+<link rel="stylesheet" href="site.css?v=20261001-homepage">
+</head>
+<body class="site-page">
+
+<!-- Generated from content/*.md by tools/build_site.py. Edit Markdown source, not this file. -->
+<nav>
+  <a href="index.html" class="brand">Statlib</a>
+  <div class="links">
+    <a href="index.html">About</a>
+    <a href="tutorial/index.html">Tutorial</a>
+    <a href="roadmap.html">Roadmap</a>
+    <a href="todos.html" class="active">TODOs</a>
+    <a href="contribute.html">Contribute</a>
+    <a href="governance.html">Governance</a>
+  </div>
+</nav>
+
+<main>
+  <div class="wrap">
+    <h1>Open formalization work</h1>
+    <p class="intro">These theorem statements are preserved as structured <code>TODO</code> comments in Statlib rather than compiled declarations. Each item links to its exact source location and is a concrete starting point for contributors.</p>
+    <div id="todo-board" class="data-board" aria-live="polite" aria-busy="true">
+    <p class="data-status">Loading open statements…</p>
+    </div>
+  </div>
+</main>
+
+<script src="homepage.js" defer></script>
+
+</body>
+</html>

tools/build_site.py

@@ -14,6 +14,7 @@
 PAGES = {
     "index": "index.html",
     "roadmap": "roadmap.html",
+    "todos": "todos.html",
     "contribute": "contribute.html",
     "governance": "governance.html",
 }
@@ -22,6 +23,7 @@
     ("index.html", "About", "index"),
     ("tutorial/index.html", "Tutorial", None),
     ("roadmap.html", "Roadmap", "roadmap"),
+    ("todos.html", "TODOs", "todos"),
     ("contribute.html", "Contribute", "contribute"),
     ("governance.html", "Governance", "governance"),
 ]