From 8754d058399df6df845064a3eae5b8a5b376a47d Mon Sep 17 00:00:00 2001 From: zixiaowang17 Date: Thu, 1 Oct 2026 15:50:55 -0400 Subject: [PATCH] feat: add stable homepage work board --- .github/workflows/build-site.yml | 4 + .github/workflows/refresh-homepage-data.yml | 45 + .gitignore | 1 + README.md | 10 + content/index.md | 23 +- contribute.html | 2 +- contributors.js | 289 -- data/homepage.json | 3063 +++++++++++++++++++ governance.html | 2 +- homepage.js | 367 +++ index.html | 29 +- roadmap.html | 2 +- site.css | 61 +- tools/build_homepage_data.py | 334 ++ tools/build_site.py | 19 +- tools/test_build_homepage_data.py | 45 + 16 files changed, 3977 insertions(+), 319 deletions(-) create mode 100644 .github/workflows/refresh-homepage-data.yml delete mode 100644 contributors.js create mode 100644 data/homepage.json create mode 100644 homepage.js create mode 100644 tools/build_homepage_data.py create mode 100644 tools/test_build_homepage_data.py diff --git a/.github/workflows/build-site.yml b/.github/workflows/build-site.yml index a662445..0e436bb 100644 --- a/.github/workflows/build-site.yml +++ b/.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 diff --git a/.github/workflows/refresh-homepage-data.yml b/.github/workflows/refresh-homepage-data.yml new file mode 100644 index 0000000..0d96d61 --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index 049a771..5d32aff 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,4 @@ _out/ node_modules/ tmp/ test-results/ +_upstream/ diff --git a/README.md b/README.md index 094e8c7..daebc5b 100644 --- a/README.md +++ b/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. diff --git a/content/index.md b/content/index.md index 981fefb..e988e16 100644 --- a/content/index.md +++ b/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]] diff --git a/contribute.html b/contribute.html index cba0086..5f4ae72 100644 --- a/contribute.html +++ b/contribute.html @@ -4,7 +4,7 @@ Contributing to Statlib - + diff --git a/contributors.js b/contributors.js deleted file mode 100644 index 5c0a5c5..0000000 --- a/contributors.js +++ /dev/null @@ -1,289 +0,0 @@ -// Renders a live community activity board (commits, comments, issues/PRs opened) into #activity. -// The static list in contributors.md stays as the fallback if the API is unavailable. -(function () { - "use strict"; - - const REPO = "stat-lib/statlib"; - const API = `https://api.github.com/repos/${REPO}`; - const WEEK = 7 * 24 * 3600; - - // Accounts that are not individual people. - const HIDDEN = new Set(["formal-stat"]); - - // GitHub login -> display name and preferred homepage. - const PEOPLE = { - RemyDegenne: { name: "Rémy Degenne", url: "https://remydegenne.github.io/" }, - zixiaowang17: { name: "Zixiao Jolene Wang", url: "https://zixiaowang17.github.io/" }, - bocowgill: { name: "Bo Cowgill", url: "http://bocowgill.com" }, - "rajarshi-mukherjee24": { name: "Rajarshi Mukherjee", url: "https://rajarshi-mukherjee24.github.io/" }, - CoolRmal: { name: "Yongxi (Aaron) Lin", url: "https://coolrmal.github.io/" }, - richardkwo: { name: "Richard Guo", url: "https://unbiased.co.in" }, - qingyuanzhao: { name: "Qingyuan Zhao", url: "http://www.statslab.cam.ac.uk/~qz280/" }, - bjoernkjoshanssen: { name: "Bjørn Kjos-Hanssen", url: "http://math.hawaii.edu/wordpress/bjoern/" }, - }; - - // Stacked bottom to top in this order; colors are set in site.css. - const KINDS = [ - { key: "commits", one: "commit", many: "commits" }, - { key: "comments", one: "comment", many: "comments" }, - { key: "opened", one: "issue/PR opened", many: "issues/PRs opened" }, - ]; - - const section = document.getElementById("activity"); - if (!section) return; - - const isPerson = (user) => - user && user.type !== "Bot" && !user.login.endsWith("[bot]") && !HIDDEN.has(user.login); - const displayName = (login) => (PEOPLE[login] || {}).name || login; - - const el = (tag, attrs = {}, children = []) => { - const node = document.createElement(tag); - for (const [key, value] of Object.entries(attrs)) { - if (key === "text") node.textContent = value; - else node.setAttribute(key, value); - } - for (const child of [].concat(children)) if (child) node.append(child); - return node; - }; - - const svg = (tag, attrs = {}) => { - const node = document.createElementNS("http://www.w3.org/2000/svg", tag); - for (const [key, value] of Object.entries(attrs)) node.setAttribute(key, value); - return node; - }; - - const fmtDate = (seconds) => - new Date(seconds * 1000).toLocaleDateString("en-US", { month: "short", day: "numeric", year: "numeric", timeZone: "UTC" }); - const fmtMonth = (seconds) => - new Date(seconds * 1000).toLocaleDateString("en-US", { month: "short", timeZone: "UTC" }); - const count = (n, kind) => `${n.toLocaleString()} ${n === 1 ? kind.one : kind.many}`; - - // GitHub's commit stats bucket weeks starting Sunday 00:00 UTC; match that. - const weekStart = (iso) => { - const d = new Date(iso); - d.setUTCHours(0, 0, 0, 0); - d.setUTCDate(d.getUTCDate() - d.getUTCDay()); - return d.getTime() / 1000; - }; - - const tooltip = el("div", { class: "gh-tooltip", role: "status", "aria-live": "polite" }); - document.body.append(tooltip); - const showTip = (event, text) => { - tooltip.textContent = text; - tooltip.style.display = "block"; - const box = tooltip.getBoundingClientRect(); - let x = event.clientX + 12; - if (x + box.width > window.innerWidth - 8) x = event.clientX - box.width - 12; - tooltip.style.left = `${x + window.scrollX}px`; - tooltip.style.top = `${event.clientY + window.scrollY - box.height - 10}px`; - }; - const hideTip = () => { tooltip.style.display = "none"; }; - - const weekTotal = (week, kinds) => kinds.reduce((sum, k) => sum + week[k.key], 0); - - // Stacked weekly columns. Every chart shares yMax so heights compare across people. - function weeklyChart(weeks, yMax, kinds, { height, axis, label }) { - const width = 600; - const plotH = height - (axis ? 18 : 0); - const slot = width / weeks.length; - const barW = Math.max(1, Math.min(slot - 2, slot * 0.6)); - const gap = 2; // surface gap between stacked segments - const root = svg("svg", { - viewBox: `0 0 ${width} ${height}`, - preserveAspectRatio: "none", - class: "gh-chart", - role: "img", - "aria-label": label, - }); - root.style.height = `${height}px`; - root.append(svg("line", { x1: 0, x2: width, y1: plotH, y2: plotH, class: "gh-baseline" })); - - weeks.forEach((week, i) => { - const x = i * slot + (slot - barW) / 2; - const present = kinds.filter((k) => week[k.key] > 0); - let base = plotH; - present.forEach((kind, j) => { - const h = (week[kind.key] / yMax) * (plotH - 4); - const top = base - h; - const isTop = j === present.length - 1; - const r = isTop ? Math.min(2, barW / 2, h) : 0; - const bottom = j === 0 ? base : base - gap / 2; - const segTop = isTop ? top : top + gap / 2; - if (bottom - segTop > 0.5) { - root.append(svg("path", { - class: `gh-bar gh-${kind.key}`, - d: `M${x},${bottom}V${segTop + r}Q${x},${segTop} ${x + r},${segTop}H${x + barW - r}Q${x + barW},${segTop} ${x + barW},${segTop + r}V${bottom}Z`, - })); - } - base = top; - }); - - // Full-height hit target, larger than the mark. - const hit = svg("rect", { x: i * slot, y: 0, width: slot, height: plotH, class: "gh-hit" }); - const parts = present.map((k) => count(week[k.key], k)); - const text = `Week of ${fmtDate(week.w)}: ${parts.length ? parts.join(", ") : "no activity"}`; - hit.addEventListener("mousemove", (e) => { hit.classList.add("on"); showTip(e, text); }); - hit.addEventListener("mouseleave", () => { hit.classList.remove("on"); hideTip(); }); - root.append(hit); - - if (axis) { - const prev = weeks[i - 1]; - if (!prev || fmtMonth(prev.w) !== fmtMonth(week.w)) { - const t = svg("text", { x, y: height - 4, class: "gh-axis" }); - t.textContent = fmtMonth(week.w); - root.append(t); - } - } - }); - return root; - } - - function legend(kinds) { - return el("div", { class: "gh-legend" }, kinds.map((k) => - el("span", { class: "gh-legend-item" }, [el("span", { class: `gh-swatch gh-${k.key}` }), k.many]) - )); - } - - function card(row, rank, grand, yMax, kinds) { - const info = PEOPLE[row.user.login] || {}; - const meta = KINDS.filter((k) => row[k.key] > 0).map((k) => count(row[k.key], k)); - const pct = grand ? (row.total / grand) * 100 : 0; - const share = el("div", { class: "gh-share", title: `${pct.toFixed(0)}% of all activity` }, [ - el("span", { class: "gh-share-fill" }), - ]); - share.firstChild.style.width = `${pct}%`; - const node = el("li", { class: "gh-card" }, [ - el("span", { class: "gh-rank", text: `#${rank}` }), - el("div", { class: "gh-person" }, [ - el("img", { src: `https://avatars.githubusercontent.com/${row.user.login}?s=96`, alt: "", class: "gh-avatar", loading: "lazy" }), - el("div", { class: "gh-who" }, [ - el("a", { href: info.url || row.user.html_url, target: "_blank", rel: "noopener", class: "gh-name", text: displayName(row.user.login) }), - el("a", { href: row.user.html_url, target: "_blank", rel: "noopener", class: "gh-login", text: `@${row.user.login}` }), - ]), - el("div", { class: "gh-meta", text: meta.join(" · ") }), - ]), - share, - ]); - if (row.weeks.length) { - node.append(weeklyChart(row.weeks, yMax, kinds, { height: 56, axis: false, label: `Weekly activity by ${displayName(row.user.login)}` })); - } - return node; - } - - function render(rows, weekStarts, commitWeeks) { - // Commits only join the charts when GitHub returned weekly commit stats. - const kinds = commitWeeks ? KINDS : KINDS.slice(1); - const grand = rows.reduce((sum, r) => sum + r.total, 0); - const view = el("div", { class: "gh-view" }); - - if (weekStarts.length) { - const combined = weekStarts.map((w, i) => { - const week = { w }; - for (const k of KINDS) week[k.key] = rows.reduce((sum, r) => sum + r.weeks[i][k.key], 0); - return week; - }); - const combinedMax = Math.max(1, ...combined.map((w) => weekTotal(w, kinds))); - view.append(el("div", { class: "gh-overview" }, [ - el("div", { class: "gh-overview-head" }, [ - el("div", { class: "gh-overview-title", text: `Activity per week · ${rows.length} people` }), - legend(kinds), - ]), - weeklyChart(combined, combinedMax, kinds, { height: 120, axis: true, label: `Weekly activity in ${REPO}` }), - ])); - } - - const personMax = Math.max(1, ...rows.flatMap((r) => r.weeks.map((w) => weekTotal(w, kinds)))); - const grid = el("ol", { class: "gh-cards" }); - rows.forEach((r, i) => grid.append(card(r, i + 1, grand, personMax, kinds))); - view.append(grid); - section.querySelector("ul").replaceWith(view); - } - - const sleep = (ms) => new Promise((resolve) => setTimeout(resolve, ms)); - - // GitHub answers 202 while it computes statistics; poll briefly. - async function loadStats() { - for (let attempt = 0; attempt < 5; attempt++) { - const res = await fetch(`${API}/stats/contributors`); - if (res.status === 200) return res.json(); - if (res.status !== 202) throw new Error(`stats ${res.status}`); - await sleep(1500 * (attempt + 1)); - } - throw new Error("stats not ready"); - } - - // Follows GitHub's Link header to collect every page of a list endpoint. - async function fetchAll(url, maxPages = 10) { - const items = []; - for (let page = 0; url && page < maxPages; page++) { - const res = await fetch(url); - if (!res.ok) throw new Error(`${url} ${res.status}`); - items.push(...(await res.json())); - const next = /<([^>]+)>;\s*rel="next"/.exec(res.headers.get("Link") || ""); - url = next ? next[1] : null; - } - return items; - } - - async function main() { - const [stats, comments, issues] = await Promise.all([ - loadStats().catch(() => null), - fetchAll(`${API}/issues/comments?per_page=100`).catch(() => []), - fetchAll(`${API}/issues?state=all&per_page=100`).catch(() => []), - ]); - // Without weekly stats, fall back to plain commit totals. - const totals = stats ? [] : await fetchAll(`${API}/contributors?per_page=100`).catch(() => []); - - const events = []; // [user, kind, weekStart] - comments.forEach((c) => events.push([c.user, "comments", weekStart(c.created_at)])); - issues.forEach((i) => events.push([i.user, "opened", weekStart(i.created_at)])); - - // Continuous week axis from the first activity to the current week. - const starts = events.map((e) => e[2]); - if (stats && stats[0]) starts.push(stats[0].weeks[0].w); - const weekStarts = []; - if (starts.length) { - const end = weekStart(new Date().toISOString()); - for (let w = Math.min(...starts); w <= end; w += WEEK) weekStarts.push(w); - } - const index = new Map(weekStarts.map((w, i) => [w, i])); - - const people = new Map(); - const row = (user) => { - if (!people.has(user.login)) { - people.set(user.login, { - user, commits: 0, comments: 0, opened: 0, - weeks: weekStarts.map((w) => ({ w, commits: 0, comments: 0, opened: 0 })), - }); - } - return people.get(user.login); - }; - - (stats || []).filter((s) => isPerson(s.author)).forEach((s) => { - const r = row(s.author); - s.weeks.forEach((wk) => { - if (!wk.c) return; - r.commits += wk.c; - const i = index.get(wk.w); - if (i != null) r.weeks[i].commits += wk.c; - }); - }); - totals.filter(isPerson).forEach((c) => { row(c).commits += c.contributions; }); - events.forEach(([user, kind, w]) => { - if (!isPerson(user)) return; - const r = row(user); - r[kind] += 1; - r.weeks[index.get(w)][kind] += 1; - }); - - const rows = [...people.values()] - .map((r) => Object.assign(r, { total: r.commits + r.comments + r.opened })) - .filter((r) => r.total > 0) - .sort((a, b) => b.total - a.total || a.user.login.localeCompare(b.user.login)); - if (rows.length) render(rows, weekStarts, Boolean(stats)); - } - - main().catch(() => { - // Keep the static fallback list. - }); -})(); diff --git a/data/homepage.json b/data/homepage.json new file mode 100644 index 0000000..6e3ba5e --- /dev/null +++ b/data/homepage.json @@ -0,0 +1,3063 @@ +{ + "generated_at": "2026-10-01T19:48:51+00:00", + "statlib_sha": "49d91527a7f57d3e81259cbcc256bcf6ecd3d730", + "todos": [ + { + "name": "Contiguous1.contiguous2", + "kind": "theorem", + "module": "Statlib.Contiguity.Def", + "summary": "Prove that `Contiguous1` implies `Contiguous2`.", + "statement": "theorem Contiguous1.contiguous2 {l : Filter α} (P Q : ∀ a, ProbabilityMeasure (Ω a)) (hPQ : Contiguous1 l P Q) : Contiguous2 l P Q", + "source_url": "https://github.com/stat-lib/statlib/blob/49d91527a7f57d3e81259cbcc256bcf6ecd3d730/Statlib/Contiguity/Def.lean#L149" + }, + { + "name": "contiguous2_iff_contiguous3", + "kind": "theorem", + "module": "Statlib.Contiguity.Def", + "summary": "Prove the equivalence of `Contiguous2` and `Contiguous3`.", + "statement": "theorem contiguous2_iff_contiguous3 {l : Filter α} (P Q : ∀ a, ProbabilityMeasure (Ω a)) : Contiguous2 l P Q ↔ Contiguous3 l P Q", + "source_url": "https://github.com/stat-lib/statlib/blob/49d91527a7f57d3e81259cbcc256bcf6ecd3d730/Statlib/Contiguity/Def.lean#L155" + }, + { + "name": "Contiguous3.contiguous1", + "kind": "theorem", + "module": "Statlib.Contiguity.Def", + "summary": "Prove that `Contiguous3` implies `Contiguous1`.", + "statement": "theorem Contiguous3.contiguous1 {l : Filter α} (P Q : ∀ a, ProbabilityMeasure (Ω a)) (hPQ : Contiguous3 l P Q) : Contiguous1 l P Q", + "source_url": "https://github.com/stat-lib/statlib/blob/49d91527a7f57d3e81259cbcc256bcf6ecd3d730/Statlib/Contiguity/Def.lean#L161" + }, + { + "name": "Contiguous.TFAE", + "kind": "theorem", + "module": "Statlib.Contiguity.Def", + "summary": "Prove that the first four definitions of contiguity are equivalent.", + "statement": "theorem Contiguous.TFAE {l : Filter α} (P Q : ∀ a, ProbabilityMeasure (Ω a)) : List.TFAE [Contiguous1 l P Q, Contiguous2 l P Q, Contiguous3 l P Q, Contiguous4 l P Q]", + "source_url": "https://github.com/stat-lib/statlib/blob/49d91527a7f57d3e81259cbcc256bcf6ecd3d730/Statlib/Contiguity/Def.lean#L167" + }, + { + "name": "Contiguous5.contiguous1_of_hasAntitoneBasis_le_cofinite", + "kind": "theorem", + "module": "Statlib.Contiguity.Def", + "summary": "Replace the AI-generated proof with a reviewed proof.", + "statement": "theorem Contiguous5.contiguous1_of_hasAntitoneBasis_le_cofinite {l : Filter α} {P Q : ∀ a, ProbabilityMeasure (Ω a)} {b : ℕ → Set α} (hPQ : Contiguous5 l P Q) (hb : l.HasAntitoneBasis b) (hl : l ≤ cofinite) : Contiguous1 l P Q", + "source_url": "https://github.com/stat-lib/statlib/blob/49d91527a7f57d3e81259cbcc256bcf6ecd3d730/Statlib/Contiguity/Def.lean#L173" + }, + { + "name": "Contiguous5.contiguous1_of_isCountablyGenerated_le_cofinite", + "kind": "theorem", + "module": "Statlib.Contiguity.Def", + "summary": "Prove the countably generated specialization after the antitone-basis result.", + "statement": "theorem Contiguous5.contiguous1_of_isCountablyGenerated_le_cofinite {l : Filter α} [l.IsCountablyGenerated] {P Q : ∀ a, ProbabilityMeasure (Ω a)} (hPQ : Contiguous5 l P Q) (hl : l ≤ cofinite) : Contiguous1 l P Q", + "source_url": "https://github.com/stat-lib/statlib/blob/49d91527a7f57d3e81259cbcc256bcf6ecd3d730/Statlib/Contiguity/Def.lean#L180" + }, + { + "name": "Contiguous5.contiguous1_atTop", + "kind": "theorem", + "module": "Statlib.Contiguity.Def", + "summary": "Prove the `atTop` specialization of `Contiguous5 → Contiguous1`.", + "statement": "theorem Contiguous5.contiguous1_atTop (hPQ : Contiguous5 atTop P Q) : Contiguous1 atTop P Q", + "source_url": "https://github.com/stat-lib/statlib/blob/49d91527a7f57d3e81259cbcc256bcf6ecd3d730/Statlib/Contiguity/Def.lean#L191" + }, + { + "name": "contiguous5_atTop_iff_contiguous1", + "kind": "theorem", + "module": "Statlib.Contiguity.Def", + "summary": "Prove the equivalence of `Contiguous1` and `Contiguous5` for sequences.", + "statement": "theorem contiguous5_atTop_iff_contiguous1 : Contiguous1 atTop P Q ↔ Contiguous5 atTop P Q", + "source_url": "https://github.com/stat-lib/statlib/blob/49d91527a7f57d3e81259cbcc256bcf6ecd3d730/Statlib/Contiguity/Def.lean#L196" + }, + { + "name": "Contiguous.nat_TFAE", + "kind": "theorem", + "module": "Statlib.Contiguity.Def", + "summary": "Prove that all five definitions are equivalent for sequences.", + "statement": "theorem Contiguous.nat_TFAE : List.TFAE [Contiguous1 atTop P Q, Contiguous2 atTop P Q, Contiguous3 atTop P Q, Contiguous4 atTop P Q, Contiguous5 atTop P Q]", + "source_url": "https://github.com/stat-lib/statlib/blob/49d91527a7f57d3e81259cbcc256bcf6ecd3d730/Statlib/Contiguity/Def.lean#L201" + } + ], + "activity": { + "repository": "stat-lib/statlib", + "window": "52 weeks", + "week_starts": [ + 1759622400, + 1760227200, + 1760832000, + 1761436800, + 1762041600, + 1762646400, + 1763251200, + 1763856000, + 1764460800, + 1765065600, + 1765670400, + 1766275200, + 1766880000, + 1767484800, + 1768089600, + 1768694400, + 1769299200, + 1769904000, + 1770508800, + 1771113600, + 1771718400, + 1772323200, + 1772928000, + 1773532800, + 1774137600, + 1774742400, + 1775347200, + 1775952000, + 1776556800, + 1777161600, + 1777766400, + 1778371200, + 1778976000, + 1779580800, + 1780185600, + 1780790400, + 1781395200, + 1782000000, + 1782604800, + 1783209600, + 1783814400, + 1784419200, + 1785024000, + 1785628800, + 1786233600, + 1786838400, + 1787443200, + 1788048000, + 1788652800, + 1789257600, + 1789862400, + 1790467200 + ], + "people": [ + { + "login": "RemyDegenne", + "name": "Rémy Degenne", + "profile_url": "https://github.com/RemyDegenne", + "homepage_url": "https://remydegenne.github.io/", + "avatar_url": "https://avatars.githubusercontent.com/u/4094732?v=4", + "commits": 23, + "comments": 2, + "opened": 4, + "weeks": [ + { + "w": 1759622400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760227200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760832000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1761436800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762041600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762646400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763251200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763856000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1764460800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765065600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765670400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766275200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766880000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1767484800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768089600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768694400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769299200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769904000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1770508800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771113600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771718400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772323200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772928000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1773532800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774137600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774742400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775347200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775952000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1776556800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777161600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777766400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778371200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778976000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1779580800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780185600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780790400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1781395200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782000000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782604800, + "commits": 5, + "comments": 2, + "opened": 2 + }, + { + "w": 1783209600, + "commits": 4, + "comments": 0, + "opened": 0 + }, + { + "w": 1783814400, + "commits": 3, + "comments": 0, + "opened": 0 + }, + { + "w": 1784419200, + "commits": 1, + "comments": 0, + "opened": 0 + }, + { + "w": 1785024000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785628800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786233600, + "commits": 10, + "comments": 0, + "opened": 2 + }, + { + "w": 1786838400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1787443200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788048000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788652800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1789257600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1789862400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1790467200, + "commits": 0, + "comments": 0, + "opened": 0 + } + ], + "total": 29 + }, + { + "login": "zixiaowang17", + "name": "Zixiao Jolene Wang", + "profile_url": "https://github.com/zixiaowang17", + "homepage_url": "https://zixiaowang17.github.io/", + "avatar_url": "https://avatars.githubusercontent.com/u/94130343?v=4", + "commits": 17, + "comments": 6, + "opened": 1, + "weeks": [ + { + "w": 1759622400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760227200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760832000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1761436800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762041600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762646400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763251200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763856000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1764460800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765065600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765670400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766275200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766880000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1767484800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768089600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768694400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769299200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769904000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1770508800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771113600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771718400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772323200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772928000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1773532800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774137600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774742400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775347200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775952000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1776556800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777161600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777766400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778371200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778976000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1779580800, + "commits": 4, + "comments": 0, + "opened": 0 + }, + { + "w": 1780185600, + "commits": 1, + "comments": 0, + "opened": 0 + }, + { + "w": 1780790400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1781395200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782000000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782604800, + "commits": 3, + "comments": 4, + "opened": 0 + }, + { + "w": 1783209600, + "commits": 0, + "comments": 0, + "opened": 1 + }, + { + "w": 1783814400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1784419200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785024000, + "commits": 1, + "comments": 0, + "opened": 0 + }, + { + "w": 1785628800, + "commits": 2, + "comments": 0, + "opened": 0 + }, + { + "w": 1786233600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786838400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1787443200, + "commits": 0, + "comments": 1, + "opened": 0 + }, + { + "w": 1788048000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788652800, + "commits": 1, + "comments": 0, + "opened": 0 + }, + { + "w": 1789257600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1789862400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1790467200, + "commits": 5, + "comments": 1, + "opened": 0 + } + ], + "total": 24 + }, + { + "login": "bocowgill", + "name": "Bo Cowgill", + "profile_url": "https://github.com/bocowgill", + "homepage_url": "http://bocowgill.com", + "avatar_url": "https://avatars.githubusercontent.com/u/1121490?v=4", + "commits": 4, + "comments": 15, + "opened": 4, + "weeks": [ + { + "w": 1759622400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760227200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760832000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1761436800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762041600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762646400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763251200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763856000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1764460800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765065600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765670400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766275200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766880000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1767484800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768089600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768694400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769299200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769904000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1770508800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771113600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771718400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772323200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772928000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1773532800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774137600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774742400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775347200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775952000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1776556800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777161600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777766400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778371200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778976000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1779580800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780185600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780790400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1781395200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782000000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782604800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783209600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783814400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1784419200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785024000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785628800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786233600, + "commits": 0, + "comments": 0, + "opened": 1 + }, + { + "w": 1786838400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1787443200, + "commits": 2, + "comments": 2, + "opened": 1 + }, + { + "w": 1788048000, + "commits": 0, + "comments": 2, + "opened": 0 + }, + { + "w": 1788652800, + "commits": 2, + "comments": 8, + "opened": 0 + }, + { + "w": 1789257600, + "commits": 0, + "comments": 2, + "opened": 2 + }, + { + "w": 1789862400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1790467200, + "commits": 0, + "comments": 1, + "opened": 0 + } + ], + "total": 23 + }, + { + "login": "CoolRmal", + "name": "Yongxi (Aaron) Lin", + "profile_url": "https://github.com/CoolRmal", + "homepage_url": "https://coolrmal.github.io/", + "avatar_url": "https://avatars.githubusercontent.com/u/97214596?v=4", + "commits": 5, + "comments": 2, + "opened": 9, + "weeks": [ + { + "w": 1759622400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760227200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760832000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1761436800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762041600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762646400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763251200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763856000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1764460800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765065600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765670400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766275200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766880000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1767484800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768089600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768694400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769299200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769904000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1770508800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771113600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771718400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772323200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772928000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1773532800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774137600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774742400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775347200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775952000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1776556800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777161600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777766400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778371200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778976000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1779580800, + "commits": 1, + "comments": 0, + "opened": 1 + }, + { + "w": 1780185600, + "commits": 1, + "comments": 0, + "opened": 1 + }, + { + "w": 1780790400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1781395200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782000000, + "commits": 2, + "comments": 2, + "opened": 7 + }, + { + "w": 1782604800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783209600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783814400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1784419200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785024000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785628800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786233600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786838400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1787443200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788048000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788652800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1789257600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1789862400, + "commits": 1, + "comments": 0, + "opened": 0 + }, + { + "w": 1790467200, + "commits": 0, + "comments": 0, + "opened": 0 + } + ], + "total": 16 + }, + { + "login": "rajarshi-mukherjee24", + "name": "Rajarshi Mukherjee", + "profile_url": "https://github.com/rajarshi-mukherjee24", + "homepage_url": "https://rajarshi-mukherjee24.github.io/", + "avatar_url": "https://avatars.githubusercontent.com/u/49079135?v=4", + "commits": 4, + "comments": 4, + "opened": 5, + "weeks": [ + { + "w": 1759622400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760227200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760832000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1761436800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762041600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762646400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763251200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763856000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1764460800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765065600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765670400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766275200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766880000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1767484800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768089600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768694400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769299200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769904000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1770508800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771113600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771718400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772323200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772928000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1773532800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774137600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774742400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775347200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775952000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1776556800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777161600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777766400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778371200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778976000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1779580800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780185600, + "commits": 3, + "comments": 0, + "opened": 5 + }, + { + "w": 1780790400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1781395200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782000000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782604800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783209600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783814400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1784419200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785024000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785628800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786233600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786838400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1787443200, + "commits": 0, + "comments": 1, + "opened": 0 + }, + { + "w": 1788048000, + "commits": 0, + "comments": 1, + "opened": 0 + }, + { + "w": 1788652800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1789257600, + "commits": 1, + "comments": 1, + "opened": 0 + }, + { + "w": 1789862400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1790467200, + "commits": 0, + "comments": 1, + "opened": 0 + } + ], + "total": 13 + }, + { + "login": "bjoernkjoshanssen", + "name": "Bjørn Kjos-Hanssen", + "profile_url": "https://github.com/bjoernkjoshanssen", + "homepage_url": "http://math.hawaii.edu/wordpress/bjoern/", + "avatar_url": "https://avatars.githubusercontent.com/u/1740286?v=4", + "commits": 0, + "comments": 0, + "opened": 2, + "weeks": [ + { + "w": 1759622400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760227200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760832000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1761436800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762041600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762646400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763251200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763856000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1764460800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765065600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765670400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766275200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766880000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1767484800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768089600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768694400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769299200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769904000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1770508800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771113600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771718400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772323200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772928000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1773532800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774137600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774742400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775347200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775952000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1776556800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777161600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777766400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778371200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778976000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1779580800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780185600, + "commits": 0, + "comments": 0, + "opened": 1 + }, + { + "w": 1780790400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1781395200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782000000, + "commits": 0, + "comments": 0, + "opened": 1 + }, + { + "w": 1782604800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783209600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783814400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1784419200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785024000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785628800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786233600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786838400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1787443200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788048000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788652800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1789257600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1789862400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1790467200, + "commits": 0, + "comments": 0, + "opened": 0 + } + ], + "total": 2 + }, + { + "login": "blfang", + "name": "blfang", + "profile_url": "https://github.com/blfang", + "homepage_url": "https://github.com/blfang", + "avatar_url": "https://avatars.githubusercontent.com/u/1924485?v=4", + "commits": 1, + "comments": 0, + "opened": 1, + "weeks": [ + { + "w": 1759622400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760227200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760832000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1761436800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762041600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762646400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763251200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763856000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1764460800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765065600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765670400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766275200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766880000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1767484800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768089600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768694400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769299200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769904000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1770508800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771113600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771718400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772323200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772928000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1773532800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774137600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774742400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775347200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775952000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1776556800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777161600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777766400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778371200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778976000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1779580800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780185600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780790400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1781395200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782000000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782604800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783209600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783814400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1784419200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785024000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785628800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786233600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786838400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1787443200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788048000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788652800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1789257600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1789862400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1790467200, + "commits": 1, + "comments": 0, + "opened": 1 + } + ], + "total": 2 + }, + { + "login": "qingyuanzhao", + "name": "Qingyuan Zhao", + "profile_url": "https://github.com/qingyuanzhao", + "homepage_url": "http://www.statslab.cam.ac.uk/~qz280/", + "avatar_url": "https://avatars.githubusercontent.com/u/3944837?v=4", + "commits": 0, + "comments": 2, + "opened": 0, + "weeks": [ + { + "w": 1759622400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760227200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760832000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1761436800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762041600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762646400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763251200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763856000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1764460800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765065600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765670400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766275200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766880000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1767484800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768089600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768694400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769299200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769904000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1770508800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771113600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771718400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772323200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772928000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1773532800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774137600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774742400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775347200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775952000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1776556800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777161600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777766400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778371200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778976000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1779580800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780185600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780790400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1781395200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782000000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782604800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783209600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783814400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1784419200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785024000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785628800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786233600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786838400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1787443200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788048000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788652800, + "commits": 0, + "comments": 1, + "opened": 0 + }, + { + "w": 1789257600, + "commits": 0, + "comments": 1, + "opened": 0 + }, + { + "w": 1789862400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1790467200, + "commits": 0, + "comments": 0, + "opened": 0 + } + ], + "total": 2 + }, + { + "login": "richardkwo", + "name": "Richard Guo", + "profile_url": "https://github.com/richardkwo", + "homepage_url": "https://unbiased.co.in", + "avatar_url": "https://avatars.githubusercontent.com/u/4409730?v=4", + "commits": 0, + "comments": 2, + "opened": 0, + "weeks": [ + { + "w": 1759622400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760227200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1760832000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1761436800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762041600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1762646400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763251200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1763856000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1764460800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765065600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1765670400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766275200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1766880000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1767484800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768089600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1768694400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769299200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1769904000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1770508800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771113600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1771718400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772323200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1772928000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1773532800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774137600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1774742400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775347200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1775952000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1776556800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777161600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1777766400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778371200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1778976000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1779580800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780185600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1780790400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1781395200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782000000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1782604800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783209600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1783814400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1784419200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785024000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1785628800, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786233600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1786838400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1787443200, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788048000, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1788652800, + "commits": 0, + "comments": 2, + "opened": 0 + }, + { + "w": 1789257600, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1789862400, + "commits": 0, + "comments": 0, + "opened": 0 + }, + { + "w": 1790467200, + "commits": 0, + "comments": 0, + "opened": 0 + } + ], + "total": 2 + } + ] + } +} diff --git a/governance.html b/governance.html index 0e3aec9..38c4be3 100644 --- a/governance.html +++ b/governance.html @@ -5,7 +5,7 @@ Governance — Statlib - + diff --git a/homepage.js b/homepage.js new file mode 100644 index 0000000..db48fc4 --- /dev/null +++ b/homepage.js @@ -0,0 +1,367 @@ +// Renders the cached homepage snapshot. The browser never calls the GitHub API directly. +(function () { + "use strict"; + + const DATA_URL = "data/homepage.json"; + const KINDS = [ + { key: "commits", one: "commit", many: "commits" }, + { key: "comments", one: "comment", many: "comments" }, + { key: "opened", one: "issue/PR opened", many: "issues/PRs opened" }, + ]; + + const el = (tag, attrs = {}, children = []) => { + const node = document.createElement(tag); + for (const [key, value] of Object.entries(attrs)) { + if (key === "text") node.textContent = value; + else node.setAttribute(key, value); + } + for (const child of [].concat(children)) if (child) node.append(child); + return node; + }; + + const svg = (tag, attrs = {}) => { + const node = document.createElementNS("http://www.w3.org/2000/svg", tag); + for (const [key, value] of Object.entries(attrs)) node.setAttribute(key, value); + return node; + }; + + const fmtDate = (seconds) => + new Date(seconds * 1000).toLocaleDateString("en-US", { + month: "short", + day: "numeric", + year: "numeric", + timeZone: "UTC", + }); + const fmtMonth = (seconds) => + new Date(seconds * 1000).toLocaleDateString("en-US", { + month: "short", + timeZone: "UTC", + }); + const fmtUpdated = (value) => + new Date(value).toLocaleDateString("en-US", { + month: "short", + day: "numeric", + year: "numeric", + timeZone: "UTC", + }); + const count = (number, kind) => + `${number.toLocaleString()} ${number === 1 ? kind.one : kind.many}`; + const weekTotal = (week) => + KINDS.reduce((sum, kind) => sum + week[kind.key], 0); + + const tooltip = el("div", { + class: "gh-tooltip", + role: "status", + "aria-live": "polite", + }); + document.body.append(tooltip); + + const showTip = (event, text) => { + tooltip.textContent = text; + tooltip.style.display = "block"; + const box = tooltip.getBoundingClientRect(); + let x = event.clientX + 12; + if (x + box.width > window.innerWidth - 8) { + x = event.clientX - box.width - 12; + } + tooltip.style.left = `${x + window.scrollX}px`; + tooltip.style.top = `${event.clientY + window.scrollY - box.height - 10}px`; + }; + + const hideTip = () => { + tooltip.style.display = "none"; + }; + + function weeklyChart(weeks, yMax, { height, axis, label }) { + const width = 600; + const plotHeight = height - (axis ? 18 : 0); + const slot = width / weeks.length; + const barWidth = Math.max(1, Math.min(slot - 2, slot * 0.6)); + const gap = 2; + const root = svg("svg", { + viewBox: `0 0 ${width} ${height}`, + preserveAspectRatio: "none", + class: "gh-chart", + role: "img", + "aria-label": label, + }); + root.style.height = `${height}px`; + root.append( + svg("line", { + x1: 0, + x2: width, + y1: plotHeight, + y2: plotHeight, + class: "gh-baseline", + }), + ); + + weeks.forEach((week, index) => { + const x = index * slot + (slot - barWidth) / 2; + const present = KINDS.filter((kind) => week[kind.key] > 0); + let base = plotHeight; + present.forEach((kind, kindIndex) => { + const segmentHeight = (week[kind.key] / yMax) * (plotHeight - 4); + const top = base - segmentHeight; + const isTop = kindIndex === present.length - 1; + const radius = isTop ? Math.min(2, barWidth / 2, segmentHeight) : 0; + const bottom = kindIndex === 0 ? base : base - gap / 2; + const segmentTop = isTop ? top : top + gap / 2; + if (bottom - segmentTop > 0.5) { + root.append( + svg("path", { + class: `gh-bar gh-${kind.key}`, + d: `M${x},${bottom}V${segmentTop + radius}Q${x},${segmentTop} ${x + radius},${segmentTop}H${x + barWidth - radius}Q${x + barWidth},${segmentTop} ${x + barWidth},${segmentTop + radius}V${bottom}Z`, + }), + ); + } + base = top; + }); + + const hit = svg("rect", { + x: index * slot, + y: 0, + width: slot, + height: plotHeight, + class: "gh-hit", + }); + const parts = present.map((kind) => count(week[kind.key], kind)); + const text = `Week of ${fmtDate(week.w)}: ${parts.length ? parts.join(", ") : "no activity"}`; + hit.addEventListener("mousemove", (event) => { + hit.classList.add("on"); + showTip(event, text); + }); + hit.addEventListener("mouseleave", () => { + hit.classList.remove("on"); + hideTip(); + }); + root.append(hit); + + if (axis) { + const previous = weeks[index - 1]; + if (!previous || fmtMonth(previous.w) !== fmtMonth(week.w)) { + const textNode = svg("text", { + x, + y: height - 4, + class: "gh-axis", + }); + textNode.textContent = fmtMonth(week.w); + root.append(textNode); + } + } + }); + return root; + } + + function legend() { + return el( + "div", + { class: "gh-legend" }, + KINDS.map((kind) => + el("span", { class: "gh-legend-item" }, [ + el("span", { class: `gh-swatch gh-${kind.key}` }), + kind.many, + ]), + ), + ); + } + + function activityCard(person, rank, grandTotal, yMax) { + const meta = KINDS.filter((kind) => person[kind.key] > 0).map((kind) => + count(person[kind.key], kind), + ); + const share = grandTotal ? (person.total / grandTotal) * 100 : 0; + const shareBar = el( + "div", + { class: "gh-share", title: `${share.toFixed(0)}% of all activity` }, + [el("span", { class: "gh-share-fill" })], + ); + shareBar.firstChild.style.width = `${share}%`; + return el("li", { class: "gh-card" }, [ + el("span", { class: "gh-rank", text: `#${rank}` }), + el("div", { class: "gh-person" }, [ + el("img", { + src: person.avatar_url, + alt: "", + class: "gh-avatar", + loading: "lazy", + }), + el("div", { class: "gh-who" }, [ + el("a", { + href: person.homepage_url, + target: "_blank", + rel: "noopener", + class: "gh-name", + text: person.name, + }), + el("a", { + href: person.profile_url, + target: "_blank", + rel: "noopener", + class: "gh-login", + text: `@${person.login}`, + }), + ]), + el("div", { class: "gh-meta", text: meta.join(" · ") }), + ]), + shareBar, + weeklyChart(person.weeks, yMax, { + height: 56, + axis: false, + label: `Weekly activity by ${person.name}`, + }), + ]); + } + + function renderTodos(data) { + const board = document.getElementById("todo-board"); + if (!board) return; + board.replaceChildren(); + board.setAttribute("aria-busy", "false"); + + if (!data.todos.length) { + board.append(el("p", { class: "data-status", text: "No open statements." })); + return; + } + + const list = el("ol", { class: "todo-list" }); + data.todos.forEach((todo) => { + const actions = [ + el("a", { + href: todo.source_url, + target: "_blank", + rel: "noopener", + text: "View source", + }), + ]; + if (todo.issue_url) { + actions.push( + el("a", { + href: todo.issue_url, + target: "_blank", + rel: "noopener", + text: "Open issue", + }), + ); + } + list.append( + el("li", { class: "todo-item" }, [ + el("div", { class: "todo-title" }, [ + el("h3", {}, [ + el("a", { + href: todo.source_url, + target: "_blank", + rel: "noopener", + text: todo.name, + }), + ]), + el("span", { class: "tag", text: todo.module }), + ]), + el("p", { text: todo.summary }), + el("div", { class: "todo-actions" }, actions), + el("details", { class: "todo-statement" }, [ + el("summary", { text: "Statement" }), + el("code", { text: todo.statement }), + ]), + ]), + ); + }); + board.append( + el("div", { class: "data-summary" }, [ + el("span", { + text: `${data.todos.length} open statement${data.todos.length === 1 ? "" : "s"}`, + }), + el("span", { text: `Updated ${fmtUpdated(data.generated_at)}` }), + ]), + list, + ); + } + + function renderActivity(data) { + const board = document.getElementById("activity-board"); + if (!board) return; + board.replaceChildren(); + board.setAttribute("aria-busy", "false"); + const activity = data.activity; + const rows = activity.people; + if (!rows.length) { + board.append( + el("p", { class: "data-status", text: "No activity in this period." }), + ); + return; + } + + const combined = activity.week_starts.map((week, index) => ({ + w: week, + commits: rows.reduce( + (sum, person) => sum + person.weeks[index].commits, + 0, + ), + comments: rows.reduce( + (sum, person) => sum + person.weeks[index].comments, + 0, + ), + opened: rows.reduce( + (sum, person) => sum + person.weeks[index].opened, + 0, + ), + })); + const combinedMax = Math.max(1, ...combined.map(weekTotal)); + const personMax = Math.max( + 1, + ...rows.flatMap((person) => person.weeks.map(weekTotal)), + ); + const grandTotal = rows.reduce((sum, person) => sum + person.total, 0); + const cards = el("ol", { class: "gh-cards" }); + rows.forEach((person, index) => { + cards.append(activityCard(person, index + 1, grandTotal, personMax)); + }); + + board.append( + el("div", { class: "data-summary" }, [ + el("span", { text: `${activity.window} · ${rows.length} contributors` }), + el("span", { text: `Updated ${fmtUpdated(data.generated_at)}` }), + ]), + el("div", { class: "gh-view" }, [ + el("div", { class: "gh-overview" }, [ + el("div", { class: "gh-overview-head" }, [ + el("div", { class: "gh-overview-title", text: "Activity per week" }), + legend(), + ]), + weeklyChart(combined, combinedMax, { + height: 120, + axis: true, + label: `Weekly activity in ${activity.repository}`, + }), + ]), + cards, + ]), + ); + } + + function showError(boardId) { + const board = document.getElementById(boardId); + if (!board) return; + board.setAttribute("aria-busy", "false"); + board.replaceChildren( + el("p", { + class: "data-status", + text: "The latest snapshot is temporarily unavailable.", + }), + ); + } + + fetch(DATA_URL) + .then((response) => { + if (!response.ok) throw new Error(`snapshot ${response.status}`); + return response.json(); + }) + .then((data) => { + renderTodos(data); + renderActivity(data); + }) + .catch(() => { + showError("todo-board"); + showError("activity-board"); + }); +})(); diff --git a/index.html b/index.html index 06dda3f..ff0d64d 100644 --- a/index.html +++ b/index.html @@ -5,7 +5,7 @@ Statlib - + @@ -24,24 +24,25 @@

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. Please check out our contributors below (activity loaded live from GitHub). Interested in joining us? Check out our Zulip channel here!

