This page is the same spec the VeriLib editors load at /dynamic-chart, /dynamic-chart-v2, and /dynamic-chart-v3. Live atoms tables (v4) are on Dynamic chart tables. In the app, fenced chart blocks render as charts. Here they are copy-pasteable JSON.

Documentation source of truth: verilib-frontend (private) — docs/dynamic-chart.md and docs/dynamic-chart-v4.md.

Dynamic chart pages¶

A chart page is one markdown document. Headings and paragraphs are the page. Each chart is a JSON object inside a fenced chart block. Edit (top right) changes copy or JSON; Reset restores this sample. Saves in this browser only (localStorage), not MySQL.

/dynamic-chart, /dynamic-chart-v2, and /dynamic-chart-v3 load this catalog (separate drafts). /dynamic-chart-v4 is a second seed: live atoms tables (GROUP BY chapter / kind). See dynamic-chart-v4.md.

How a chart gets its numbers¶

Time, line, and stacked charts draw four slots: completed, inProgress, unspecified, total. Labels, colours, and line style are yours. What number goes in each slot depends on source. "type": "table" is a count grid instead (see atoms below).

Page markdown
  └── fenced chart JSON
        ├── type / width / series / legend / x   (how it looks)
        └── source.kind
              ├── inline      → points you typed in "data"
              ├── repostats   → VeriLib DB (repostats snapshots)
              ├── url         → public HTTPS JSON file
              └── atoms       → live GROUP BY on the atoms table (type: table)

`source.kind`	Where the points come from	You must be
omitted or `inline`	The `data` array in the JSON	—
`repostats`	MySQL table `repostats` via `GET /repobrowser/progress_chart_data` (same snapshots as SignalShotV2)	logged in
`url`	`GET` a public `https://…` JSON file (GitHub Pages is CORS `*`)	—
`atoms`	Live counts from MySQL `atoms` via `GET /repobrowser/atom_group_data` (GROUP BY folder or `statement_type`)	logged in

repostats does not run SQL you write. It reads probe snapshots already stored as rows. Lean / leanblueprint also stuffed extra counters into raw_record (JSON blob). atomType and metrics remap that blob onto the four slots.

atoms is a constrained GROUP BY (chapter from code_path, or statement_type) — not arbitrary SQL, and not Verso blueprint nodes (those are not ingested yet). Use "type": "table" with that source. Live examples: /dynamic-chart-v4.

If a live fetch fails and you also included data, the chart shows data as fallback.

Write a chart block¶

Fence language is chart or charts. Body must be one JSON object, not an array. Consecutive charts that share the same "row" string sit on one grid.

Do not put a chart fence in a how-to snippet — the editor treats every chart fence as a real chart. Show the grammar as JSON:

{
  "id": "a",
  "row": "top",
  "width": "1/2",
  "type": "line",
  "data": [
    { "capturedAt": "2026-01-01", "completed": 4, "inProgress": 2 }
  ]
}

A second card on the same row uses the same "row" and "width": "1/2", with "source": { "kind": "repostats", "repos": ["verilibUser/repo-slug"] } instead of data.

Click a legend item in the app to hide or show that series.

Options (all of them)¶

Page / card¶

Field	Required	Values	Default	What it does
`id`	no	string, unique on the page	`chart-{type}`	Stable key for live fetches
`type`	yes	`stacked-time` \| `line` \| `stacked-bar` \| `table`	—	`stacked-bars` is accepted as `stacked-bar`. `table` is a grouped count grid, not a plot
`title`	no	string	none	Card heading
`row`	no	string	none	Same value → same grid row
`width`	no	`full` \| `1/2` \| `1/3`	`full`	Column span (6 / 3 / 2 of a 6-col grid)
`height`	no	number (px)	`280`	Plot height
`x`	no	`{ "type": "time" \\| "index" \\| "category", "field": "…" }`	`{ "type": "time", "field": "capturedAt" }`	`category` is treated as `index`. `field` names the date or label column
`y`	no	`{ "type": "linear" }`	linear	Only linear
`legend`	no	`{ "show": true \\| false, "position": "bottom" \\| "right" }`	show true, position bottom	`show: false` hides it
`series`	no	array of series objects	all four keys, default colours	Omit a `key` to hide that series. Unused on `table`
`columns`	no	array of table column objects	Verso-like Defs/Theorems counts	`type: table` only
`source`	no	object, see below	`{ "kind": "inline" }`	Where points / table buckets come from
`data`	yes if inline	non-empty array of points or table rows	`[]`	Hardcoded points; optional fallback for live sources

