diff --git a/Justfile b/Justfile index f895fef..4d2372a 100644 --- a/Justfile +++ b/Justfile @@ -739,6 +739,7 @@ atlas-build: atlas-check: bun scripts/atlas/census-atlas.mjs check bun test tests/atlas/census-atlas.test.mjs + bash tests/census/build_rows_status_test.sh atlas-find query: bun scripts/atlas/census-atlas.mjs find "{{query}}" diff --git a/scripts/census/build-rows.sh b/scripts/census/build-rows.sh index 67b8e15..4fc6127 100644 --- a/scripts/census/build-rows.sh +++ b/scripts/census/build-rows.sh @@ -14,6 +14,13 @@ # tests/, fixtures/, corpus/, benches/ count as fixtures. "theory" is a # first-pass heuristic: more Agda/Lean/Rocq/Isabelle files than Idris2/SPARK # files. A human confirms each row. +# +# status_doc names one document per repository. A repository's proof status +# lives in its PROOF-STATUS file (standards PROOF-POLICY ยง8.5); PROOF-NEEDS +# lists obligations and proof-debt lists holes. So a PROOF-STATUS document +# wins over a proof-debt one, which wins over a PROOF-NEEDS one; within a +# rank the first path in sorted order wins. Taking the first sorted path +# alone named docs/status/PROOF-NEEDS.adoc over docs/status/PROOF-STATUS.adoc. set -euo pipefail R=$1 T=$2 tmp=$(mktemp -d); trap 'rm -rf "$tmp"' EXIT @@ -42,7 +49,11 @@ jq -r '.repo+"\t"+.path' "$R/repos-with-status.jsonl" | sort > "$tmp/status.tsv" awk -F'\t' ' FILENAME ~ /holes\.tsv$/ { h[$1" "$2]++; next } FILENAME ~ /decls\.tsv$/ { d[$1]++; next } - FILENAME ~ /status\.tsv$/ { if (!($1 in st)) st[$1]=$2; next } + FILENAME ~ /status\.tsv$/ { + b = tolower($2); sub(/.*\//, "", b) + k = (b ~ /^proof-status/) ? 3 : (b ~ /^proof-debt/) ? 2 : 1 + if (!($1 in st) || k > sk[$1]) { st[$1]=$2; sk[$1]=k } + next } { n[$1]++; if ($3) fx[$1]++; pc[$1" "$2]++ if ($2 ~ /agda|lean|rocq|isabelle/) th[$1]++; if ($2 ~ /idris2|spark/) en[$1]++ } END { diff --git a/tests/census/build_rows_status_test.sh b/tests/census/build_rows_status_test.sh new file mode 100755 index 0000000..16d7b49 --- /dev/null +++ b/tests/census/build_rows_status_test.sh @@ -0,0 +1,49 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# +# build-rows.sh picks one status_doc per repository: PROOF-STATUS over +# proof-debt over PROOF-NEEDS, the first sorted path within a rank. The +# previous rule (first sorted path) named docs/status/PROOF-NEEDS.adoc for +# repositories whose status lives in docs/status/PROOF-STATUS.adoc. +# Usage: bash tests/census/build_rows_status_test.sh (needs jq) +set -euo pipefail +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)" +command -v jq >/dev/null || { echo "FAIL: jq is required" >&2; exit 1; } +raw=$(mktemp -d); trap 'rm -rf "$raw"' EXIT + +: > "$raw/holes.jsonl"; : > "$raw/decls.jsonl" +# A non-empty template list: build-rows.sh reads it with NR==FNR, so an +# empty list would swallow files.jsonl as template paths and emit no rows. +echo "verification/proofs/template-only.v" > "$raw/template.txt" +for r in o/both o/needs-only o/debt-and-needs o/root-status o/none; do + printf '{"repo":"%s","path":"src/A.agda","ext":"agda"}\n' "$r" +done > "$raw/files.jsonl" +cat > "$raw/repos-with-status.jsonl" <<'J' +{"repo":"o/both","path":"docs/status/PROOF-NEEDS.adoc"} +{"repo":"o/both","path":"docs/status/PROOF-STATUS.adoc"} +{"repo":"o/needs-only","path":"docs/status/PROOF-NEEDS.adoc"} +{"repo":"o/debt-and-needs","path":"PROOF-NEEDS.md"} +{"repo":"o/debt-and-needs","path":"docs/proof-debt.adoc"} +{"repo":"o/root-status","path":"PROOF-NEEDS.adoc"} +{"repo":"o/root-status","path":"proofs/proof-status.md"} +{"repo":"o/root-status","path":"PROOF-STATUS.adoc"} +J + +rows=$(bash "$ROOT/scripts/census/build-rows.sh" "$raw" "$raw/template.txt") +doc() { + local repo="$1" + jq -r --arg r "$repo" '.[] | select(.repo == $r) | .status_doc' <<< "$rows" +} +fail=0 +expect() { + local repo="$1" want="$2" got + got=$(doc "$repo") + if [[ "$got" == "$want" ]]; then echo "PASS: $repo -> ${want:-}" + else echo "FAIL: $repo -> '$got', expected '$want'"; fail=1; fi +} +expect o/both docs/status/PROOF-STATUS.adoc +expect o/needs-only docs/status/PROOF-NEEDS.adoc +expect o/debt-and-needs docs/proof-debt.adoc +expect o/root-status PROOF-STATUS.adoc +expect o/none "" +exit "$fail"