+

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…

+
+
-

Community Activity

- +

Community activity

+

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

+
+

Loading community activity…

+
- + diff --git a/roadmap.html b/roadmap.html index a16c5ef..547852a 100644 --- a/roadmap.html +++ b/roadmap.html @@ -5,7 +5,7 @@ Roadmap — Statlib - + diff --git a/site.css b/site.css index c9dc13a..1eabba9 100644 --- a/site.css +++ b/site.css @@ -261,7 +261,7 @@ body.site-page { .site-page .todo-list { list-style: none; - margin: 16px 0 0; + margin: 12px 0 0; padding: 0; } @@ -287,6 +287,11 @@ body.site-page { margin: 0; } +.site-page .todo-title h3 a { + text-decoration-color: #cfcfcf; + text-underline-offset: 3px; +} + .site-page .tag { display: inline-block; border: 1px solid var(--line); @@ -331,10 +336,64 @@ body.site-page { color: var(--text); } +.site-page .todo-statement { + color: var(--muted); + font-family: system-ui, -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif; + font-size: 13px; + margin-top: 9px; +} + +.site-page .todo-statement summary { + cursor: pointer; + text-decoration: underline; + text-decoration-color: #cfcfcf; + text-underline-offset: 2px; +} + +.site-page .todo-statement code { + display: block; + margin-top: 9px; + overflow-x: auto; + padding: 10px 12px; + white-space: pre-wrap; +} + +.site-page .data-board { + min-height: 48px; +} + +.site-page .data-status, +.site-page .data-summary { + color: var(--quiet); + font-family: system-ui, -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif; + font-size: 13px; + line-height: 1.5; +} + +.site-page .data-status { + border: 1px solid var(--line-soft); + margin: 12px 0 0; + padding: 12px 14px; +} + +.site-page .data-summary { + display: flex; + flex-wrap: wrap; + justify-content: space-between; + gap: 4px 20px; + margin: 12px 0 0; +} + .site-page .people { margin-top: 36px; } +.site-page .people > p { + color: #3f3f3f; + font-size: 15px; + margin-bottom: 12px; +} + .site-page .people h2 { color: var(--faint); font-family: system-ui, -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif; diff --git a/tools/build_homepage_data.py b/tools/build_homepage_data.py new file mode 100644 index 0000000..9a78bdd --- /dev/null +++ b/tools/build_homepage_data.py @@ -0,0 +1,334 @@ +#!/usr/bin/env python3 +"""Build the cached data used by the Statlib homepage. + +TODOs are extracted from structured Lean comments. Community activity is fetched only by the +scheduled GitHub Action, never by a visitor's browser. +""" + +from __future__ import annotations + +import argparse +import json +import os +import re +import subprocess +import urllib.error +import urllib.parse +import urllib.request +from collections import defaultdict +from datetime import datetime, timedelta, timezone +from pathlib import Path +from typing import Any + + +ROOT = Path(__file__).resolve().parents[1] +DEFAULT_OUTPUT = ROOT / "data" / "homepage.json" +REPOSITORY = "stat-lib/statlib" +HIDDEN_ACCOUNTS = {"formal-stat"} +PEOPLE = { + "RemyDegenne": ("Rémy Degenne", "https://remydegenne.github.io/"), + "zixiaowang17": ("Zixiao Jolene Wang", "https://zixiaowang17.github.io/"), + "bocowgill": ("Bo Cowgill", "http://bocowgill.com"), + "rajarshi-mukherjee24": ( + "Rajarshi Mukherjee", + "https://rajarshi-mukherjee24.github.io/", + ), + "CoolRmal": ("Yongxi (Aaron) Lin", "https://coolrmal.github.io/"), + "richardkwo": ("Richard Guo", "https://unbiased.co.in"), + "qingyuanzhao": ("Qingyuan Zhao", "http://www.statslab.cam.ac.uk/~qz280/"), + "bjoernkjoshanssen": ( + "Bjørn Kjos-Hanssen", + "http://math.hawaii.edu/wordpress/bjoern/", + ), +} +TODO_BLOCK = re.compile(r"/-\s*TODO(?:\((#\d+)\))?:\s*(.*?)-/", re.DOTALL) +DECLARATION = re.compile( + r"(?m)^\s*(theorem|lemma|def|instance)\s+([A-Za-z0-9_'.]+)" +) + + +def git_output(repo: Path, *args: str) -> str: + process = subprocess.run( + ["git", "-C", str(repo), *args], + check=True, + capture_output=True, + text=True, + ) + return process.stdout.strip() + + +def one_line(text: str) -> str: + return " ".join(text.split()) + + +def extract_todos(statlib_root: Path) -> tuple[str, list[dict[str, Any]]]: + sha = git_output(statlib_root, "rev-parse", "HEAD") + source_root = statlib_root / "Statlib" + if not source_root.is_dir(): + raise ValueError(f"{source_root} does not exist") + + todos: list[dict[str, Any]] = [] + for path in sorted(source_root.rglob("*.lean")): + text = path.read_text(encoding="utf-8") + relative = path.relative_to(statlib_root).as_posix() + module = relative.removesuffix(".lean").replace("/", ".") + for block in TODO_BLOCK.finditer(text): + body = block.group(2).strip() + declaration = DECLARATION.search(body) + if declaration is None: + continue + line = text.count("\n", 0, block.start()) + 1 + description = one_line(body[: declaration.start()].strip()) + statement = one_line(body[declaration.start() :].strip()) + issue = block.group(1) + item = { + "name": declaration.group(2), + "kind": declaration.group(1), + "module": module, + "summary": description, + "statement": statement, + "source_url": ( + f"https://github.com/{REPOSITORY}/blob/{sha}/{relative}#L{line}" + ), + } + if issue: + number = issue.removeprefix("#") + item["issue_url"] = ( + f"https://github.com/{REPOSITORY}/issues/{number}" + ) + todos.append(item) + return sha, todos + + +def github_token() -> str | None: + token = os.environ.get("GH_TOKEN") or os.environ.get("GITHUB_TOKEN") + if token: + return token + try: + process = subprocess.run( + ["gh", "auth", "token"], + check=True, + capture_output=True, + text=True, + ) + except (FileNotFoundError, subprocess.CalledProcessError): + return None + return process.stdout.strip() or None + + +def github_get(path: str, token: str | None) -> tuple[Any, dict[str, str]]: + request = urllib.request.Request( + f"https://api.github.com{path}", + headers={ + "Accept": "application/vnd.github+json", + "User-Agent": "statlib-homepage-data", + **({"Authorization": f"Bearer {token}"} if token else {}), + }, + ) + try: + with urllib.request.urlopen(request, timeout=30) as response: + return json.load(response), dict(response.headers.items()) + except urllib.error.HTTPError as error: + detail = error.read().decode("utf-8", errors="replace") + raise RuntimeError(f"GitHub API returned {error.code}: {detail}") from error + + +def github_pages( + endpoint: str, + token: str | None, + params: dict[str, str], + max_pages: int = 10, +) -> list[dict[str, Any]]: + items: list[dict[str, Any]] = [] + for page in range(1, max_pages + 1): + query = urllib.parse.urlencode({**params, "per_page": "100", "page": str(page)}) + payload, _ = github_get(f"{endpoint}?{query}", token) + if not isinstance(payload, list): + raise RuntimeError(f"Expected a list from {endpoint}") + items.extend(payload) + if len(payload) < 100: + break + return items + + +def week_start(value: datetime) -> int: + value = value.astimezone(timezone.utc) + value = value.replace(hour=0, minute=0, second=0, microsecond=0) + days_since_sunday = (value.weekday() + 1) % 7 + return int((value - timedelta(days=days_since_sunday)).timestamp()) + + +def parse_time(value: str) -> datetime: + return datetime.fromisoformat(value.replace("Z", "+00:00")) + + +def is_person(user: dict[str, Any] | None) -> bool: + if not user or not user.get("login"): + return False + login = user["login"] + return ( + user.get("type") != "Bot" + and not login.endswith("[bot]") + and login not in HIDDEN_ACCOUNTS + ) + + +def build_activity(now: datetime) -> dict[str, Any]: + token = github_token() + current_week = week_start(now) + week_starts = [ + current_week - (51 - index) * 7 * 24 * 3600 for index in range(52) + ] + cutoff = datetime.fromtimestamp(week_starts[0], timezone.utc) + cutoff_iso = cutoff.isoformat().replace("+00:00", "Z") + + commits = github_pages( + f"/repos/{REPOSITORY}/commits", + token, + {"since": cutoff_iso}, + ) + comments = github_pages( + f"/repos/{REPOSITORY}/issues/comments", + token, + {"since": cutoff_iso}, + ) + issues = github_pages( + f"/repos/{REPOSITORY}/issues", + token, + {"state": "all"}, + ) + + index = {value: position for position, value in enumerate(week_starts)} + people: dict[str, dict[str, Any]] = {} + + def row(user: dict[str, Any]) -> dict[str, Any]: + login = user["login"] + if login not in people: + display_name, homepage = PEOPLE.get(login, (login, user["html_url"])) + people[login] = { + "login": login, + "name": display_name, + "profile_url": user["html_url"], + "homepage_url": homepage, + "avatar_url": user["avatar_url"], + "commits": 0, + "comments": 0, + "opened": 0, + "weeks": [ + {"w": value, "commits": 0, "comments": 0, "opened": 0} + for value in week_starts + ], + } + return people[login] + + def add(user: dict[str, Any] | None, kind: str, created_at: str) -> None: + if not is_person(user): + return + position = index.get(week_start(parse_time(created_at))) + if position is None: + return + person = row(user) + person[kind] += 1 + person["weeks"][position][kind] += 1 + + for commit in commits: + created_at = commit.get("commit", {}).get("author", {}).get("date") + if created_at: + add(commit.get("author"), "commits", created_at) + for comment in comments: + add(comment.get("user"), "comments", comment["created_at"]) + for issue in issues: + if parse_time(issue["created_at"]) >= cutoff: + add(issue.get("user"), "opened", issue["created_at"]) + + rows = list(people.values()) + for person in rows: + person["total"] = person["commits"] + person["comments"] + person["opened"] + rows.sort(key=lambda person: (-person["total"], person["login"].lower())) + return { + "repository": REPOSITORY, + "window": "52 weeks", + "week_starts": week_starts, + "people": rows, + } + + +def validate(payload: Any) -> None: + if not isinstance(payload, dict): + raise ValueError("homepage data must be an object") + required = {"generated_at", "statlib_sha", "todos", "activity"} + missing = required.difference(payload) + if missing: + raise ValueError(f"homepage data is missing: {', '.join(sorted(missing))}") + if not isinstance(payload["todos"], list): + raise ValueError("todos must be a list") + for todo in payload["todos"]: + for key in ("name", "kind", "module", "summary", "source_url"): + if not isinstance(todo.get(key), str) or not todo[key]: + raise ValueError(f"invalid TODO field {key}") + activity = payload["activity"] + if not isinstance(activity, dict) or not isinstance(activity.get("people"), list): + raise ValueError("activity.people must be a list") + if len(activity.get("week_starts", [])) != 52: + raise ValueError("activity must contain 52 week starts") + + +def read_existing(path: Path) -> dict[str, Any] | None: + if not path.exists(): + return None + payload = json.loads(path.read_text(encoding="utf-8")) + validate(payload) + return payload + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--statlib-root", type=Path) + parser.add_argument("--output", type=Path, default=DEFAULT_OUTPUT) + parser.add_argument("--refresh-activity", action="store_true") + parser.add_argument("--validate-only", action="store_true") + args = parser.parse_args() + + existing = read_existing(args.output) + if args.validate_only: + if existing is None: + raise ValueError(f"{args.output} does not exist") + return + if args.statlib_root is None: + parser.error("--statlib-root is required unless --validate-only is used") + + statlib_root = args.statlib_root.resolve() + sha, todos = extract_todos(statlib_root) + if args.refresh_activity: + try: + activity = build_activity(datetime.now(timezone.utc)) + except (OSError, RuntimeError, ValueError) as error: + if existing is None: + raise + print(f"Keeping the previous activity snapshot: {error}") + activity = existing["activity"] + elif existing is not None: + activity = existing["activity"] + else: + raise ValueError("an initial activity snapshot requires --refresh-activity") + + content = {"statlib_sha": sha, "todos": todos, "activity": activity} + previous_content = ( + {key: existing[key] for key in content} if existing is not None else None + ) + generated_at = ( + existing["generated_at"] + if previous_content == content + else datetime.now(timezone.utc).replace(microsecond=0).isoformat() + ) + payload = {"generated_at": generated_at, **content} + validate(payload) + args.output.parent.mkdir(parents=True, exist_ok=True) + args.output.write_text( + json.dumps(payload, ensure_ascii=False, indent=2) + "\n", + encoding="utf-8", + ) + + +if __name__ == "__main__": + main() diff --git a/tools/build_site.py b/tools/build_site.py index 6342bf9..9fd4efe 100755 --- a/tools/build_site.py +++ b/tools/build_site.py @@ -228,6 +228,13 @@ def insert_roadmap_toc(self) -> None: self.lines.append("") self.lines.append("") + def insert_data_board(self, board: str, loading_text: str) -> None: + self.lines.append( + f'
' + ) + self.lines.append(f'

{html.escape(loading_text)}

') + self.lines.append("
") + def render(self, body: str) -> str: if self.page_key == "roadmap": self.collect_roadmap_toc(body) @@ -243,6 +250,16 @@ def render(self, body: str) -> str: self.flush_paragraph() self.insert_roadmap_toc() continue + if line.strip() == "[[todo-board]]": + self.close_list() + self.flush_paragraph() + self.insert_data_board("todo-board", "Loading open statements…") + continue + if line.strip() == "[[community-activity]]": + self.close_list() + self.flush_paragraph() + self.insert_data_board("activity-board", "Loading community activity…") + continue heading = re.match(r"^(#{1,6})\s+(.+)$", line) if heading: self.handle_heading(len(heading.group(1)), heading.group(2)) @@ -292,7 +309,7 @@ def render_page(page_key: str, meta: dict[str, str], body_html: str) -> str: head.append(f'') head.extend( [ - '', + '', "", '', "", diff --git a/tools/test_build_homepage_data.py b/tools/test_build_homepage_data.py new file mode 100644 index 0000000..b4eeb99 --- /dev/null +++ b/tools/test_build_homepage_data.py @@ -0,0 +1,45 @@ +from __future__ import annotations + +import tempfile +import unittest +from pathlib import Path +from unittest.mock import patch + +import build_homepage_data + + +class ExtractTodosTest(unittest.TestCase): + def test_extracts_only_structured_todo_declarations(self) -> None: + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + source = root / "Statlib" / "Topic" / "Def.lean" + source.parent.mkdir(parents=True) + source.write_text( + """+/-! +The word TODO in prose is not a task. +-/ + +-- TODO: an ordinary implementation note + +/- TODO(#42): Prove the planned result. +theorem Topic.planned_result (p : Prop) : p → p +-/ +""", + encoding="utf-8", + ) + with patch.object(build_homepage_data, "git_output", return_value="abc123"): + sha, todos = build_homepage_data.extract_todos(root) + + self.assertEqual(sha, "abc123") + self.assertEqual(len(todos), 1) + self.assertEqual(todos[0]["name"], "Topic.planned_result") + self.assertEqual(todos[0]["module"], "Statlib.Topic.Def") + self.assertEqual(todos[0]["summary"], "Prove the planned result.") + self.assertEqual( + todos[0]["issue_url"], + "https://github.com/stat-lib/statlib/issues/42", + ) + + +if __name__ == "__main__": + unittest.main()