Repository navigation
chore(census): refresh the row of system-et (the wager proofs are on its main branch) - #60
Merged
Merged
Conversation
…its main branch) The wager proofs merged into the main branch of system-et (pull request 89) after the row was taken this morning. The row said 86 proof files and 612 declarations. The main branch now has more. `scripts/census/update-rows.sh hyperpolymath/system-et` (the script of `just update-rows`) took the row again: - proof files: 86 to 102 (agda 65 to 80, lean 21 to 22) - declarations: 612 to 773 - holes, axioms, unsafe flags, policy files: 0, as before The count of the scanner includes project files. Of the 102 files, 79 are `.agda` and 20 are `.lean`; the other 3 are the `.agda-lib` file, `lakefile.toml` and `lean-toolchain`. `bun scripts/atlas/census-atlas.mjs build` made the atlas views again from the same rows. Only the row of system-et changes, 1 line in each of the 6 generated files. `docs/status/ROADMAP.adoc` records this change under "Open census work", as the rule for census data says. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK
|
hyperpolymath
marked this pull request as ready for review
November 10, 2026 19:32
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 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 row of
hyperpolymath/system-etwas out of date. The wager proofs merged into the main branch of system-et (pull request 89, 2026-11-10 17:16 UTC) after the row was taken this morning (#48). This pull request takes the row again.This is the 1 open pull request that changes census rows.
docs/status/ROADMAP.adocrecords it under "Open census work", as the rule "One writer for census data" says. The other open pull request (#59) changes no row.Changes
docs/catalogue/census/catalogue-rows.jsonanddocs/catalogue/catalogue.adoc: written byscripts/census/update-rows.sh hyperpolymath/system-et. This is the script ofjust update-rows.justis not installed in the session, so I ran the script directly, with the same argument.docs/atlas/generated/(4 files): written bybun scripts/atlas/census-atlas.mjs build, from the same rows.docs/status/ROADMAP.adoc: the record under "Open census work".No row was edited by hand. Only the row of system-et changes: 1 line in each of the 6 generated files.
What the numbers count. The scanner counts project files also. Of the 102 files, 79 are
.agdafiles and 20 are.leanfiles. The other 3 are the.agda-libfile,lakefile.tomlandlean-toolchain. The scan read system-et atbbe1d13, and its list of.agdaand.leanfiles is equal to the list on that commit (99 files).RSR Quality Checklist
Required
just testwas not run (nojustin the session)..envfiles includedunsafeblocks, banned functions, SPDX headers. No source file changes.As Applicable
docs/status/ROADMAP.adocupdatedTesting
Run locally at
b704582:bash scripts/census/render-catalogue.sh docs/catalogue/census | diff -u docs/catalogue/catalogue.adoc -(thecatalogue-checkrecipe): no difference, exit 0.bun scripts/atlas/census-atlas.mjs check:PASS: generated atlas matches census.bun test tests/atlas/census-atlas.test.mjs: 10 pass, 0 fail.bash tests/census/build_rows_status_test.sh: pass.bash scripts/check-ijson-jcs.sh --enforce: 17 files checked, 17 canonical.Not verified:
Generated by Claude Code