From a16daa75b0b19220aa8a4f1308e39eaf53906918 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:37:19 +0000 Subject: [PATCH 1/2] fix(census): pick the proof-status ledger, and keep rows with an empty template list MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit build-rows.sh chose each repository's status document by path order, so docs/status/PROOF-NEEDS.adoc won over docs/status/PROOF-STATUS.adoc and resource-algebra's row points at its to-do list rather than its ledger (PROOF-POLICY §8.5's proof-status file). It now ranks PROOF-STATUS, then proof-debt, then PROOF-NEEDS. The committed rows change at the next census run; nothing generated is edited by hand. The template list was read with awk's NR==FNR, which is also true of every line when the list is empty, so an empty list silently dropped every row. It keys on FILENAME == ARGV[1] now. tests/census/status_doc_rank_test.sh covers both (it fails on the old script) and runs in proven-tests.yml beside the atlas tests. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/proven-tests.yml | 1 + CHANGELOG.adoc | 11 +++++++++ README.adoc | 4 +++ scripts/census/build-rows.sh | 16 +++++++++--- tests/census/status_doc_rank_test.sh | 37 ++++++++++++++++++++++++++++ 5 files changed, 65 insertions(+), 4 deletions(-) create mode 100755 tests/census/status_doc_rank_test.sh diff --git a/.github/workflows/proven-tests.yml b/.github/workflows/proven-tests.yml index fb802367..2e4eedef 100644 --- a/.github/workflows/proven-tests.yml +++ b/.github/workflows/proven-tests.yml @@ -49,6 +49,7 @@ jobs: run: | bun scripts/atlas/census-atlas.mjs check bun test tests/atlas/census-atlas.test.mjs + bash tests/census/status_doc_rank_test.sh - name: Install verified Nickel 1.18.0 (K9 L2 semantics) run: | set -euo pipefail diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index a7a75078..7b28de1e 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -10,6 +10,17 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. ==== Fixed +* Census rows: `scripts/census/build-rows.sh` picked a repository's status + document by path order, so `docs/status/PROOF-NEEDS.adoc` won over + `docs/status/PROOF-STATUS.adoc` (resource-algebra's row points at its + to-do list, not its ledger). It now takes a PROOF-STATUS file first, then a + proof-debt file, then PROOF-NEEDS. The committed rows change at the next + census run. +* `build-rows.sh` read the template list with awk's `NR==FNR`, which is also + true of every line when that list is empty, so an empty list silently + dropped every row. It keys on the file name now. + `tests/census/status_doc_rank_test.sh` covers both and runs in + `proven-tests.yml`. * `repo-init` minting a repository created with GitHub's "Use this template" (measured on metadatastician/lintel, 2026-10-14): ** provenance recorded the CHILD's own HEAD as the template commit. The diff --git a/README.adoc b/README.adoc index 2aec13fe..e032ac90 100644 --- a/README.adoc +++ b/README.adoc @@ -75,6 +75,10 @@ The first census covered 476 repositories: * *Hole, axiom, unsafe and policy counts* are textual candidates, not kernel verdicts. The kernel is the authority. `import Mathlib` shows under policy. +* *Status document*: the first of a PROOF-STATUS file, a proof-debt file, a + PROOF-NEEDS file. Rows from the 2026-10-26 census were picked by path, so + some point at PROOF-NEEDS where a PROOF-STATUS exists; the next census + corrects them. * *Declaration counts* overcount Agda and Idris2: every column-0 type signature counts, helpers included. * *Older template copies* survive as "own" files in some repos: for example diff --git a/scripts/census/build-rows.sh b/scripts/census/build-rows.sh index 67b8e15b..4be14343 100644 --- a/scripts/census/build-rows.sh +++ b/scripts/census/build-rows.sh @@ -19,7 +19,7 @@ R=$1 T=$2 tmp=$(mktemp -d); trap 'rm -rf "$tmp"' EXIT jq -r '[.repo,.path,.ext]|@tsv' "$R/files.jsonl" \ -| awk -F'\t' 'NR==FNR{t[$1]=1;next} !($2 in t)' "$T" - \ +| awk -F'\t' 'FILENAME==ARGV[1]{t[$1]=1;next} !($2 in t)' "$T" - \ | awk -F'\t' 'BEGIN{OFS="\t"} { e=$3; p="other" if (e ~ /agda/) p="agda"; else if (e ~ /idr|ipkg/) p="idris2" @@ -32,12 +32,20 @@ jq -r '[.repo,.path,.ext]|@tsv' "$R/files.jsonl" \ print $1, p, fx }' > "$tmp/cls.tsv" jq -r '[.repo,.file,.class]|@tsv' "$R/holes.jsonl" \ -| awk -F'\t' 'NR==FNR{t[$1]=1;next} !($2 in t){print $1"\t"$3}' "$T" - > "$tmp/holes.tsv" +| awk -F'\t' 'FILENAME==ARGV[1]{t[$1]=1;next} !($2 in t){print $1"\t"$3}' "$T" - > "$tmp/holes.tsv" jq -r '[.repo,.file]|@tsv' "$R/decls.jsonl" \ -| awk -F'\t' 'NR==FNR{t[$1]=1;next} !($2 in t){print $1}' "$T" - > "$tmp/decls.tsv" +| awk -F'\t' 'FILENAME==ARGV[1]{t[$1]=1;next} !($2 in t){print $1}' "$T" - > "$tmp/decls.tsv" -jq -r '.repo+"\t"+.path' "$R/repos-with-status.jsonl" | sort > "$tmp/status.tsv" +# One status document per repository, by kind before path: a PROOF-STATUS +# file is the ledger (PROOF-POLICY §8.5), proof-debt the escape-hatch record, +# PROOF-NEEDS the to-do list. Sorting by path alone picked +# docs/status/PROOF-NEEDS.adoc over docs/status/PROOF-STATUS.adoc. +jq -r '.repo+"\t"+.path' "$R/repos-with-status.jsonl" \ +| awk -F'\t' 'BEGIN{OFS="\t"} { b=toupper($2); sub(/.*\//, "", b) + k = (b ~ /^PROOF-STATUS/) ? 0 : (b ~ /^PROOF-DEBT/) ? 1 : 2 + print $1, k, $2 }' \ +| sort -t$'\t' -k1,1 -k2,2n -k3,3 | cut -f1,3 > "$tmp/status.tsv" awk -F'\t' ' FILENAME ~ /holes\.tsv$/ { h[$1" "$2]++; next } diff --git a/tests/census/status_doc_rank_test.sh b/tests/census/status_doc_rank_test.sh new file mode 100755 index 00000000..92c0ce98 --- /dev/null +++ b/tests/census/status_doc_rank_test.sh @@ -0,0 +1,37 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# build-rows.sh picks one status document per repository: PROOF-STATUS +# before proof-debt before PROOF-NEEDS, whatever their paths sort to. +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." +raw=$(mktemp -d); trap 'rm -rf "$raw"' EXIT +: > "$raw/holes.jsonl"; : > "$raw/decls.jsonl" +# An empty template list must not drop every row (awk NR==FNR did). +: > "$raw/template.txt" +for r in a/needs-first a/debt-only a/needs-only; do + printf '{"repo":"%s","path":"src/X.agda","ext":"agda"}\n' "$r" >> "$raw/files.jsonl" +done +cat > "$raw/repos-with-status.jsonl" <<'J' +{"repo":"a/needs-first","path":"docs/status/PROOF-NEEDS.adoc"} +{"repo":"a/needs-first","path":"docs/status/PROOF-STATUS.adoc"} +{"repo":"a/needs-first","path":"docs/proof-debt.adoc"} +{"repo":"a/debt-only","path":"PROOF-NEEDS.adoc"} +{"repo":"a/debt-only","path":"docs/proof-debt.md"} +{"repo":"a/needs-only","path":"PROOF-NEEDS.adoc"} +J +got=$(bash scripts/census/build-rows.sh "$raw" "$raw/template.txt" \ + | jq -r '.[] | .repo + " " + .status_doc' | sort) +want=$'a/debt-only docs/proof-debt.md\na/needs-first docs/status/PROOF-STATUS.adoc\na/needs-only PROOF-NEEDS.adoc' +if [ "$got" != "$want" ]; then + printf 'FAIL: status documents\n--- want\n%s\n--- got\n%s\n' "$want" "$got" >&2 + exit 1 +fi +echo "PASS: build-rows.sh ranks PROOF-STATUS, then proof-debt, then PROOF-NEEDS" +# A listed template path still counts as boilerplate: with every proof file +# on the list, no repository has own files, so there are no rows. +echo "src/X.agda" > "$raw/template.txt" +if [ "$(bash scripts/census/build-rows.sh "$raw" "$raw/template.txt")" != "[]" ]; then + echo "FAIL: template paths were counted as own files" >&2 + exit 1 +fi +echo "PASS: template paths are set aside, and an empty template list drops nothing" From 1e1b58d0ba33ffb64ddd04943d0a1a27c3b0ceb0 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:57:56 +0000 Subject: [PATCH 2/2] docs(architecture): regenerate the repository map The committed REPOSITORY-MAP.adoc predates applied-systems/ and its subdirectories, so tests/shape/repo_map_determinism_test.sh fails and estate-rules is red on main. Regenerated with `just repo-map` (scripts/gen-repo-map.sh); the determinism test passes under every locale it tries. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- docs/architecture/REPOSITORY-MAP.adoc | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index d28ba7e4..e2cc583c 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/docs/architecture/REPOSITORY-MAP.adoc @@ -117,6 +117,10 @@ predecessors did. | yes | - +| `applied-systems/` +| yes +| owner-requested reusable applications area (2026-11-07) + | `benches/` | optional | Cargo-conventional at package root @@ -204,6 +208,11 @@ your own repo - but do not read their emptiness as neglect here. | `.machine_readable/bot_directives/` | `.machine_readable/descriptiles/anchors/` | `.machine_readable/scripts/verification/` +| `applied-systems/decision-science/` +| `applied-systems/finance/` +| `applied-systems/finance/cohort-economics/` +| `applied-systems/finance/liquidity/` +| `applied-systems/organisational-design/` | `docs/governance/audit/` | `docs/governance/audit/compliance/` | `docs/governance/audit/effects/`