Repository navigation
fix(census): land the scanner fixes from the open pull requests (WO 0.1, A) - #51
Merged
Merged
Conversation
….1, A) Carries the kept code of seven open pull requests onto main, as the owner approved row by row on 2026-11-10 (ruling D-6 (a)). Row data, repository maps and reruns from those pull requests are not carried: main has a newer full census. The catalogue text that describes the new rules changes at the next full census, so it never describes rules that did not make the rows. - build-rows.sh reads each list with FILENAME==ARGV[1]. On main an empty template list dropped every row (#25, a16daa7). - Template boilerplate is a file whose (path, blob) the template shipped, so a repository that rewrote a template file keeps it as its own (design of #26, 185e6cb; test of #20, c24d989, adapted). The template repository owns its own files (#44, 352af98). template-blobs.tsv is regenerated from rsr-template-repo today (56 pairs). - proof-holes.sh blanks comments and strings before it matches, and reports Idris2 signatures without clauses as axiom candidates (#27, ec833bc, 2f0f75e). - The census sees Rust proofs: Creusot with Pearlite, and Verus (#31, 7b1e096, cc2bdaa), with the assume_specification rule of #34 (d35fce4). - Ada counts as SPARK only where SPARK_Mode is on for the file or a .adc file (#44, 352af98). - Status documents keep the order of main (PROOF-STATUS, proof-debt, PROOF-NEEDS) in one mechanism, not two; a document nested two directories deep ranks after every shallow one (#31). - CI runs every tests/census/*.sh and the catalogue currency check (the CI step of #17, c8fc593). just census-test runs the same tests. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM
|
hyperpolymath
marked this pull request as ready for review
November 10, 2026 17:57
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
|
Caution Review failedThe pull request is closed.
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. |
This was referenced Nov 10, 2026
Closed
hyperpolymath
pushed a commit
that referenced
this pull request
Nov 10, 2026
WO 1.1: CI already runs just catalogue-check and every census test (#51). A planted duplicate row fails two CI steps: the atlas check ('Invalid or duplicate repo') and the catalogue currency check. A clean tree passes both. WO 1.2: CI runs .machine_readable/arrival-pack/verify.sh (the recipe just validate-claude-md) after Nickel is installed. A hand edit inside the generated region of CLAUDE.md fails it (checked by hand: exit 1). The coaptation check waits for stage 3, which regenerates the receipt. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM
1 task done
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Landing change A of work order 0.1 (
docs/proposals/mathesis-re-anchoring.adoc). The owner approved each triage row on 2026-11-10 (ruling D-6 (a)). This carries the kept code of #25, #26, #20, #27, #31, #34, #44 and the CI step of #17. Row data, repository maps and census reruns from those pull requests are not carried:mainhas a newer full census.Changes
build-rows.shreads each list withFILENAME==ARGV[1]. Onmain, an empty template list drops every row: the test of fix(census): pick the proof-status ledger, and keep rows with an empty template list #25 fails onmainand passes here.template-blobs.tsvis regenerated from rsr-template-repo today.proof-holes.shblanks comments and strings before it matches, and reports Idris2 signatures without clauses as axiom candidates (fix(census): comment-aware proof-holes.sh, Idris2 undefined-declaration axioms; refresh 13 rows #27).SPARK_Modeis on (fix(census): count Ada as SPARK only when it opts in; catalogue the template's own proofs; rerun the census #44).mainin one mechanism (it had two); a document nested two directories deep ranks last (census: see proofs written in Rust (Creusot/Pearlite, Verus), rank status docs #31).tests/census/*.shand the catalogue currency check.just census-testruns the same tests.The catalogue text that describes the new rules changes at the next full census, so the text never describes rules that did not make the rows. The scanner changes must also go to the proof-craft skill, the source of
proof-holes.sh.RSR Quality Checklist
Required
As Applicable
proven-tests.ymlTesting
just census-test: all 5 test files pass.just catalogue-check: catalogue current.just validate-repo-map: up to date.Generated by Claude Code