Add a stable, separate TODO board

.github/workflows/build-site.yml

@@ -14,6 +14,10 @@ jobs:
       - uses: actions/setup-python@v5
         with:
           python-version: "3.x"
+      - name: Validate homepage snapshot
+        run: python3 tools/build_homepage_data.py --validate-only
+      - name: Test homepage data extraction
+        run: python3 -m unittest discover -s tools -p "test_*.py"
       - name: Rebuild generated HTML
         run: python3 tools/build_site.py
       - name: Check generated files are committed

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

@@ -0,0 +1,45 @@
+name: Refresh homepage data
+
+on:
+  schedule:
+    - cron: "17 5 * * 1"
+  workflow_dispatch:
+
+permissions:
+  contents: write
+
+concurrency:
+  group: refresh-homepage-data
+  cancel-in-progress: true
+
+jobs:
+  refresh:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/checkout@v4
+        with:
+          repository: stat-lib/statlib
+          path: _upstream/statlib
+          fetch-depth: 1
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.x"
+      - name: Refresh the stable homepage snapshot
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: python3 tools/build_homepage_data.py --statlib-root _upstream/statlib --refresh-activity
+      - name: Rebuild generated HTML
+        run: python3 tools/build_site.py
+      - name: Check generated files
+        run: git diff --check
+      - name: Commit updated data
+        run: |
+          if git diff --quiet; then
+            exit 0
+          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 commit -m "chore: refresh homepage data"
+          git push

.gitignore

@@ -8,3 +8,4 @@ _out/
 node_modules/
 tmp/
 test-results/
+_upstream/

README.md

@@ -25,3 +25,13 @@ git status
 ```
 
 Include the changed `content/*.md` files and the regenerated `.html` files. CI fails if the generated HTML is stale.
+
+## Homepage Data
+
+The homepage reads `data/homepage.json`, a same-origin snapshot generated from the public
+`stat-lib/statlib` repository. Visitors never call the GitHub API directly.
+
+The `Refresh homepage data` workflow updates the snapshot each Monday and can also be run
+manually. It extracts structured `/- TODO: ... -/` theorem comments from Lean source files and
+collects the last 52 weeks of repository activity. If GitHub activity cannot be refreshed, the
+generator retains the last successful activity snapshot.

content/index.md

@@ -1,21 +1,22 @@
 ---
 title: Statlib
 description: A Lean 4 library for foundational and modern theoretical statistics.
-script: contributors.js
+script: homepage.js
 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. Please check out our contributors [below](#activity) (activity loaded live from [GitHub](https://github.com/stat-lib/statlib/graphs/contributors?all=1)). Interested in joining us? Check out our Zulip channel [here](https://leanprover.zulipchat.com/#narrow/channel/611809-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).
 
-## Community Activity {#activity .people}
+## Open formalization work {#todos .todo-section}
 
-- ![Bo Cowgill](https://avatars.githubusercontent.com/bocowgill) **[Bo Cowgill](https://github.com/bocowgill)** *@bocowgill*
-- ![Yongxi (Aaron) Lin](https://avatars.githubusercontent.com/CoolRmal) **[Yongxi (Aaron) Lin](https://github.com/CoolRmal)** *@CoolRmal*
-- ![Rémy Degenne](https://avatars.githubusercontent.com/RemyDegenne) **[Rémy Degenne](https://github.com/RemyDegenne)** *@RemyDegenne*
-- ![Rajarshi Mukherjee](https://avatars.githubusercontent.com/rajarshi-mukherjee24) **[Rajarshi Mukherjee](https://github.com/rajarshi-mukherjee24)** *@rajarshi-mukherjee24*
-- ![Zixiao Jolene Wang](https://avatars.githubusercontent.com/zixiaowang17) **[Zixiao Jolene Wang](https://github.com/zixiaowang17)** *@zixiaowang17*
-- ![Bjørn Kjos-Hanssen](https://avatars.githubusercontent.com/bjoernkjoshanssen) **[Bjørn Kjos-Hanssen](https://github.com/bjoernkjoshanssen)** *@bjoernkjoshanssen*
-- ![Qingyuan Zhao](https://avatars.githubusercontent.com/qingyuanzhao) **[Qingyuan Zhao](https://github.com/qingyuanzhao)** *@qingyuanzhao*
-- ![Richard Guo](https://avatars.githubusercontent.com/richardkwo) **[Richard Guo](https://github.com/richardkwo)** *@richardkwo*
+Statements marked `TODO` in Statlib are collected here automatically. They are concrete starting points for contributors and are not compiled declarations yet.
+
+[[todo-board]]
+
+## Community activity {#activity .people}
+
+Activity is refreshed from GitHub on a schedule and served as a stable snapshot.
+
+[[community-activity]]

contribute.html

@@ -4,7 +4,7 @@
 <meta charset="utf-8">
 <meta name="viewport" content="width=device-width, initial-scale=1">
 <title>Contributing to Statlib</title>
-<link rel="stylesheet" href="site.css?v=20260922-contributors">
+<link rel="stylesheet" href="site.css?v=20261001-homepage">
 </head>
 <body class="site-page">