From b402d6f3106ebc373a504a53a8c3bf393473b7cf Mon Sep 17 00:00:00 2001 From: zixiaowang17 Date: Thu, 1 Oct 2026 15:57:23 -0400 Subject: [PATCH] refactor: move TODO board to its own page --- .github/workflows/refresh-homepage-data.yml | 2 +- README.md | 1 + content/index.md | 8 +---- content/todos.md | 12 +++++++ contribute.html | 1 + governance.html | 1 + index.html | 10 ++---- roadmap.html | 1 + todos.html | 38 +++++++++++++++++++++ tools/build_site.py | 2 ++ 10 files changed, 60 insertions(+), 16 deletions(-) create mode 100644 content/todos.md create mode 100644 todos.html diff --git a/.github/workflows/refresh-homepage-data.yml b/.github/workflows/refresh-homepage-data.yml index 0d96d61..9db1ccb 100644 --- a/.github/workflows/refresh-homepage-data.yml +++ b/.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 diff --git a/README.md b/README.md index daebc5b..dc09c7f 100644 --- a/README.md +++ b/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: diff --git a/content/index.md b/content/index.md index e988e16..04e8d2b 100644 --- a/content/index.md +++ b/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} diff --git a/content/todos.md b/content/todos.md new file mode 100644 index 0000000..2b0e376 --- /dev/null +++ b/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]] diff --git a/contribute.html b/contribute.html index 5f4ae72..31cbc9f 100644 --- a/contribute.html +++ b/contribute.html @@ -15,6 +15,7 @@ About Tutorial Roadmap + TODOs Contribute Governance diff --git a/governance.html b/governance.html index 38c4be3..cb43dd2 100644 --- a/governance.html +++ b/governance.html @@ -16,6 +16,7 @@ About Tutorial Roadmap + TODOs Contribute Governance diff --git a/index.html b/index.html index ff0d64d..2a9c460 100644 --- a/index.html +++ b/index.html @@ -16,6 +16,7 @@ About Tutorial Roadmap + TODOs Contribute Governance @@ -24,14 +25,7 @@

Statlib

-

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.

-
-

Open formalization work

-

Statements marked TODO in Statlib are collected here automatically. They are concrete starting points for contributors and are not compiled declarations yet.

-
-

Loading open statements…

-
-
+

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. Interested in joining us? Visit our Zulip channel.

Community activity

Activity is refreshed from GitHub on a schedule and served as a stable snapshot.

diff --git a/roadmap.html b/roadmap.html index 547852a..de2210c 100644 --- a/roadmap.html +++ b/roadmap.html @@ -16,6 +16,7 @@ About Tutorial Roadmap + TODOs Contribute Governance
diff --git a/todos.html b/todos.html new file mode 100644 index 0000000..d1e3679 --- /dev/null +++ b/todos.html @@ -0,0 +1,38 @@ + + + + + +Open formalization work — Statlib + + + + + + + + +
+
+

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.

+
+

Loading open statements…

+
+
+
+ + + + + diff --git a/tools/build_site.py b/tools/build_site.py index 9fd4efe..c6eca98 100755 --- a/tools/build_site.py +++ b/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"), ]