perf: store census data as single JSON arrays

Justfile

@@ -716,7 +716,7 @@ uncloak:
 
 # ── mathesis: estate maths catalogue ──────────────────────────────────────
 
-# Re-run the proof census over docs/catalogue/census/repos.jsonl and regenerate the catalogue
+# Re-run the proof census over docs/catalogue/census/repos.json and regenerate the catalogue
 census:
     bash scripts/census/run-census.sh
 

README.adoc

@@ -20,14 +20,14 @@ in Rocq and Lean). The working method is the proof-craft skill.
 [cols="1,3"]
 |===
 |`docs/catalogue/catalogue.adoc` |The catalogue: one row per repository with proof files of its own, split into theory and engineering. Generated; do not edit by hand.
-|`docs/catalogue/census/` |What the catalogue is rendered from: `catalogue-rows.jsonl` (one row of counts per repository, no file paths), `repos.jsonl` (the census input), `unreachable.jsonl` and `template-paths.txt`. Each JSONL file is I-JSON/JCS, one object per line.
+|`docs/catalogue/census/` |What the catalogue is rendered from: `catalogue-rows.json` (one row of counts per repository, no file paths), `repos.json` (the census input), `unreachable.json` and `template-paths.txt`. Each `.json` file is one I-JSON/JCS array.
 |`scripts/census/` |`run-census.sh` (whole census), `census-repo.sh` (one repo), `summarise.sh`, `build-rows.sh` (raw census to rows), `render-catalogue.sh` (rows to catalogue), and proof-craft's `proof-holes.sh`.
 |`Justfile` |`just census`, `just catalogue`, `just catalogue-check` (the committed catalogue matches the committed data).
 |===
 
 == How the census works
 
-. *List repositories.* `docs/catalogue/census/repos.jsonl` is the input. Agent sessions build
+. *List repositories.* `docs/catalogue/census/repos.json` is the input. Agent sessions build
   it with the Claude Code remote `list_repos` tool, because the GitHub API is
   not reachable from them.
 . *List proof files cheaply.* Each repository is cloned blobless with
@@ -54,7 +54,7 @@ The first census covered 476 repositories:
   the end of the catalogue, among them `cut-calculus`.
 * *Possibly missing:* the listing returned only repositories pushed since
   2026-09-15, so older, untouched repos may be absent. Add them to
-  `docs/catalogue/census/repos.jsonl` and rerun.
+  `docs/catalogue/census/repos.json` and rerun.
 * *Theory or engineering* is a heuristic: more Agda, Lean, Rocq or Isabelle
   files than Idris2 or SPARK files reads as theory. Confirm each row against
   PROOF-POLICY.

docs/catalogue/census/unreachable.json

@@ -0,0 +1 @@
+[{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"catachresis-colloquium/reflexive-ai-studio"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/007-lang"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/HOL"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/achievements-lab"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/ai-cli-lab"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/axel-protocol"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/blog-drafts"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/claude-config-vault"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/claude-memory"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/contractiles-a2-lab"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/cut-calculus"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/dev-notes-vault"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/dev-notes"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/dotfiles"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/echobox"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/email-octad-experiment"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/estate-scripts"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/frayed-knot-toolkit"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/fumble"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/git-seo"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/hottchpotch"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/hyperpolymath-sovereign-registry"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/info"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/jewell.nexus"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/jonathanjewell.dev"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/lcb-website"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/lfs-shared"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/linguist"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/memory-vault"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/poly-observability-mcp"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/polystack"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/rescript"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/squisher-corpus"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/this-ssg"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/tools"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/typefix-zero"},{"error":"fatal: could not read Username for 'https://github.com': terminal prompts disabled","exit":128,"repo":"hyperpolymath/vex-tools"}]

scripts/census/build-rows.sh

@@ -2,7 +2,7 @@
 # SPDX-License-Identifier: MPL-2.0
 # Fold the raw, path-level census into one row per repository.
 #
-# Usage: build-rows.sh RAW_DIR TEMPLATE_PATHS > catalogue-rows.jsonl
+# Usage: build-rows.sh RAW_DIR TEMPLATE_PATHS > catalogue-rows.json
 #   RAW_DIR         files.jsonl, holes.jsonl, decls.jsonl, repos-with-status.jsonl
 #                   (written by census-repo.sh + summarise.sh; not committed)
 #   TEMPLATE_PATHS  one path per line: proof files the RSR template ships,
@@ -61,4 +61,5 @@ awk -F'\t' '
 | jq -RcS 'split("\t") | {class:.[0], repo:.[1], own_files:(.[2]|tonumber),
     fixture_files:(.[3]|tonumber), provers:.[4], declarations:(.[5]|tonumber),
     holes:(.[6]|tonumber), axioms:(.[7]|tonumber), unsafe:(.[8]|tonumber),
-    policy:(.[9]|tonumber), status_doc:.[10]}'
+    policy:(.[9]|tonumber), status_doc:.[10]}' \
+| jq -cS -s .

