This page is the same spec the VeriLib editors load at /dynamic-chart, /dynamic-chart-v2, and /dynamic-chart-v3, and the Markdown format of user pages at /pages and /p/{username}/{slug}. Besides chart, a page can use eight more block types, including latex and the live extract store (VQ) blocks. 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.

Page blocks (/pages)

A page is Markdown. Prose renders as normal Markdown (headings, lists, links, images, tables). A fenced block whose language is one of the labels below becomes a component. Anything else stays a code block. The first # H1 is the page title in the file; the preview hides it.

Fence	What it renders	Body	Data
chart / charts	Line, stacked time, stacked bar, or count table	One JSON object (options)	inline, repostats, url, atoms, or vq
cards	Grid of repository progress cards	{ "repos": ["owner/slug"], "variant": "green" }	Live, signed-in viewer
stats	Up to 8 headline tiles	{ "items": [{ "value", "label", "hint" }] }	Static text you type
signalshot	Verification Progress chart plus named repo cards	{ "title", "variant", "items": [{ "id", "name", "description", "repo", "githubUrl" }] }	Live when an item has repo
latex	A formula rendered with KaTeX	Bare LaTeX, or { "tex": "...", "displayMode": true }	Static
pdf	An embedded PDF in an iframe	One http(s) URL as the whole body	URL
vqstats	Live headline tiles from the latest stored snapshot	JSON, see VQ blocks	Extract store
vqextracts	Table of the newest stored snapshots	JSON	Extract store
vqatoms	Paged, searchable list of atoms	JSON	Extract store

latex

Static math, rendered with KaTeX. A bare body is display math. Use the JSON form for inline math.

```latex
\mathrm{progress} = \frac{\text{verified} + \text{trusted}}{\text{tracked}}
```

```latex
{ "tex": "x^2 + y^2 = r^2", "displayMode": false }
```

An empty body, invalid JSON, or an empty tex shows an inline error box instead of breaking the page.

stats, cards, signalshot, pdf

{ "items": [ { "value": "12", "label": "Tracked items", "hint": "Entered by hand" } ] }

stats never calls an API: tiles show the strings you write. Use vqstats when the numbers should follow a repository. cards.repos and signalshot.items[].repo use the VeriLib owner/slug from /r/{username}/{slug}, not the GitHub name.

Extract store (VQ) blocks

Three blocks and one chart source read the GraphQL extract store (Hasura on VQD/VQS/VQP). The browser never talks to Hasura. It calls the site's own POST /api/vq route, which:

1. validates the request against an allow-list of operations (latest, history, extracts, breakdown, atoms) and clamps limits;
2. asks the PHP API whether the viewer may see the repository (GET /v2/repo/repobrowser/{repoId}/check-status with the viewer's cookies, which enforces the VIEWER role: public repo, owner, shared user, or admin);
3. only then queries Hasura with a server-side API key (VQ_GRAPHQL_API_KEY), and returns trimmed rows. The S3 location of a snapshot is never returned.

A published page therefore shows VQ blocks to anyone who may see the repository, and shows an error box to everyone else. Every VQ block takes repo as VeriLib owner/slug or a numeric repo id, and an optional pipeline (lean, leanblueprint, verus, aeneas) to read only snapshots from that probe.

vqstats

Live tiles from the latest snapshot of one repository.

{
  "repo": "username/repo-slug",
  "pipeline": "leanblueprint",
  "title": "Latest snapshot",
  "tiles": ["tracked", "completed", "percent_complete", "in_progress", "unspecified"]
}

Field	Required	Notes
repo	yes	owner/slug or numeric id
pipeline	no	Only read this probe's snapshots
tiles	no	1–8 of tracked, completed, percent_complete, verified, in_progress, unspecified, failed, translated, atoms, snapshots, captured, commit, pipeline. Default: tracked, completed, percent_complete, in_progress, unspecified
title	no	Up to 200 characters

completed = verified + trusted. in_progress = specified-but-unfinished + failed, the same partition as the progress chart.

vqextracts

Table of the newest snapshots (capture time, pipeline, commit, tracked, completed, in progress, unspecified, mini progress bar).

{ "repo": "username/repo-slug", "title": "Recent probe runs", "limit": 8 }

limit is 1–50 (default 8), newest first.

vqatoms

Paged list of atoms in the latest snapshot: code path, kind (statement_type), verification status, specified. Readers can search by code path. Untracked atoms are excluded.

{
  "repo": "username/repo-slug",
  "title": "Unfinished theorems",
  "kind": ["theorem"],
  "status": ["unverified", "failed"],
  "pageSize": 20
}

Field	Required	Notes
kind	no	Up to 8 statement_type values (theorem, def, structure, …)
status	no	Up to 8 of verified, transitively-verified, trusted, unverified, failed
search	no	Initial case-insensitive code-path filter
searchable	no	false hides the search box
pageSize	no	5–100, default 15

---

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)
              └── vq          → stored snapshots in the GraphQL extract store (VQD/VQS/VQP)

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
vq	Historical snapshots (line/stacked) or a grouped breakdown of the latest snapshot (table) from the GraphQL extract store, through POST /api/vq	may view the repo

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):