Series object¶

Field	Required	Values	Default
`key`	yes	`completed` \| `inProgress` \| `unspecified` \| `total`	—
`label`	no	legend text	Completed / In-Progress / Unspecified / Total
`color`	no	CSS colour	`#01BB00` / `#E8BA00` / `#E4E4E4` / `#888899`
`dashed`	no	boolean	`true` for `total`
`filled`	no	boolean	`true` for `completed`

key aliases (so blueprint JSON can use its own names):

You may write	Slot it becomes
`completed`, `verified`, `verified_trusted`, `definitionsVerified`	`completed`
`inProgress`, `in_progress`, `specifiedOnly`, `theoremsVerified`	`inProgress`
`unspecified`	`unspecified`
`total`, `tracked`	`total`

Data point fields¶

Each point is a JSON object. Dates may be 2026-01-01 or 2026-01-01T00:00:00.

Slot	Accepted keys on the point
completed	`completed`, `verified_trusted`, `verified`
inProgress	`inProgress`, `in_progress`, `specifiedOnly`
unspecified	`unspecified`
total	`tracked`, `total` (else sum of the three buckets + `failed`)
date	`x.field` if set, else `capturedAt`, `dateStr`, or `date`
bar label	`chapter` or `label` (tooltip / category tick)

Optional extras stored but not required: verified, translated, failed.

`source` — inline (hardcoded JSON)¶

"source": { "kind": "inline" }

Or omit source. data must be a non-empty array.

`source` — repostats (VeriLib DB)¶

"source": {
  "kind": "repostats",
  "repos": ["verilibUser/repo-slug"],
  "aggregate": "sum",
  "pipeline": "leanblueprint",
  "atomType": "all",
  "metrics": { "completed": "thm_total", "inProgress": "def_total", "unspecified": "0", "total": "thm_total+def_total" }
}

Field	Required	Values	Notes
`kind`	yes	`repostats`
`repos`	yes	non-empty array	`"username/slug"` from `/r/{username}/{slug}` or numeric repo id. Not the GitHub owner. Username match is case-insensitive
`aggregate`	no	`sum` (default) \| `latest`	`sum` merges several repos by calendar date (forward-fill). `latest` uses the first repo only
`pipeline`	no	string	Keep snapshots whose `pipeline` column equals this (`leanblueprint`, `lean`)
`atomType`	no	`all` (default) \| `def` \| `thm`	Project definition/theorem counters from `raw_record` onto the four slots
`metrics`	no	object of four expressions	Override what each slot reads. `+` sums fields. `"0"` is the constant zero

Default metrics for atomType:

`atomType`	completed	inProgress	unspecified	total
`all`	`verified_trusted`	`in_progress`	`unspecified`	`tracked`
`def`	`def_verified+def_trusted`	`def_in_progress`	`def_unrealized`	`def_total`
`thm`	`thm_verified+thm_trusted`	`thm_in_progress`	`thm_unrealized`	`thm_total`

Lookup is top-level JSON field first, then raw_record. Aliases: bp_def_* (leanblueprint) and lean_def_* / lean_thm_sorry (bare Lean). Type splits are 0 when raw_record was never written.

Named fields understood in metrics expressions (19): verified_trusted, in_progress, unspecified, tracked, verified, translated, failed, def_verified, def_trusted, def_in_progress, def_unrealized, def_failed, def_total, thm_verified, thm_trusted, thm_in_progress, thm_unrealized, thm_failed, thm_total. Each also accepts bp_* and lean_* aliases where probes wrote them.

