Skip to content

Live editor: /dynamic-chart-v4. This is the same markdown as react-graph-standard/src/components/dynamicChart/defaultPageV4.md. Chart fences render as live tables in the app; here they are copy-pasteable JSON.

Parent spec: Dynamic chart pages.

By chapter (live atoms)

Verso’s By chapter table counts blueprint nodes (definition vs theorem, specified / verified / ready-next). Those node atoms (language: "blueprint") are not stored in MySQL yet — probe-leanblueprint enriches the probe JSON, then repostats.raw_record keeps only repo-wide totals.

What is on each VeriLib atom:

Column Meaning
code_path Lean file path. Chapter ≈ the Nth folder (pathDepth, default 2 → KVAC/Core/… → Core)
statement_type def, theorem, structure, abbrev, …
specified 0 / 1
status_id verified / transitively-verified / trusted / unverified / failed

So this page is a live GROUP BY of the atoms table, not a copy of Verso. Ready next does not exist on atoms (that is a blueprint-dependency walk). Empty Verso chapters with “no registry entries yet” also do not appear — there are no atom rows to group.

New chart type: "type": "table". New source: "kind": "atoms". You pick the row (groupBy) and the columns (kinds, specified, status). The API only returns count buckets; the browser maps them onto your column spec. No user SQL.

Repo below is today’s successful leanblueprint atomize: steven460191/keyedverificationanonymouscredential-model-4 (270 atoms). Logged in required.

Folder chapters (pathDepth 2)

groupBy: "chapter" takes the 2nd code_path segment. Definitions here are Lean def + structure + abbrev + inductive + instance (not Verso’s paper-node class). Theorems with status_id transitively-verified count as Verified even when specified is 0 — that is what this repo actually stored.

{
  "id": "kvac-by-chapter",
  "type": "table",
  "title": "By chapter — Lean atoms",
  "width": "full",
  "source": {
    "kind": "atoms",
    "repos": ["steven460191/keyedverificationanonymouscredential-model-4"],
    "groupBy": "chapter",
    "pathDepth": 2,
    "columns": [
      { "key": "def_total", "group": "Definitions", "label": "Total", "kinds": ["def", "structure", "abbrev", "inductive", "instance"] },
      { "key": "def_specified", "group": "Definitions", "label": "Specified", "kinds": ["def", "structure", "abbrev", "inductive", "instance"], "specified": true },
      { "key": "thm_total", "group": "Theorems", "label": "Total", "kinds": ["theorem"] },
      { "key": "thm_specified", "group": "Theorems", "label": "Specified", "kinds": ["theorem"], "specified": true },
      { "key": "thm_verified", "group": "Theorems", "label": "Verified", "kinds": ["theorem"], "status": ["verified", "transitively-verified"] }
    ]
  }
}

Deeper folders (pathDepth 3)

Same atoms, one more path segment — KVAC/Schemes/MicroCMZ becomes MicroCMZ instead of Schemes.

{
  "id": "kvac-depth-3",
  "type": "table",
  "title": "By subfolder — pathDepth 3",
  "width": "full",
  "source": {
    "kind": "atoms",
    "repos": ["steven460191/keyedverificationanonymouscredential-model-4"],
    "groupBy": "chapter",
    "pathDepth": 3
  }
}

By statement_type

Row = atom kind. Columns = Total / Specified / Verified. Same atoms source, different groupBy.

{
  "id": "kvac-by-kind",
  "type": "table",
  "title": "By statement_type",
  "width": "full",
  "source": {
    "kind": "atoms",
    "repos": ["steven460191/keyedverificationanonymouscredential-model-4"],
    "groupBy": "statement_type",
    "columns": [
      { "key": "total", "label": "Total" },
      { "key": "specified", "label": "Specified", "specified": true },
      { "key": "verified", "label": "Verified", "status": ["verified", "transitively-verified"] },
      { "key": "trusted", "label": "Trusted", "status": ["trusted"] },
      { "key": "unverified", "label": "Unverified", "status": ["unverified"] }
    ]
  }
}

Column spec

Each column is a count filter over the buckets:

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

groupBy is chapter or statement_type. pathDepth is 1–4 (chapter only).

When source.kind is atoms, each rendered table includes a collapsible Live data source section below the grid. It lists:

  • The API path (GET /repobrowser/atom_group_data)
  • Bucket shape: group × statement_type × specified × status_id → count
  • statement_type values present in this repo (use these in columns[].kinds)
  • Allowed status filter names
  • Row groups returned for the current groupBy / pathDepth

Use that footer to discover which kinds and status filters actually match data — the interactive spec alone cannot know your repo’s contents.

Interactive chart spec

Hover/click keywords in the embedded spec on /pages (or open /assets/docs/dynamic-chart-spec.html on VD). The Live atoms table tab now documents columns[].key, label, group, kinds, specified, and status. Database (repostats) lists 19 supported metric field names; External JSON (url) documents snapshot vs array schemas.