Repository navigation
census: partial refresh with provenance; reconciliation targets - #24
Open
hyperpolymath wants to merge 4 commits into
Open
hyperpolymath wants to merge 4 commits into
hyperpolymath wants to merge 4 commits into
Conversation
Add a sanctioned partial census refresh. `run-census.sh --merge FILE` (`just census-merge`) censuses only the listed repositories and merges them into the committed data with the new `scripts/census/merge-rows.sh`. Records outside the list are kept byte for byte, so the catalogue no longer has to be rebuilt from all 476 repositories to refresh a few. Record provenance. `census-repo.sh` now notes the commit it read, and every run writes `docs/catalogue/census/provenance.json` with each repository's commit and the UTC date. Test and wire it. `tests/census/merge-rows.test.sh` (`just census-test`) has 13 cases, seven of them fail-closed; a planted defect in the merge fails 6 of them. CI now runs it with the catalogue freshness check. Use it for the 17 repositories in AffineScript's completion plan. Eight rows changed; out-of-scope rows are untouched. The rows match an independently derived candidate. Add those repositories to the cross-prover reconciliation targets and register, from local canonical-flag runs on 2026-11-09. Those runs used Agda 2.6.3 and are not home-repo receipts, so every status stays at AGDA-PENDING or earlier and no grade is derived. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjbCwy9iYWY9vKgzGW
|
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 23 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. |
Use [[ ]] for the new conditionals and copy positional parameters into named locals in the test helpers (S7688, S7679). Behaviour is unchanged: 13/13 tests pass, and a planted merge defect still fails 6 of them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjbCwy9iYWY9vKgzGW
Re-checked with Lean 4.15.0 installed from releases.lean-lang.org: StackcertCore.lean has type errors in the proof of cert_sound. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjbCwy9iYWY9vKgzGW
The committed map predates applied-systems/, so the estate-rules repo-map determinism test fails on main (a3dbe73) as well as on this branch. Regenerated with scripts/gen-repo-map.sh; the test now passes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjbCwy9iYWY9vKgzGW
Owner
Author
|
Generated by Claude Code |
|
Owner
Author
|
Bringing the deed level means adopting the canon's new Generated by Claude Code |
hyperpolymath
marked this pull request as ready for review
November 9, 2026 15:47
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
hyperpolymath
added a commit
to hyperpolymath/affinescript
that referenced
this pull request
Nov 10, 2026
#787) This follows the merged completion plan, #786. I re-ran every prover that could be installed, and judged each proof against `metadatastician/standards` `3-practice/PROOF-POLICY.adoc` at commit `9bdf864`. ## What changed - **Proof ledger**, in `docs/EXPLAINME.adoc`. The README-EXPLAINME standard requires one whenever a repo claims proofs, and this repo had none. It is keyed to the obligation IDs in `docs/PROOF-NEEDS.adoc` and has 22 rows: 7 `proven`, all of them about models rather than the shipped code; 13 `open`; and 2 `argued`. No theory theorem has a proof witness grade, because none has an Agda source. - **Solo core status.** `docs/SOUNDNESS.adoc` and `docs/PROOF-NEEDS.adoc` still said the Solo core's progress and preservation were `?todo`. Both now check under Idris2 0.7.0 and are total. That was a local check; no CI job runs it yet. - **PROOF-NEEDS caveats.** P-3, P-4 and the K-1 real-lift text now say they hold for models only. F-5 records the real `render_ty` counterexample and stays open. - **Plan proof route.** The completion plan's proof route was Coq-first. It is now aligned with the policy: theory goes in Agda with Rocq and Lean rechecks, and engineering goes in Idris2 or under a recorded §4 exception. There is a new section 5.0 and corrected rungs. - **Plan findings and rulings.** Workflow W7 is corrected. The plan also gains the verified per-repo results, new cross-repo items, and owner questions 16 to 19 with the owner's rulings of 2026-11-09. - **Idris2 0.8.0 results and provisioning fix** (`19084c8`). - typed-wasm passes `tools/check-kernel-proofs.sh` in full under its pinned Idris2 0.8.0 (`15a3e4e`). The plan's `Region.idr` item is closed. - januskey and absolute-zero type-check under the 0.8.0 release. - New estate item: the Idris2 repos check against three different compilers. typed-wasm uses the v0.8.0 tag, januskey and absolute-zero use a pack image built from Idris2 `main`, and anytype uses 0.7.0. - The W0 recipe now passes `PREFIX` to `make bootstrap` as well as to `make install`. Without that, Idris2 type-checks but cannot run programs, and still exits 0. ## New holes - **H20.** `Face.render_ty` is not injective. On the Js face, `List[Option[Int]]` and `Option[List[Int]]` both render as `List[Int] | null`; on Cafe both render as `List[Int]?`. I observed this by calling the built library. The Coq F-5 theorem proves the opposite, but for a model that differs from the code. - **H21.** The Coq proof gate covers only 96 of the 137 assertions. A planted `Admitted` false lemma and a planted `Axiom False` both passed a replica of the gate. - **H22.** The 23 staged Agda files under `proposals/` pass the canonical flags, but nothing runs them. `tools/check-proofs.sh --agda` reports SKIP when its environment variables are unset. ## Proof review results - **Coq.** All 20 files build under Coq 8.18, and all 137 assertions are closed under the global context. Several headline theorems hold by definition: P3 borrow soundness, F3, F4, F1 `same_cube`, and `QttTyping.usage_soundness`. The `Real*` models differ from `lib/codegen.ml`. - **Idris2 Solo core.** It checks, and `progress` and `preservation` are total. - **Lean, installed with the owner's approval from `releases.lean-lang.org`.** - tropical-types builds all 20 modules at its 4.13.0 pin. Its 334 theorems use no `sorry`, no Mathlib and no `Classical.choice`. - occupancy's `stackcert` does not compile at its 4.15.0 pin. - This repo's copy of the tropical file compiles at 4.13.0. - **Not re-run.** CI's Coq 8.20.1 was not re-run. ## Checks - `bash tools/check-doc-truthing.sh`: OK - `bash tools/check-soundness-ledger.sh`: all 5 properties hold. It ran on deepened history. - `asciidoctor --failure-level=WARN` on all four files: clean Companion change in mathesis: hyperpolymath/mathesis#24. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01J4QvDjbCwy9iYWY9vKgzGW --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
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 could only rebuild the whole catalogue from all 476 repositories, so it could not refresh a few repositories without disturbing the rest. This adds a sanctioned partial refresh with per-repository provenance and uses it for the 17 repositories in AffineScript's completion plan. It also adds those repositories to the cross-prover reconciliation targets and register.
Changes
scripts/census/merge-rows.sh(new): replaces, removes or adds records only for the listed repositories. Every other record is kept byte for byte. It fails closed on bad input, duplicates or an empty scope.scripts/census/run-census.sh --merge FILEandjust census-merge FILE: census only the listed repositories, then merge rows, unreachable entries and provenance.census-repo.shrecords the commit it read. Every run writesdocs/catalogue/census/provenance.jsonwith repository, commit and UTC date.tests/census/merge-rows.test.shandjust census-test: 13 cases, seven of them fail-closed. CI (proven-tests.yml) now runs these tests and the catalogue freshness check, which was not wired before.docs/status/CROSS-PROVER-RECONCILIATION.adoc: added targets and register rows for echo-types, secret-types, epistemic-types, residual-evidence-types, choreographic-types, occupancy-types, absolute-zero, januskey and affinescript. They come from local runs underagda --safe --without-K --cubical-compatibleat Agda 2.6.3. These are not home-repo receipts, and four of these repos pin 2.6.4.3, so every status stays atAGDA-PENDINGor earlier and no grade is derived.RSR Quality Checklist
Required
just testitself exits 127 on both the base and this branch, because idris2 and zig are not installed; that failure is unrelated to this change.unsafeblocks without// SAFETY:comments.envfiles includedAs Applicable
(status)/(maturity)updated: not changedCHANGELOGor release notes updatedTesting
bash tests/census/merge-rows.test.shrender-catalogue.shdiff)bun scripts/atlas/census-atlas.mjs checkbun test tests/atlas/census-atlas.test.mjsscripts/check-ijson-jcs.sh --enforce .scripts/check-adoc-renders.sh .The refreshed rows also match a candidate produced independently, with a one-off merge command, before this tooling existed.
Not done here
repos.jsonwas not refreshed, so repositories created since the first census are still missing.Generated by Claude Code