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/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/` 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"