Repository navigation
fix(census): comment-aware proof-holes.sh, Idris2 undefined-declaration axioms; refresh 13 rows - #27
Open
hyperpolymath wants to merge 4 commits into
Open
hyperpolymath wants to merge 4 commits into
hyperpolymath wants to merge 4 commits into
Conversation
…rows proof-holes.sh matched markers line by line and skipped only lines that start with a comment, so prose inside multi-line comments (for example "no new [Admitted.]") was counted as a hole, and a marker after a closed comment on the same line was missed. It now matches against a copy of each file with block comments (nested), line comments and simple string literals blanked out, keeping line numbers and Agda/Idris pragmas. Evidence: on 16 local repos the change adds no finding and removes 9, each a marker that appears only in a comment (6 in ephapax, 2 in absolute-zero, 1 in tropical-types). tests/census/proof_holes_comments_test.sh plants 14 markers in code across Rocq, Agda, Idris2, Lean, Creusot, SPARK and Isabelle plus decoys in comments and strings; the new scanner reports exactly the 14 and the old one misses the inline Admitted. The test is wired into estate-rules.yml. Census: the 13 rows in this session's repository scope were re-run with census-repo.sh and merged; docs/catalogue/census/refreshes.json records which rows and why, and the catalogue prints it. ephapax drops from 15 holes to 0 after the D0/D0b retirement (hyperpolymath/ephapax#422). Atlas regenerated; catalogue-check, atlas check and tests, ijson-jcs and adoc render checks pass. The comment-blanking pass is a local change to a copy of the proof-craft skill's scanner and needs carrying back to the skill. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY
|
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 29 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. |
…ates Idris2 0.8.0 accepts a top-level type signature that has no clauses and treats it as a postulate, even under %default total: `0 bad : Void` lets a module prove `1 = 2` with no warning (checked by hand). proof-holes.sh did not see these, so a repo could hold postulates and still report 0 axioms. scripts/census/idris2-undefined.awk now reports such signatures, on the comment-blanked copy, as class `axiom`, marker `undefined declaration`. Signatures after %foreign/%extern are FFI and are not reported; infix (backtick) clauses count as definitions. Evidence: across all .idr files in the Idris2 0.8.0 libs (base, contrib, linear, network, papers, prelude, test) it reports nothing. In ephapax it finds the 12 erased declarations of src/abi (Invariants.idr x11, Foreign.idr x1), which the ABI documents as "erased postulates". The census test now plants one, plus an FFI signature and an infix definition that must not be reported (15 markers). The 13 in-scope rows were re-run from one clean pass (an earlier pass lost rows when the disk filled): ephapax now shows 0 holes, 12 axioms. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY
hyperpolymath
changed the title
estate-rules failed on ec833bc at "Repository map generates identically across locales": the committed map predates applied-systems/ (added on main in 1058bb8, 2026-11-07, without a regeneration). origin/main (a3dbe73) fails the same test, so this is inherited, not caused by the census change; tests/census/ is not listed in the map. This is the output of `bash scripts/gen-repo-map.sh .`, unedited, and is a no-op once main carries the same regeneration. Verified: tests/shape/repo_map_determinism_test.sh fails before and passes after; the remaining estate-rules steps that the red step had masked also pass locally (root shape, no-md, adoc renders with asciidoctor 2.0.26, no-vlang, no-a2ml, the new census comment test, deed clause, mint tests with just 1.43.0, template conformance, governance, ijson-jcs --enforce, required contexts). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY
Canon lockstep fails on main (a3dbe73) and on this PR: the deed pins canon 2.1.3, while metadatastician/standards main canon.lock is 2.1.5 (gate table 0.3.1). This ports f22faaf from #29 unchanged: :version "2.1.5" and :gates-sha256 5c510bba…; criteria-sha256 is unchanged. The resulting blob equals #29's (ddb2e29), so this is a no-op once #29 lands. Verified against the live canon.lock: [canon] version 2.1.5, gates sha256 5c510bba…, criteria 6a5aa885…; the gates file on standards main hashes to 5c510bba…. The lockstep job's own compare step, run locally, passes on all three pins. validate-deed.sh with deed_lint.js at the pinned standards 8e48b1c reports 2 files, 0 failing; deed_clause_test, root shape, template conformance and governance tests pass. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY
Owner
Author
|
CI status for the two red checks on ec833bc:
Generated by Claude Code |
|
hyperpolymath
marked this pull request as ready for review
November 9, 2026 15:41
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
This PR fixes three problems with
scripts/census/proof-holes.sh:(* c *) Lemma a : False. Admitted..%default total. I checked this by hand:0 bad : Voidlets a module prove1 = 2with no warning. The scanner never saw these.What changes:
scripts/census/idris2-undefined.awkreports top-level Idris2 signatures that have no clauses, as classaxiomwith markerundefined declaration. Signatures after%foreign/%externare FFI and are not reported. Backtick infix clauses count as definitions.The 13 census rows in this session's repository scope are re-run with the fixed scanner. For ephapax: 0 holes (it was 15, all prose in comments, after its D0/D0b retirement in hyperpolymath/ephapax#422), and 12 axioms. The 12 are the erased declarations in
src/abithat its ABI documents as "erased postulates".Changes
scripts/census/proof-holes.sh:scripts/census/idris2-undefined.awk(new).tests/census/proof_holes_comments_test.sh(new, wired intoestate-rules.yml):docs/catalogue/census/catalogue-rows.json: the 13 in-scope rows are re-run from one clean pass (an earlier pass lost rows when the disk filled). Repo order is unchanged.docs/catalogue/census/refreshes.json(new) records which rows were re-run and why, andrender-catalogue.shprints it under the intro.docs/catalogue/catalogue.adocanddocs/atlas/generated/*are regenerated.RSR Quality Checklist
Required
tests/census/proof_holes_comments_test.sh: PASS;bun test tests/atlas/census-atlas.test.mjs: 10 pass.bash -n)unsafeblocks without// SAFETY:comments (n/a)scripts/check-escape-hatches.shpasses..envfiles includedAs Applicable
Testing
.idrfile in the Idris2 0.8.0libs/tree (base, contrib, linear, network, papers, prelude, test): 0 reports..idrfiles: only the 12 ephapax declarations.%foreignsignatures that come after modifier lines, and backtick infix definitions. Both are fixed and covered by the test.Admittedand the undefined declaration.census-atlas.mjs check: PASS;check-ijson-jcs.sh --enforce: 5/5 canonical;check-adoc-renders.sh: PASS;check-lock-sync.sh,check-root-shape.sh: PASS.Not done
run-census.shfixes both.engineeringby the first-pass heuristic, because it has more Idris2 files than Rocq files. The owner has since ruled its soundness statements theory (No-False gate hardening, D0/D0b status sync, and the W0 wave (E0/E1 holes, probes, aLib conformer) ephapax#425).🤖 Generated with Claude Code
https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY