Repository navigation
census: count a declared negative control as a control, not an axiom - #88
Merged
Merged
Conversation
proof-holes.sh counted the postulate in CompositionalDA.jl proofs/agda/reject/Postulate.agda as an axiom (and the controls' missing --safe as policy). That file is a negative control: its header carries '-- EXPECT: [Pp]ostulate', the home gate's statement that the checker must reject it, and proofs/tests/axiom-audit.sh excludes proofs/agda/reject/ on purpose. The row therefore showed axioms 1 where the package has none in its checked cone. Rule fix at source: a file whose own header has an 'EXPECT: <pattern>' line comment is a declared negative control; its findings are emitted as class 'control' (still listed in holes.jsonl, not dropped) and do not count as hole, axiom, unsafe or policy, nor affect --fail-on. A real postulate, or a file that only mentions EXPECT: in prose, still counts (new test). Rows regenerated with update-rows.sh and atlas build, not hand-edited: CompositionalDA.jl axioms 1 -> 0 (re-pinned to 93fbfaf), ExactCounts.jl axioms 1 -> 0 and policy 6 -> 0, ExactTests.jl axioms 1 -> 0 and policy 1 -> 0 (same commits as before). JuliaPackageSpitter.jl keeps axioms 1: its postulate is tests/trusted-base-fixtures/RealPostulate.agda, which declares no EXPECT line, so it is not reclassified here. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmpJaHQJA34ezbx2YX
|
Warning Review limit reachedYou'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 4 minutes. View limit details
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. |
SonarCloud flagged the new emit, is_control and count helpers and the control test for reading positional parameters directly and for single bracket tests. Bind each parameter to a named local and use [[ ]]. The scan's output is unchanged; every tests/census script still passes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmpJaHQJA34ezbx2YX
|
hyperpolymath
marked this pull request as ready for review
November 13, 2026 19:59
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. |
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
The census counted every textual
postulateas an axiom. That included files that a home repository keeps as negative controls, which its own gate must reject. Because of this,CompositionalDA.jl,ExactCounts.jlandExactTests.jleach showed 1 axiom that is not in their trusted base. This came up during work on JoshuaJewell/MetaManifold-WebUI#23 (CompositionalDA.jl).Changes
scripts/census/proof-holes.sh: a file whose own header has a line commentEXPECT: <pattern>is a declared negative control. Its findings are emitted as classcontrol. They are still listed, but they are not counted as hole, axiom, unsafe or policy, and they do not affect--fail-on. The rule uses the declaration that the home repository makes in the file, not a hard-codedreject/path.tests/census/proof_holes_control_test.sh: new test. A control is classedcontrol. A real postulate, and a file that only mentionsEXPECT:in prose, still count as axioms.scripts/census/summarise.sh: small doc change.update-rows.shandcensus-atlas.mjs build(not edited by hand):CompositionalDA.jl: axioms 1 to 0. The commit moves to93fbfaf, from the fresh clone.ExactCounts.jl: axioms 1 to 0, policy 6 to 0. Same commit.ExactTests.jl: axioms 1 to 0, policy 1 to 0. Same commit.JuliaPackageSpitter.jlkeeps axioms 1. Itstests/trusted-base-fixtures/RealPostulate.agdahas noEXPECT:line. I did not inspect it further.Evidence for CompositionalDA.jl:
proofs/agda/reject/Postulate.agda:18is its only real postulate, and line 11 declares-- EXPECT: [Pp]ostulate.proofs/tests/axiom-audit.sh:14excludesproofs/agda/reject/on purpose.Prelude.agda:17andLogHom.agda:6mention the word only in comments.RSR Quality Checklist
Required
tests/census/*.sh,catalogue-check(diff clean),census-atlas.mjs check, atlas tests,theory-ledger verify,cohort.mjs check, applied testsjustis not installed in the sandbox)unsafeblocks.envfiles includedTesting
Not run here, with the reason for each:
just check:justis not installed.check-proofs: needs guix, agda, coqc and lean.claims-registry check: needsMATHESIS_STANDARDS.site-check: needs asciidoctor.One test in
tests/registry/fails becauseMATHESIS_STANDARDSis not set. It fails the same way on a cleanmain. CI must confirm the gates that did not run here.Generated by Claude Code