DB path (what the browser actually calls):

GET /v2/repo/resolve/{username}/{slug} (or /v2/repo/resolve/id/{id}) → users + repos → numeric repo_id
GET /repobrowser/progress_chart_data?repo_id= → SELECT … FROM repostats WHERE repo_id = ? (non-empty status columns), including raw_record
Browser: optional pipeline filter → optional atomType / metrics projection → optional date merge (sum) → four series slots

`source` — url (external JSON)¶

"source": {
  "kind": "url",
  "url": "https://example.github.io/blueprint-progress-history.json",
  "format": "blueprint-progress-history",
  "metrics": { "completed": "definitionsVerified", "inProgress": "theoremsVerified", "unspecified": "0", "total": "total" }
}

Field	Required	Notes
`kind`	yes	`url`
`url`	yes	Must be `https://…`
`format`	no	`blueprint-progress-history` flattens `snapshots[].definitions` / `theorems` into the four slots plus `definitionsVerified` / `theoremsVerified`
`metrics`	no	Same expression language as repostats

Accepted URL JSON shapes:

blueprint-progress-history (with format): { "snapshots": [ { "date", "definitions": { "total", "specified", "verified" }, "theorems": { … } } ] } — flattened to verified / specifiedOnly / total per snapshot.
Point array (no format): [ { "capturedAt"|"dateStr"|"date", "completed"|"verified_trusted", "inProgress"|"in_progress", "unspecified", "total"|"tracked" } ].

Default metrics for blueprint history: completed=verified, inProgress=specifiedOnly, unspecified=unspecified, total=total.

Without that format, the URL body must be an array of points (same shape as inline data).

`source` — atoms (live `GROUP BY`)¶

"source": {
  "kind": "atoms",
  "repos": ["verilibUser/repo-slug"],
  "groupBy": "chapter",
  "pathDepth": 2,
  "columns": [
    { "key": "def_total", "group": "Definitions", "label": "Total", "kinds": ["def", "structure", "abbrev", "inductive", "instance"] },
    { "key": "thm_total", "group": "Theorems", "label": "Total", "kinds": ["theorem"] },
    { "key": "thm_verified", "group": "Theorems", "label": "Verified", "kinds": ["theorem"], "status": ["verified", "transitively-verified"] }
  ]
}

Use with "type": "table". GET /repobrowser/atom_group_data returns count buckets; the browser maps them onto columns. No user SQL.

Field	Required	Values	Notes
`kind`	yes	`atoms`
`repos`	yes	non-empty array	Same `"username/slug"` or id as repostats
`groupBy`	no	`chapter` (default) \| `statement_type`	chapter — row label = Nth segment of `code_path` (`pathDepth`, default 2). statement_type — row label = Lean kind (`def`, `theorem`, …). Not Verso blueprint/paper nodes.
`pathDepth`	no	1–4	Default 2 (`KVAC/Core/file.lean` → Core)
`columns`	no	array	See below. Defaults: Definitions/Theorems totals + specified + verified

Table column object

Field	What it does
`key`	Cell field name
`group`	Optional top header (Definitions / Theorems)
`label`	Column title
`kinds`	Keep these `statement_type` values. Omit = all kinds
`specified`	`true` / `false` / omit
`status`	Any of `verified`, `transitively-verified`, `trusted`, `unverified`, `failed`

This is not Verso’s paper-node table. Blueprint node atoms (language: "blueprint") and Ready next are not in MySQL. Full worked page: /dynamic-chart-v4 and dynamic-chart-v4.md. Live tables show statement_type values in this repo under the grid (expand “Live data source”).

Interactive keyword spec: /assets/docs/dynamic-chart-spec.html (also embedded on /pages). Hover/click coloured tokens for columns[].key, repostats field list, and URL schemas.

What this editor does not do¶

Arbitrary SQL (only groupBy chapter / statement_type on atoms)
Verso “Ready next” or chapters with no Lean files
Saving the markdown in MySQL (browser localStorage only)
Non-linear Y axes, extra series keys, or http:// URLs

