Skip to content

fix(census): prefer a repository's PROOF-STATUS file as its status document - #17

Open
hyperpolymath wants to merge 2 commits into
mainfrom
claude/census-prefers-proof-status
Open

hyperpolymath wants to merge 2 commits into
mainfrom
claude/census-prefers-proof-status

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Summary

scripts/census/build-rows.sh picks one proof-status document per repository by sorting the paths alone. A repository that has both docs/status/PROOF-NEEDS.adoc and docs/status/PROOF-STATUS.adoc was therefore catalogued under PROOF-NEEDS, which is an obligations list, not the per-claim record. standards/3-practice/PROOF-POLICY.adoc §8.5 puts grades and recheck legs in the proof-status file, so the catalogue's pointer should reach that file. metadatastician/lintel is the case in the committed catalogue.

The choice now ranks PROOF-STATUS first, then PROOF-NEEDS, then proof-debt. Within a rank it takes the first path in byte order, under LC_ALL=C, so the choice no longer depends on the runner's locale.

Changes

  • scripts/census/build-rows.sh: ranks the status documents as described.
  • tests/census/build_rows_status_test.sh (new): covers four cases. PROOF-STATUS wins even where its path sorts later; PROOF-NEEDS beats proof-debt; proof-debt is used when it is the only document; and one of two PROOF-STATUS files is chosen. It fails on the old code (first case) and passes on the new. proven-tests.yml runs it beside the atlas tests.
  • docs/architecture/REPOSITORY-MAP.adoc: regenerated by scripts/gen-repo-map.sh. It was already stale on main (applied-systems/), and the new tests/census/ directory adds to it.

The committed rows and catalogue are unchanged: this fixes the rule, and the next census applies it. render-catalogue.sh against the committed data still matches docs/catalogue/catalogue.adoc.

Context: rows due for a refresh

Running census-repo.sh and build-rows.sh today shows the committed rows for two repositories are out of date:

repo own files fixtures declarations status doc
hyperpolymath/secret-types: committed / today 16 / 21 3 / 5 67 / 91 PROOF-STATUS.adoc
metadatastician/lintel: committed / today 6 / 13 4 / 9 58 / 80 docs/status/PROOF-NEEDS.adoc (committed) / docs/status/PROOF-STATUS.adoc (with this fix)

I'd refresh those rows after hyperpolymath/secret-types#26 and metadatastician/lintel#22 merge. Both move their proofs to the canonical --cubical-compatible invocation and record Proof Witness Grades (PWG-3) per claim. Lintel#22 also replaces its placeholder PROOF-STATUS with the real §8.5 record. Refreshing now would catalogue lintel's boilerplate status file.

RSR Quality Checklist

Required

  • Tests pass: bash tests/census/build_rows_status_test.sh passes, and the catalogue check matches.
  • Code is formatted
  • Linter is clean
  • No banned language patterns (bash, jq, awk)
  • No unsafe blocks without // SAFETY: comments
  • No banned functions
  • SPDX license headers present on all new/modified source files
  • No secrets, credentials, or .env files included

Generated by Claude Code

…cument

build-rows.sh chose one proof-status document per repository by sorting
paths alone, so a repo with docs/status/PROOF-NEEDS.adoc and
docs/status/PROOF-STATUS.adoc was catalogued under PROOF-NEEDS: an
obligations list, not the per-claim record. PROOF-POLICY §8.5 says grades and
recheck legs live in the proof-status file, so the catalogue's pointer should
reach it. metadatastician/lintel is the case in the committed catalogue.

The choice now ranks PROOF-STATUS before PROOF-NEEDS before proof-debt. Within
a rank it takes the first path in byte order, under LC_ALL=C so the choice no
longer depends on the runner's locale.

- tests/census/build_rows_status_test.sh covers four cases: PROOF-STATUS
  winning where its path sorts later, PROOF-NEEDS over proof-debt, proof-debt
  alone, and two PROOF-STATUS files. It fails on the old code (case one) and
  passes on the new. proven-tests.yml runs it beside the atlas tests.
- The committed rows are unchanged; the next census run applies the rule.
  `just catalogue-check` still matches.
- docs/architecture/REPOSITORY-MAP.adoc regenerated by scripts/gen-repo-map.sh.
  It was already stale on main (applied-systems/), and the new tests/census
  directory adds to it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs
@coderabbitai

coderabbitai Bot commented Nov 9, 2026 •

Copy link
Copy Markdown

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 20 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

Run configuration

Commits

Reviewing files that changed from the base of the PR and between a3dbe73 and a11e46b.

Files selected for processing: 5

  • .github/workflows/proven-tests.yml
  • docs/architecture/REPOSITORY-MAP.adoc
  • mathesis_chora.deed
  • scripts/census/build-rows.sh
  • tests/census/build_rows_status_test.sh
  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

…epo#298)

Canon lockstep is red on main and on this PR: standards' canon.lock now
records 2.1.5 (metadatastician/standards#1424: gate table 0.3.1 and the
applicability policy changed; the criteria did not), while this deed
declared 2.1.3. Only the (canon) clause moves: :version 2.1.3 to 2.1.5,
and :gates-sha256 2f31f46d… to 5c510bba…. canon.lock marks 2.1.5 draft;
this adopts the identity the lockstep gate compares.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs
@sonarqubecloud

sonarqubecloud Bot commented Nov 9, 2026

Copy link
Copy Markdown

@hyperpolymath
hyperpolymath marked this pull request as ready for review November 9, 2026 15:50
@chatgpt-codex-connector

Copy link
Copy Markdown
Codex Review Summary: ❌ Failed

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ❌ Failed 2026-11-09T15:50:53.007904Z
We couldn’t complete this review. Comment @codex review to try again.
a11e46b Draft marked ready
ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@chatgpt-codex-connector

Copy link
Copy Markdown

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants