Skip to content

fix(census): prefer a repo's PROOF-STATUS ledger; refresh hvn-dehallucinator's row - #18

Merged
hyperpolymath merged 2 commits into
mainfrom
claude/census-prefer-proof-status
Nov 10, 2026
Merged

hyperpolymath merged 2 commits into
mainfrom
claude/census-prefer-proof-status

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Summary

Two changes so the catalogue reflects metadatastician/hvn-dehallucinator as it is now:

  • The census chose a repository's status document by alphabetical order. A template-era PROOF-NEEDS.adoc therefore won over the real ledger beside it, and hvn-dehallucinator was catalogued against the wrong file.
  • That repository's row was from the 2026-10-26 census. Since then it has gained Haruspex*.agda, two reject fixtures and the differential-test TLA+ files.

Changes

  • scripts/census/build-rows.sh ranks status documents: PROOF-STATUS, then PROOF-NEEDS, then proof-debt, then the path. Committed rows change only when they are rebuilt, so other repositories that carry both documents keep their old pick until the next full census.

  • I rebuilt one row, metadatastician/hvn-dehallucinator at f2f31f7, with census-repo.sh, summarise.sh and build-rows.sh, and merged it into catalogue-rows.json by repo. Order and the one-line canonical form are unchanged.

    own files fixtures provers declarations status document
    before (2026-10-26) 9 3 agda 5, idris2 1, tla 3 108 docs/status/PROOF-NEEDS.adoc
    after (f2f31f7) 16 7 agda 10, idris2 1, tla 5 203 docs/status/PROOF-STATUS.adoc
  • docs/catalogue/catalogue.adoc and docs/atlas/generated/* are regenerated from the rows.

  • CHANGELOG.adoc gets an entry for both changes.

I did not run run-census.sh with a one-repo list: it would rewrite catalogue-rows.json and unreachable.json with that one repository only.

RSR Quality Checklist

Required

  • Tests pass:
    • render-catalogue.sh | diff catalogue.adoc: no difference (the catalogue-check recipe, run by hand because just is not installed here);
    • bun scripts/atlas/census-atlas.mjs check: PASS;
    • bun test tests/atlas/census-atlas.test.mjs: 10 pass, 0 fail.
  • Code is formatted
  • Linter is clean
  • No banned language patterns (bash, jq)
  • No unsafe blocks
  • No banned functions
  • SPDX license headers present on all new/modified source files
  • No secrets, credentials, or .env files included

As Applicable

  • CHANGELOG updated

Testing

As listed above. Every row except hvn-dehallucinator's is still the 2026-10-26 census. A row count is not a proof: theorem truth and receipts stay in the home repository (docs/standards/AUTHORITY.adoc).


Generated by Claude Code

…cinator's row

build-rows.sh took the first status document in alphabetical order, so a
template-era PROOF-NEEDS.adoc won over the real ledger beside it. It now
ranks PROOF-STATUS, then PROOF-NEEDS, then proof-debt, then the path.
Committed rows change only when rebuilt.

Rebuild one row, metadatastician/hvn-dehallucinator at f2f31f7, with
census-repo.sh, summarise.sh and build-rows.sh, merged into the committed
rows by repo: 16 own proof files (was 9), 7 fixtures (was 3), 203
declarations (was 108), status document docs/status/PROOF-STATUS.adoc.
The catalogue and the atlas are regenerated from the rows; the catalogue
check, `census-atlas check` and the atlas tests pass. Every other row is
still the 2026-10-26 census.

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

coderabbitai Bot commented Nov 9, 2026 •

Copy link
Copy Markdown

Explain Change →

Caution

Review failed

The pull request is closed.

  • 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

hyperpolymath commented Nov 9, 2026 •

Copy link
Copy Markdown
Owner Author

Two checks fail on this PR. Neither is caused by it, and both fail the same way on main:

  • Dogfood Gate / Canon lockstep. It compares canon.lock with mathesis_chora.deed and reports "the template does not implement the canon at HEAD". This PR changes neither file. The latest three Dogfood Gate runs on main all fail: a3dbe73 (run 42592014015), 4a90f39 and 1058bb8. Fixing it means moving this repository's canon pin, which is the owner's call.
  • estate-rules (tests/shape/repo_map_determinism_test.sh). It reports that the committed docs/architecture/REPOSITORY-MAP.adoc is stale and should be regenerated with just repo-map. The same test fails on a checkout of main at a3dbe73. The fix is to regenerate the map on main with bash scripts/gen-repo-map.sh .. I have not done that here: it would fold unrelated changes into this PR.

Generated by Claude Code

@hyperpolymath
hyperpolymath marked this pull request as ready for review November 9, 2026 15:52
@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:52:47.366824Z
We couldn’t complete this review. Comment @codex review to try again.
654de35 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.

@hyperpolymath
hyperpolymath merged commit dd1e832 into main Nov 10, 2026
40 of 41 checks passed
@sonarqubecloud

Copy link
Copy Markdown

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