1. Hardcoded JSON — layout, types, series¶

Two charts, one row. Left is stacked-time with verified_trusted aliases. Right is line with x.type: index, custom labels/colours, and only three series (unspecified omitted).

{
  "id": "inline-stacked",
  "row": "inline-types",
  "width": "1/2",
  "type": "stacked-time",
  "title": "stacked-time (inline)",
  "height": 240,
  "x": { "type": "time", "field": "capturedAt" },
  "y": { "type": "linear" },
  "legend": { "show": true, "position": "bottom" },
  "series": [
    { "key": "completed", "label": "Completed", "color": "#01BB00", "filled": true },
    { "key": "inProgress", "label": "In-Progress", "color": "#E8BA00" },
    { "key": "unspecified", "label": "Unspecified", "color": "#E4E4E4" },
    { "key": "total", "label": "Total", "color": "#888899", "dashed": true }
  ],
  "source": { "kind": "inline" },
  "data": [
    { "capturedAt": "2026-01-01T00:00:00", "verified_trusted": 10, "in_progress": 4, "unspecified": 2 },
    { "capturedAt": "2026-04-01T00:00:00", "verified_trusted": 18, "in_progress": 3, "unspecified": 1 },
    { "capturedAt": "2026-07-01T00:00:00", "verified_trusted": 24, "in_progress": 2, "unspecified": 1 }
  ]
}

{
  "id": "inline-line",
  "row": "inline-types",
  "width": "1/2",
  "type": "line",
  "title": "line + custom series (inline)",
  "height": 240,
  "x": { "type": "index", "field": "capturedAt" },
  "legend": { "show": true, "position": "bottom" },
  "series": [
    { "key": "completed", "label": "Done", "color": "#217ef0", "filled": true },
    { "key": "inProgress", "label": "WIP", "color": "#e8833a" },
    { "key": "total", "label": "Ceiling", "color": "#646566", "dashed": true }
  ],
  "data": [
    { "capturedAt": "2026-01-15", "completed": 4, "in_progress": 8, "unspecified": 6 },
    { "capturedAt": "2026-03-15", "completed": 9, "in_progress": 6, "unspecified": 4 },
    { "capturedAt": "2026-06-15", "completed": 14, "in_progress": 5, "unspecified": 2 }
  ]
}

Stacked bars, legend on the right, no total¶

type: "stacked-bar" (alias stacked-bars). x.type: "index" uses snapshot order. legend.position: "right".

{
  "id": "inline-bars",
  "type": "stacked-bar",
  "title": "stacked-bar, legend right",
  "width": "full",
  "height": 240,
  "x": { "type": "index" },
  "legend": { "show": true, "position": "right" },
  "series": [
    { "key": "completed", "label": "Completed", "color": "#01BB00" },
    { "key": "inProgress", "label": "In-Progress", "color": "#E8BA00" },
    { "key": "unspecified", "label": "Unspecified", "color": "#E4E4E4" }
  ],
  "data": [
    { "dateStr": "2026-02-01", "verified_trusted": 6, "in_progress": 5, "unspecified": 4 },
    { "dateStr": "2026-05-01", "verified_trusted": 12, "in_progress": 4, "unspecified": 3 },
    { "dateStr": "2026-08-01", "verified_trusted": 20, "in_progress": 2, "unspecified": 1 }
  ]
}

Width 1/3, shorter plot, legend off¶

Three cards on one row. height: 180, legend.show: false.

{
  "id": "third-a",
  "row": "thirds",
  "width": "1/3",
  "type": "line",
  "title": "width 1/3",
  "height": 180,
  "legend": { "show": false },
  "series": [
    { "key": "completed", "color": "#01BB00", "filled": true }
  ],
  "data": [
    { "capturedAt": "2026-01-01", "completed": 3 },
    { "capturedAt": "2026-06-01", "completed": 9 }
  ]
}

{
  "id": "third-b",
  "row": "thirds",
  "width": "1/3",
  "type": "line",
  "title": "second third",
  "height": 180,
  "legend": { "show": false },
  "series": [
    { "key": "inProgress", "color": "#E8BA00", "filled": true }
  ],
  "data": [
    { "capturedAt": "2026-01-01", "inProgress": 8 },
    { "capturedAt": "2026-06-01", "inProgress": 4 }
  ]
}

{
  "id": "third-c",
  "row": "thirds",
  "width": "1/3",
  "type": "line",
  "title": "third third",
  "height": 180,
  "legend": { "show": false },
  "series": [
    { "key": "total", "color": "#888899", "dashed": true }
  ],
  "data": [
    { "capturedAt": "2026-01-01", "total": 11 },
    { "capturedAt": "2026-06-01", "total": 13 }
  ]
}

Category bars (chapter / label)¶

x.type: "category" plus a chapter string on each point. Data is still hardcoded — a history JSON file has no chapter breakdown.

{
  "id": "by-chapter",
  "type": "stacked-bars",
  "title": "Atoms by chapter (inline categories)",
  "width": "full",
  "height": 300,
  "x": { "type": "category", "field": "chapter" },
  "legend": { "show": true, "position": "right" },
  "series": [
    { "key": "verified", "label": "Verified", "color": "#16a34a" },
    { "key": "specifiedOnly", "label": "Specified only", "color": "#2563eb" },
    { "key": "unspecified", "label": "Unspecified", "color": "#E4E4E4" }
  ],
  "data": [
    { "chapter": "Secure Messaging", "verified": 0, "specifiedOnly": 0, "unspecified": 27, "total": 27 },
    { "chapter": "Ratcheting Key Encapsulation Mechanism", "verified": 0, "specifiedOnly": 0, "unspecified": 23, "total": 23 },
    { "chapter": "Sparse Continuous Key Agreement", "verified": 5, "specifiedOnly": 0, "unspecified": 8, "total": 13 },
    { "chapter": "Continuous Key Agreement", "verified": 9, "specifiedOnly": 0, "unspecified": 3, "total": 12 },
    { "chapter": "Key Encapsulation Mechanism", "verified": 10, "specifiedOnly": 0, "unspecified": 1, "total": 11 },
    { "chapter": "Authenticated Encryption with Associated Data", "verified": 8, "specifiedOnly": 0, "unspecified": 1, "total": 9 },
    { "chapter": "Erasure Codes", "verified": 6, "specifiedOnly": 0, "unspecified": 0, "total": 6 }
  ]
}

2. Database — `source.kind: "repostats"`¶

Uses VeriLib username steven460191 and slug secure-messaging-2 (the path in /r/…, not GitHub owner/repo). pipeline: "leanblueprint" drops other snapshot kinds. You must be logged in.

Whole-repo status (SignalShot buckets)¶

atomType: "all" reads the lossy columns: verified_trusted, in_progress, unspecified, tracked.

{
  "id": "db-all-status",
  "type": "stacked-time",
  "title": "DB — all types, status columns",
  "width": "full",
  "height": 260,
  "x": { "type": "time", "field": "capturedAt" },
  "legend": { "show": true, "position": "bottom" },
  "series": [
    { "key": "completed", "label": "Completed", "color": "#01BB00", "filled": true },
    { "key": "inProgress", "label": "In-Progress", "color": "#E8BA00" },
    { "key": "unspecified", "label": "Unspecified", "color": "#E4E4E4" },
    { "key": "total", "label": "Total", "color": "#888899", "dashed": true }
  ],
  "source": {
    "kind": "repostats",
    "repos": ["steven460191/secure-messaging-2"],
    "aggregate": "sum",
    "pipeline": "leanblueprint",
    "atomType": "all"
  }
}

Definitions vs theorems (status of each type)¶

atomType: "def" / "thm" remap raw_record counters (bp_def_*, bp_thm_*) onto the same four slots.