1. GET /v2/repo/resolve/{username}/{slug} (or /v2/repo/resolve/id/{id}) → users + repos → numeric repo_id
2. GET /repobrowser/progress_chart_data?repo_id= → SELECT … FROM repostats WHERE repo_id = ? (non-empty status columns), including raw_record
3. 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:

1. blueprint-progress-history (with format): { "snapshots": [ { "date", "definitions": { "total", "specified", "verified" }, "theorems": { … } } ] } — flattened to verified / specifiedOnly / total per snapshot.
2. 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: expand How to use chart & cards blocks on /pages (sign-in required). Source: public/assets/docs/dynamic-chart-spec.html in verilib-frontend (served from the PHP stack on VD, not through the public nginx → Next route). Hover/click coloured tokens for columns[].key, repostats field list, and URL schemas.

source — vq (extract store)

Stored probe snapshots instead of the MySQL repostats table. Same four slots, same atomType / metrics projection, so a repostats chart can be switched to vq by changing kind.

"source": {
  "kind": "vq",
  "repos": ["verilibUser/repo-slug"],
  "aggregate": "sum",
  "pipeline": "leanblueprint",
  "limit": 200
}

For "type": "table" the latest snapshot's atoms are grouped on the server:

"source": {
  "kind": "vq",
  "repos": ["verilibUser/repo-slug"],
  "groupBy": "statement_type",
  "columns": ["total", "completed", "in_progress", "unspecified"]
}

Field	Required	Values	Notes
kind	yes	vq
repos	yes	non-empty array	"username/slug" or numeric id. Rows are summed across repos
aggregate	no	sum (default) | latest	Time series only. latest uses the first repo
pipeline	no	lean, leanblueprint, verus, aeneas	Only snapshots from this probe
limit	no	1–500	Newest N snapshots per repo. Default 200
atomType, metrics	no	as repostats	Applied to each snapshot's counters
groupBy	no	statement_type (default) | verification_status | language | chapter	Table only
pathDepth	no	1–6	Table with chapter: which code_path segment is the row (.lean stripped)
columns	no	total, verified, trusted, completed, in_progress, unspecified, failed	Table only. Default total, completed, in_progress, unspecified

Unlike atoms, columns here are plain bucket names, not filters. Buckets follow the progress chart: completed = verified (incl. transitively-verified) + trusted; failed; in_progress = specified and not completed/failed; unspecified = the rest. Untracked atoms are excluded. As with repostats, inline data is a fallback when the live fetch fails.

What this editor does not do

• Arbitrary SQL or GraphQL (atoms and vq expose fixed groupings; there is no free-form query)
• 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.
- Other allowed fences: cards ({"repos":["user/slug"]}), stats ({"items":[{"value","label","hint"}]}, hand-typed numbers), signalshot, latex (bare LaTeX or {"tex","displayMode"}), pdf (one URL), and the live extract-store blocks vqstats, vqextracts, vqatoms. No other fence names.
- vqstats: {"repo":"user/slug","pipeline":"lean","tiles":["tracked","completed","percent_complete","in_progress","unspecified"]}. vqextracts: {"repo":"user/slug","limit":8}. vqatoms: {"repo":"user/slug","kind":["theorem"],"status":["unverified"],"pageSize":15}.
- 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" }.
- Stored snapshots: "source": { "kind": "vq", "repos": ["VeriLibUser/slug"], "pipeline": "leanblueprint" } for time charts; with "type": "table" add "groupBy": "statement_type"|"verification_status"|"language"|"chapter" and "columns" from total, verified, trusted, completed, in_progress, unspecified, failed.
- Use /r/{username}/{slug} usernames, not GitHub owner/repo.
- Output only the markdown page. No commentary.