You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
chore(census): refresh the row of system-et (the Agda track is now on its main branch) - #48
The catalogue row of hyperpolymath/system-et was from 2026-11-06: 21 Lean files and no Agda file. The wager experiment in Cubical Agda is on the main branch of that repository since 2026-11-10 (stages 0 to 4). This pull request refreshes that one row and renders the catalogue and the atlas again.
Changes
docs/catalogue/census/catalogue-rows.json: the row of hyperpolymath/system-et, from scripts/census/update-rows.sh hyperpolymath/system-et, at the commit 04a8b6e of that repository.
Field
Before
After
Own proof files
21
86
Provers
lean 21
agda 65, lean 21
Declarations
164
612
Holes, axioms
0, 0
0, 0
Status file
docs/status/PROOF-NEEDS.adoc
docs/status/PROOF-STATUS.adoc
docs/catalogue/catalogue.adoc and the 4 files in docs/atlas/generated/: rendered again from the rows.
The render removes a second line for metadatastician/hvn-dehallucinator. The committed catalogue had 2 lines for that repository, and the rows have 1, so catalogue-check failed on main. The rows are the source. The removed line named PROOF-STATUS.adoc as the status file; the row names PROOF-NEEDS.adoc.
Not in this pull request
The row of metadatastician/hvn-dehallucinator is not changed. A trial refresh gave: 19 own files, 640 declarations, status file docs/status/PROOF-STATUS.adoc, and 1 hole. The hole is a false positive of scripts/census/proof-holes.sh: the word "admit" in the comment /-! The evidence contexts admit the same worlds -/ (verification/proofs/lean4/Haruspex.lean, line 882). I did not commit a row that says "1 hole" for it. The scanner needs a repair at its source before that row is refreshed.
Stages 5 to 7 of the wager experiment are not in the row. They are in pull request 89 of system-et, which is open. The census reads the main branch. After that pull request is merged, the row needs one more refresh (79 Agda modules).
No claim of the wager experiment is in the claims registry (docs/registry). A claim needs a receipt in the home repository (ADR 0004), and system-et has none.
No full census. Only the named repository was read.
RSR Quality Checklist
Required
Tests pass (just test or equivalent). just is not available in the session. Run in the session: the catalogue check (PASS), bun scripts/atlas/census-atlas.mjs check (PASS), bun test tests/atlas/census-atlas.test.mjs (10 pass), bash tests/census/build_rows_status_test.sh (PASS).
Code is formatted. Not applicable: generated data and views only.
Linter is clean (no new warnings or errors)
No banned language patterns
No unsafe blocks without // SAFETY: comments (none exist)
No banned functions
SPDX license headers present on all new/modified source files (no new file)
No secrets, credentials, or .env files included
As Applicable
Repo deed (status) / (maturity) updated. Not applicable.
Repo deed (ecosystem) updated. Not applicable.
Repo deed (meta) and/or docs/decisions/ updated. Not applicable.
docs/status/ROADMAP.adoc updated. Not done: no milestone changes.
Documentation updated for user-facing changes. Not applicable.
TOPOLOGY.md updated. Not applicable.
CHANGELOG or release notes updated. Not done: a data refresh.
New dependencies reviewed for license compatibility. Not applicable.
ABI/FFI changes validated. Not applicable.
Testing
The rows file differs from main in 1 row (a comparison of the 248 rows, one by one).
The rows file has the byte form that the census script writes (jq -cS).
The catalogue check fails on main (the second line for one repository) and passes on this branch.
Not run: the registry check (it reads receipts in other repositories), the full census.
… its main branch)
The row of hyperpolymath/system-et was from 2026-11-06: 21 Lean files
and no Agda file. The wager experiment in Cubical Agda is on the main
branch of that repository since 2026-11-10 (stages 0 to 4).
`scripts/census/update-rows.sh hyperpolymath/system-et` gives, at the
commit 04a8b6e of that repository: 86 own proof files (agda 65,
lean 21), 612 declarations, 0 holes, 0 axioms, status file
docs/status/PROOF-STATUS.adoc.
The catalogue and the 4 atlas views are rendered again from the rows.
The render also removes a second line for
metadatastician/hvn-dehallucinator. The committed catalogue had 2 lines
for that repository and the rows have 1, so `catalogue-check` failed on
main. The rows are the source; the catalogue says "do not edit by
hand". The removed line named PROOF-STATUS.adoc as the status file,
and the row names PROOF-NEEDS.adoc. The row of that repository is not
changed here: a trial refresh gave 1 hole that is a false positive of
the scanner (the word "admit" in a comment).
Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK
The catalogue adds system-et to the Theory table with updated counts and a proof-status link. It removes the former Engineering entry and changes the hvn-dehallucinator proof-status link.
Changes: Catalogue census and links
Layer / File(s)
Summary
Catalogue census and status links docs/catalogue/catalogue.adoc
The Theory table lists system-et with 86 files and 612 declarations. Its former Engineering entry is removed. The hvn-dehallucinator link changes from PROOF-STATUS to PROOF-NEEDS.
The title clearly identifies the census refresh for system-et and notes that its Agda track is now on the main branch.
Description check
The description includes the required Summary, Changes, checklist, Testing, and Screenshots sections. It explains the data changes and scope, and reports which checks passed and which were not run.
Docstring Coverage
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentat…
Linked Issues check
Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check
Check skipped because no linked issues were found for this pull request.
Full details: Docstring Coverage
Explanation
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 0 functions across 0 files. (1 skipped: 1 unsupported.)
Finishing Touches
Generate unit tests (beta)
Commit to this branch
Create a new PR
Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
Warning
Review coverage is incomplete: 1 file could not be fully reviewed. Findings from completed review steps are included; see review info for 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.
Reviewing files that changed from the base of the PR and between 8ee6354 and 6e9180e.
Files ignored due to path filters: 4
docs/atlas/generated/az.adoc is excluded by !**/generated/**
docs/atlas/generated/classes.adoc is excluded by !**/generated/**
docs/atlas/generated/index.json is excluded by !**/generated/**
docs/atlas/generated/organisations.adoc is excluded by !**/generated/**
Files selected for processing: 2
docs/catalogue/catalogue.adoc
docs/catalogue/census/catalogue-rows.json
Files not fully reviewed because their changes were unavailable: 1
docs/catalogue/census/catalogue-rows.json
Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review.
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
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 catalogue row of
hyperpolymath/system-etwas from 2026-11-06: 21 Lean files and no Agda file. The wager experiment in Cubical Agda is on the main branch of that repository since 2026-11-10 (stages 0 to 4). This pull request refreshes that one row and renders the catalogue and the atlas again.Changes
docs/catalogue/census/catalogue-rows.json: the row ofhyperpolymath/system-et, fromscripts/census/update-rows.sh hyperpolymath/system-et, at the commit04a8b6eof that repository.docs/status/PROOF-NEEDS.adocdocs/status/PROOF-STATUS.adocdocs/catalogue/catalogue.adocand the 4 files indocs/atlas/generated/: rendered again from the rows.The render removes a second line for
metadatastician/hvn-dehallucinator. The committed catalogue had 2 lines for that repository, and the rows have 1, socatalogue-checkfailed onmain. The rows are the source. The removed line namedPROOF-STATUS.adocas the status file; the row namesPROOF-NEEDS.adoc.Not in this pull request
metadatastician/hvn-dehallucinatoris not changed. A trial refresh gave: 19 own files, 640 declarations, status filedocs/status/PROOF-STATUS.adoc, and 1 hole. The hole is a false positive ofscripts/census/proof-holes.sh: the word "admit" in the comment/-! The evidence contexts admit the same worlds -/(verification/proofs/lean4/Haruspex.lean, line 882). I did not commit a row that says "1 hole" for it. The scanner needs a repair at its source before that row is refreshed.docs/registry). A claim needs a receipt in the home repository (ADR 0004), and system-et has none.RSR Quality Checklist
Required
just testor equivalent).justis not available in the session. Run in the session: the catalogue check (PASS),bun scripts/atlas/census-atlas.mjs check(PASS),bun test tests/atlas/census-atlas.test.mjs(10 pass),bash tests/census/build_rows_status_test.sh(PASS).unsafeblocks without// SAFETY:comments (none exist).envfiles includedAs Applicable
(status)/(maturity)updated. Not applicable.(ecosystem)updated. Not applicable.(meta)and/ordocs/decisions/updated. Not applicable.docs/status/ROADMAP.adocupdated. Not done: no milestone changes.TOPOLOGY.mdupdated. Not applicable.CHANGELOGor release notes updated. Not done: a data refresh.Testing
mainin 1 row (a comparison of the 248 rows, one by one).jq -cS).main(the second line for one repository) and passes on this branch.Screenshots
Not applicable.
Generated by Claude Code
Summary by CodeRabbit
hyperpolymath/system-etunder Theory, with its current file and declaration counts and proof-status link.hvn-dehallucinatorproof-status link to point toPROOF-NEEDS.adoc.