{
  "id": "db-thm-status",
  "row": "db-types",
  "width": "1/2",
  "type": "stacked-time",
  "title": "DB — theorems only (atomType thm)",
  "height": 240,
  "x": { "type": "time", "field": "capturedAt" },
  "legend": { "show": true, "position": "bottom" },
  "series": [
    { "key": "completed", "label": "Completed", "color": "#01BB00", "filled": true },
    { "key": "inProgress", "label": "In-Progress", "color": "#E8BA00" },
    { "key": "unspecified", "label": "Unspecified", "color": "#E4E4E4" },
    { "key": "total", "label": "Total", "color": "#888899", "dashed": true }
  ],
  "source": {
    "kind": "repostats",
    "repos": ["steven460191/secure-messaging-2"],
    "aggregate": "sum",
    "pipeline": "leanblueprint",
    "atomType": "thm"
  }
}

{
  "id": "db-def-status",
  "row": "db-types",
  "width": "1/2",
  "type": "stacked-time",
  "title": "DB — definitions only (atomType def)",
  "height": 240,
  "x": { "type": "time", "field": "capturedAt" },
  "legend": { "show": true, "position": "bottom" },
  "series": [
    { "key": "completed", "label": "Completed", "color": "#217ef0", "filled": true },
    { "key": "inProgress", "label": "In-Progress", "color": "#e8833a" },
    { "key": "unspecified", "label": "Unspecified", "color": "#E4E4E4" },
    { "key": "total", "label": "Total", "color": "#888899", "dashed": true }
  ],
  "source": {
    "kind": "repostats",
    "repos": ["steven460191/secure-messaging-2"],
    "aggregate": "sum",
    "pipeline": "leanblueprint",
    "atomType": "def"
  }
}

Custom metrics (reuse slots as “theorems vs definitions”)¶

The four keys stay completed / inProgress / total. metrics points them at counts by atom type. Legend labels are just text.

{
  "id": "db-type-split",
  "type": "line",
  "title": "DB — metrics: thm_total vs def_total",
  "width": "full",
  "height": 260,
  "x": { "type": "time", "field": "capturedAt" },
  "legend": { "show": true, "position": "bottom" },
  "series": [
    { "key": "completed", "label": "Theorems", "color": "#01BB00", "filled": true },
    { "key": "inProgress", "label": "Definitions", "color": "#217ef0" },
    { "key": "total", "label": "Both", "color": "#888899", "dashed": true }
  ],
  "source": {
    "kind": "repostats",
    "repos": ["steven460191/secure-messaging-2"],
    "aggregate": "sum",
    "pipeline": "leanblueprint",
    "metrics": {
      "completed": "thm_total",
      "inProgress": "def_total",
      "unspecified": "0",
      "total": "thm_total+def_total"
    }
  }
}

`aggregate: "latest"` and inline fallback¶

latest uses only the first repo (no date merge). data is ignored while the live fetch succeeds; it is the backup if resolve/fetch fails.

{
  "id": "db-latest-fallback",
  "type": "line",
  "title": "DB — aggregate latest + fallback data",
  "width": "full",
  "height": 220,
  "x": { "type": "time", "field": "capturedAt" },
  "legend": { "show": true, "position": "bottom" },
  "series": [
    { "key": "completed", "label": "Completed", "color": "#01BB00", "filled": true },
    { "key": "total", "label": "Total", "color": "#888899", "dashed": true }
  ],
  "source": {
    "kind": "repostats",
    "repos": ["steven460191/secure-messaging-2"],
    "aggregate": "latest",
    "pipeline": "leanblueprint"
  },
  "data": [
    { "capturedAt": "2026-01-01", "completed": 0, "total": 0 }
  ]
}

Numeric id is equivalent to a slug: "repos": [5309]. Several slugs with "aggregate": "sum" add matching calendar dates, same as SignalShotV2 with multiple repos in one panel.

3. External JSON — `source.kind: "url"`¶

Fetches blueprint-progress-history.json. format: "blueprint-progress-history" flattens each snapshot’s definitions / theorems buckets. No login.

