From 9fd5f1191ef183a7d5c8d30ef29796266081adeb Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 17:57:08 +0000 Subject: [PATCH] fix(census): one refresh tool that refuses private names (WO 0.1, B) Landing change B of work order 0.1, approved row by row by the owner on 2026-11-10. update-rows.sh stays the one refresh tool. The other three tools in open pull requests are not carried. - update-rows.sh refuses a name that is not public in repos.json, so a private repository never gets a row (ruling D-2; the public-only check of hyperpolymath/mathesis#41, e1e61ed). It checks every name before any clone, and a reached repository leaves unreachable.json. - A new offline test proves each refusal and that a refused run changes no census file. - The catalogue says that it carries no proof status and no grade (the sentence of #42, 54e8aad, worded to the order main uses). - gen-repo-map.sh counts a directory as declared-only when its README is a stub, not when the directory merely holds a README (#41, 4edcea9). The repository map loses 13 rows that hold real content. Not carried: the snapshot step of #41 needs mv --exchange, which coreutils 9.4 on ubuntu-24.04 does not have. The --merge mode and the provenance file of #24, and refreshed.json of #41 and #42, wait for WO 2.1, which puts the commit and the date into each row. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM --- docs/architecture/REPOSITORY-MAP.adoc | 17 ++------------ docs/catalogue/catalogue.adoc | 7 ++++++ scripts/census/render-catalogue.sh | 7 ++++++ scripts/census/update-rows.sh | 11 ++++++++- scripts/gen-repo-map.sh | 21 ++++++++++++----- tests/census/update_rows_guard_test.sh | 32 ++++++++++++++++++++++++++ 6 files changed, 73 insertions(+), 22 deletions(-) create mode 100755 tests/census/update_rows_guard_test.sh diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index e2cc583c..0edf7b6b 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/docs/architecture/REPOSITORY-MAP.adoc @@ -197,22 +197,15 @@ predecessors did. == Declared structure not yet filled -These directories currently hold only a stub `README.adoc` and a level -manifest. That is deliberate. They declare the shape a repository minted +These directories currently hold only a stub `README.adoc` or `.gitkeep`. +That is deliberate. They declare the shape a repository minted from this template is expected to grow into; they are *intended structure, not abandoned work*. Add content, or delete the directory in your own repo - but do not read their emptiness as neglect here. [cols="1"] |=== -| `.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/` @@ -237,14 +230,9 @@ your own repo - but do not read their emptiness as neglect here. | `docs/theory/ontologies/` | `docs/theory/other/` | `docs/theory/socio-technical/` -| `docs/whitepapers/` | `docs/whitepapers/academic/` | `docs/whitepapers/industry/` -| `docs/whitepapers/outreach/` | `examples/` -| `features/boj-server/` -| `features/panic-attacker/` -| `src/aspects/` | `src/aspects/integrity/` | `src/aspects/observability/` | `src/aspects/security/` @@ -255,7 +243,6 @@ your own repo - but do not read their emptiness as neglect here. | `src/errors/` | `src/interface/generated/` | `src/interface/generated/abi/` -| `tests/fuzz/` | `verification/benchmarks/` | `verification/coverage/` | `verification/fuzzing/` diff --git a/docs/catalogue/catalogue.adoc b/docs/catalogue/catalogue.adoc index 158c1acd..63ace42e 100644 --- a/docs/catalogue/catalogue.adoc +++ b/docs/catalogue/catalogue.adoc @@ -14,6 +14,13 @@ Agda and Idris2 counts include helpers. Hole, axiom, unsafe and policy counts come from proof-craft's `proof-holes.sh`: textual candidates, not kernel verdicts. +The catalogue carries no proof status and no proof witness grade (`PWG-`, +PROOF-POLICY §8). Counts say what files exist, not what has been checked, and a +grade is derived from a repository's receipts, never from a census. The +*Proof-status doc* column names the file that holds those statuses, preferring +`PROOF-STATUS` over `proof-debt` over `PROOF-NEEDS` when a repository has more +than one. + == Theory [cols="3,1,1,4,1,1,1,1,1,3",options="header"] diff --git a/scripts/census/render-catalogue.sh b/scripts/census/render-catalogue.sh index 97e92891..0109d214 100644 --- a/scripts/census/render-catalogue.sh +++ b/scripts/census/render-catalogue.sh @@ -38,6 +38,13 @@ Agda and Idris2 counts include helpers. Hole, axiom, unsafe and policy counts come from proof-craft's \`proof-holes.sh\`: textual candidates, not kernel verdicts. +The catalogue carries no proof status and no proof witness grade (\`PWG-\`, +PROOF-POLICY §8). Counts say what files exist, not what has been checked, and a +grade is derived from a repository's receipts, never from a census. The +*Proof-status doc* column names the file that holds those statuses, preferring +\`PROOF-STATUS\` over \`proof-debt\` over \`PROOF-NEEDS\` when a repository has more +than one. + == Theory $(table theory) diff --git a/scripts/census/update-rows.sh b/scripts/census/update-rows.sh index 5651ee18..13cd8c16 100644 --- a/scripts/census/update-rows.sh +++ b/scripts/census/update-rows.sh @@ -9,7 +9,8 @@ # it. Its row in catalogue-rows.json is replaced, added, or removed when it # no longer has proof files of its own. Every other row is left as it is. # Raw output goes to MATHESIS_WORK (default: a fresh temporary directory) -# and is not committed. A name must appear in repos.json, so the catalogue's +# and is not committed. Every name is checked before any clone. A name must +# appear in repos.json and be public there, so the catalogue's # repository count stays the census input; a fork must also be listed in # forks-with-own-proofs.txt. set -euo pipefail @@ -23,6 +24,9 @@ jq -c '.[]' "$census/repos.json" > "$work/repos.jsonl" for repo in "$@"; do rec=$(jq -c --arg r "$repo" 'select(.full_name == $r)' "$work/repos.jsonl") [ -n "$rec" ] || { echo "update-rows: $repo is not in repos.json" >&2; exit 1; } + # A private repository never gets a row: the catalogue is public (ruling D-2). + [ "$(jq -r '.visibility' <<<"$rec")" = public ] \ + || { echo "update-rows: $repo is not public in repos.json" >&2; exit 1; } if [ "$(jq -r '.fork' <<<"$rec")" = true ] \ && ! grep -qxF "$repo" "$census/forks-with-own-proofs.txt"; then echo "update-rows: $repo is a fork not listed in forks-with-own-proofs.txt" >&2 @@ -45,5 +49,10 @@ jq -cS --slurpfile new "$work/new-rows.json" --slurpfile names "$work/names.json map(select(.repo as $r | $names[0] | index($r) | not)) + $new[0] | sort_by(.repo) ' "$census/catalogue-rows.json" > "$work/rows.json" mv "$work/rows.json" "$census/catalogue-rows.json" +# A named repository was reached, so it leaves the "not reached" list. +jq -cS --slurpfile names "$work/names.json" \ + 'map(select(.repo as $r | $names[0] | index($r) | not))' \ + "$census/unreachable.json" > "$work/unreach.json" +mv "$work/unreach.json" "$census/unreachable.json" bash "$here/render-catalogue.sh" "$census" > "$here/../../docs/catalogue/catalogue.adoc" echo "update-rows: refreshed $(wc -l < "$work/census-list.txt") repo(s); raw census kept in $work" diff --git a/scripts/gen-repo-map.sh b/scripts/gen-repo-map.sh index befe940f..0799d54b 100755 --- a/scripts/gen-repo-map.sh +++ b/scripts/gen-repo-map.sh @@ -80,10 +80,19 @@ done < "$ALLOW" # julia-library/ child is real content. (The ply manifests that once padded # these counts were folded into the repo deed — standards#837 pilot.) declared_only() { - local d="$1" n - n=$(repo_files "$d" | awk -F/ '{print $NF}' \ - | grep -vxE 'README\.adoc|\.gitkeep' | wc -l) - [ "$n" -eq 0 ] + local d="$1" f + while IFS= read -r f; do + case "${f##*/}" in + .gitkeep) ;; + README.adoc) + # A stub has only a title, comments, attributes and blank lines. + if grep -qEv '^[[:space:]]*$|^//|^= |^:[^:]+:' "$f"; then + return 1 + fi ;; + *) return 1 ;; + esac + done < <(repo_files "$d") + return 0 } { @@ -120,8 +129,8 @@ declared_only() { echo echo "== Declared structure not yet filled" echo - echo "These directories currently hold only a stub \`README.adoc\` and a level" - echo "manifest. That is deliberate. They declare the shape a repository minted" + echo "These directories currently hold only a stub \`README.adoc\` or \`.gitkeep\`." + echo "That is deliberate. They declare the shape a repository minted" echo "from this template is expected to grow into; they are *intended" echo "structure, not abandoned work*. Add content, or delete the directory in" echo "your own repo - but do not read their emptiness as neglect here." diff --git a/tests/census/update_rows_guard_test.sh b/tests/census/update_rows_guard_test.sh new file mode 100755 index 00000000..1581be36 --- /dev/null +++ b/tests/census/update_rows_guard_test.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# update-rows.sh checks every name before any clone: an unlisted name, a +# private repository or an unlisted fork stops the run, and no file changes. +# Offline: each case fails before census-repo.sh would clone. +set -euo pipefail +root=$(cd "$(dirname "$0")/../.." && pwd) +t=$(mktemp -d); trap 'rm -rf "$t"' EXIT +mkdir -p "$t/scripts/census" "$t/docs/catalogue/census" +cp "$root/scripts/census/"*.sh "$t/scripts/census/" +c=$t/docs/catalogue/census +cat > "$c/repos.json" <<'J' +[{"fork":false,"full_name":"o/public","pushed_at":"2026-11-10T00:00:00Z","visibility":"public"}, + {"fork":false,"full_name":"o/hidden","pushed_at":"2026-11-10T00:00:00Z","visibility":"private"}, + {"fork":true,"full_name":"o/fork","pushed_at":"2026-11-10T00:00:00Z","visibility":"public"}] +J +echo '[]' > "$c/catalogue-rows.json"; echo '[]' > "$c/unreachable.json"; : > "$c/forks-with-own-proofs.txt" +before=$(cat "$c"/*.json | sha256sum) +fail=0 +expect_refusal() { # want-message name... + local want=$1; shift + if err=$(bash "$t/scripts/census/update-rows.sh" "$@" 2>&1); then + echo "FAIL: update-rows.sh $* succeeded"; fail=1 + elif [[ "$err" != *"$want"* ]]; then + echo "FAIL: update-rows.sh $*: '$err'"; fail=1 + else echo "PASS: $* -> $want"; fi +} +expect_refusal "is not in repos.json" o/missing +expect_refusal "is not public" o/public o/hidden +expect_refusal "is a fork not listed" o/fork +[ "$(cat "$c"/*.json | sha256sum)" = "$before" ] || { echo "FAIL: a refused run changed census files"; fail=1; } +exit "$fail"