scripts/census/render-catalogue.sh

@@ -3,8 +3,8 @@
 # Render the catalogue (AsciiDoc) from the committed census rows.
 #
 # Usage: render-catalogue.sh CENSUS_DIR > catalogue.adoc
-#   CENSUS_DIR holds catalogue-rows.jsonl (build-rows.sh), repos.jsonl and
-#   unreachable.jsonl. Output depends on those files only, so
+#   CENSUS_DIR holds catalogue-rows.json (build-rows.sh), repos.json and
+#   unreachable.json. Output depends on those files only, so
 #   `just catalogue-check` can prove the committed catalogue is current.
 set -euo pipefail
 C=$1
@@ -13,11 +13,11 @@ table() { # $1 = class
   echo '[cols="3,1,1,4,1,1,1,1,1,3",options="header"]'
   echo '|==='
   echo '|Repository |Own files |Fixtures |Provers (files) |Declarations |Holes |Axioms |Unsafe |Policy |Proof-status doc'
-  jq -sr --arg c "$1" '
+  jq -r --arg c "$1" '
     map(select(.class == $c))
     | sort_by(-.own_files, .repo)[]
     | "\n|https://github.com/\(.repo)[\(.repo)] |\(.own_files) |\(.fixture_files) |\(.provers) |\(.declarations) |\(.holes) |\(.axioms) |\(.unsafe) |\(.policy) |\(if .status_doc == "" then "—" else "`" + .status_doc + "`" end)"
-  ' "$C/catalogue-rows.jsonl"
+  ' "$C/catalogue-rows.json"
   echo '|==='
 }
 
@@ -27,7 +27,7 @@ cat <<EOF
 :toc:
 
 Generated by \`scripts/census/render-catalogue.sh\` from the census of
-$(jq -s length "$C/repos.jsonl") repositories. Do not edit by hand; rerun the census.
+$(jq length "$C/repos.json") repositories. Do not edit by hand; rerun the census.
 
 Each row is a repository with proof files of its own, after the files the RSR
 template ships as boilerplate are set aside. *Theory* and *engineering* are a
@@ -51,5 +51,5 @@ $(table engineering)
 These repositories could not be cloned (private, no credentials in the census
 session):
 
-$(jq -r '"* " + .repo' "$C/unreachable.jsonl")
+$(jq -r '.[] | "* " + .repo' "$C/unreachable.json")
 EOF

scripts/census/run-census.sh

@@ -4,7 +4,7 @@
 #
 # Usage: run-census.sh [REPO_LIST]
 #   REPO_LIST: one OWNER/REPO per line. Default: every non-fork repo in
-#   docs/catalogue/census/repos.jsonl. Refresh that file first when repos are
+#   docs/catalogue/census/repos.json. Refresh that file first when repos are
 #   added; the GitHub listing is not scriptable from agent sessions, so it is
 #   an input.
 #
@@ -16,19 +16,19 @@ here=$(cd "$(dirname "$0")" && pwd)
 census=$here/../../docs/catalogue/census
 work=${MATHESIS_WORK:-$(mktemp -d)}
 mkdir -p "$work"
-cp "$census/repos.jsonl" "$work/repos.jsonl"
+jq -c '.[]' "$census/repos.json" > "$work/repos.jsonl"
 if [ -n "${1:-}" ]; then
   cp "$1" "$work/census-list.txt"
 else
-  jq -r 'select(.fork|not) | .full_name | select(test("/awesome-")|not)' "$census/repos.jsonl" > "$work/census-list.txt"
+  jq -r 'select(.fork|not) | .full_name | select(test("/awesome-")|not)' "$work/repos.jsonl" > "$work/census-list.txt"
 fi
 list=$work/census-list.txt
 rm -rf "$work/out"
 while IFS= read -r repo; do
   [ -n "$repo" ] && MATHESIS_DATA=$work bash "$here/census-repo.sh" "$repo" || true
 done < "$list"
 MATHESIS_DATA=$work bash "$here/summarise.sh"
-cp "$work/unreachable.jsonl" "$census/unreachable.jsonl"
-bash "$here/build-rows.sh" "$work" "$census/template-paths.txt" > "$census/catalogue-rows.jsonl"
+jq -cS -s . "$work/unreachable.jsonl" > "$census/unreachable.json"
+bash "$here/build-rows.sh" "$work" "$census/template-paths.txt" > "$census/catalogue-rows.json"
 bash "$here/render-catalogue.sh" "$census" > "$here/../../docs/catalogue/catalogue.adoc"
 echo "raw census kept in $work"