{
  "id": "url-atoms",
  "row": "url-row",
  "width": "1/2",
  "type": "stacked-time",
  "title": "URL — blueprint atoms over time",
  "height": 260,
  "x": { "type": "time", "field": "capturedAt" },
  "legend": { "show": true, "position": "bottom" },
  "series": [
    { "key": "verified", "label": "Verified", "color": "#16a34a", "filled": true },
    { "key": "specifiedOnly", "label": "Specified only", "color": "#2563eb", "filled": true },
    { "key": "unspecified", "label": "Unspecified", "color": "#E4E4E4", "filled": true },
    { "key": "total", "label": "Total", "color": "#5b6474", "dashed": true }
  ],
  "source": {
    "kind": "url",
    "url": "https://beneficial-ai-foundation.github.io/secure-messaging/blueprint-progress-history.json",
    "format": "blueprint-progress-history"
  }
}

{
  "id": "url-def-thm",
  "row": "url-row",
  "width": "1/2",
  "type": "line",
  "title": "URL — metrics: definitions vs theorems verified",
  "height": 260,
  "x": { "type": "time", "field": "capturedAt" },
  "legend": { "show": true, "position": "bottom" },
  "series": [
    { "key": "definitionsVerified", "label": "Definitions", "color": "#2563eb", "filled": true },
    { "key": "theoremsVerified", "label": "Theorems", "color": "#16a34a" },
    { "key": "total", "label": "Total atoms", "color": "#5b6474", "dashed": true }
  ],
  "source": {
    "kind": "url",
    "url": "https://beneficial-ai-foundation.github.io/secure-messaging/blueprint-progress-history.json",
    "format": "blueprint-progress-history",
    "metrics": {
      "completed": "definitionsVerified",
      "inProgress": "theoremsVerified",
      "unspecified": "0",
      "total": "total"
    }
  }
}

4. Mix sources on one row¶

Hardcoded left, database right, same row.

{
  "id": "mix-inline",
  "row": "mix",
  "width": "1/2",
  "type": "line",
  "title": "Inline demo",
  "height": 240,
  "series": [
    { "key": "completed", "color": "#217ef0", "filled": true },
    { "key": "inProgress", "color": "#e8833a" }
  ],
  "data": [
    { "capturedAt": "2026-01-15", "completed": 4, "in_progress": 8 },
    { "capturedAt": "2026-06-15", "completed": 14, "in_progress": 5 }
  ]
}

{
  "id": "mix-live",
  "row": "mix",
  "width": "1/2",
  "type": "stacked-time",
  "title": "Same row, live DB",
  "height": 240,
  "source": {
    "kind": "repostats",
    "repos": ["steven460191/secure-messaging-2"],
    "aggregate": "sum",
    "pipeline": "leanblueprint"
  }
}

Prompt for another editor / LLM¶

You produce a VeriLib dynamic-chart markdown page (wiki prose + fenced chart JSON).

Rules:
- One markdown document. First heading is the page title.
- Charts live in fenced blocks with language chart. Body is one JSON object, not an array.
- type is stacked-time, line, stacked-bar (stacked-bars alias), or table.
- Time/line/bar series keys are only completed, inProgress, unspecified, total (aliases: verified, verified_trusted, definitionsVerified, specifiedOnly, in_progress, theoremsVerified, tracked).
- Layout: consecutive charts that should sit side by side share the same "row" string and use width 1/2 or 1/3.
- Hardcoded: omit source (or kind inline) and put points in data.
- Database snapshots: "source": { "kind": "repostats", "repos": ["VeriLibUser/slug" or numeric id], "aggregate": "sum" }. Optional pipeline, atomType (all|def|thm), metrics (field+field). data is optional fallback.
- Live atom counts: "type": "table", "source": { "kind": "atoms", "repos": ["VeriLibUser/slug"], "groupBy": "chapter"|"statement_type", "pathDepth": 2 }. Optional columns with kinds / specified / status.
- Public JSON: "source": { "kind": "url", "url": "https://...", "format": "blueprint-progress-history" }.
- Use /r/{username}/{slug} usernames, not GitHub owner/repo.
- Output only the markdown page. No commentary.