Repository navigation
Integrate CBZ-0 runbook batch 2: the federation drift crawler (#712, #716, #723, #725) and #715 - #731
Merged
Merged
Conversation
tools/cbz_drift/crawl.py discovers the federation at run time from the workspace seed: .gitmodules, gitlinks, pins.json, workspace/repositories.json, the registry named under canonical_inputs, every Lean package and every lake dependency on a reachable repository. Nothing about the topology is hardcoded, and --clone-into lets a job start from the seed alone. It blocks when two records of one identity disagree: pin sources, missing or off-line pins, registry artifact bytes and SHA-256, and the source interface of any Lean declaration declared in more than one crawled location (statement for theorems, statement and value for definitions; lexical domain in tools/cbz_drift/README.md). A record lagging a moving tip is INFO. Unreadable repositories, manifests and Lean files fail closed. tests/test_cbz_drift.py builds synthetic git federations and runs 43 tests in both interpreter modes; 35 source mutants are each killed by their designated assertion, with the unmutated copy as harness control. The new workflow runs the self-test, then crawls with main overridden to the candidate head at pins and at tips. Observed now: 9 repositories, 0 BLOCK, 592/592 registry artifacts verified, and all 482 Lean names declared in more than one place agree; the cold-start crawl from the seed alone matches. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3
Remove static PR path filtering and exercise the subscription guard in both self-test modes. Preserve the crawl and other triggers. Record the original RED result, comment-hidden-filter repair, bounded review and remaining PR #712 defects. Actual executor: OpenAI/Codex 01a11c48-e9e4-7113-a03f-24b2155da25e.
Emit INPUT-MISSING with label/repository/selected-ref/path, preserving explicit historical input refs and optional discovery semantics. Add nine real-Git regression controls, retaining the original R3 witness with provenance. Implemented by OpenAI Codex subagent cbz712_r3_registry_repair_20261029 under owner delegation. Engineering scope; scientific effect NONE. Original six qualification cases remain preserved; five unrelated defects remain open. No hosted success claimed.
R1: the crawl is now a breadth-first fixed point. Every reached repository's own .gitmodules, gitlinks, pins.json, repositories.json, canonical inputs and lake manifests are read and whatever they name is reached in turn; every reached repository is then validated and scanned once. Lake dependencies outside the federation's owners are counted, not crawled. R2 follows from moving the lake handling: an absent lake revision is PIN-MISSING. R4: --fetch refreshes each repository from origin before reading a default tip; a failed refresh is FETCH-FAILED. Adds 01a103c8's adversarial file byte-identical from 9a5d313 (red at fe676eb, green here), 11 designated tests and 8 mutants; mutant children now follow the parent's interpreter mode. 66 tests OK in both modes, 43/43 mutants killed. Real federation: 0 BLOCK at pins and tips. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3
…723 DCL P1, P2) A git lake package with a missing, empty or non-string rev was skipped before the revision guard (a silent false negative), and a non-string rev crashed. Both are now PIN-MISSING bound to repository, manifest, target and pin; the dependency is still reached. A git package without a usable URL is MALFORMED. The missing-revision test now asserts that identity. 68 tests OK in both modes; 46/46 mutants killed by designated assertions (3 new). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3
The Lean extractor compared only a declaration's own text, which missed three cases: - two copies of a statement under different `variable` or `open` commands compared equal; - so did a definition whose tactic block uses `set_option … in` or `open … in`; - a `mutual` block raised a false LEAN-SYNTAX. These are counterexamples C1, C1b, C2, C3, C3b and C4 from #712/6511042057. - The interface now carries the `open`, `variable`, `universe`, `export`, `include` and `omit` commands in scope, and any `… in` prefix. - `open … in` and `set_option … in` stay in a declaration unless they start a line that is not indented deeper than it. - `mutual … end` is a scope. Stacked on #723 (e666f48), in the order the #712 author proposed: #716, then #723, then this, then #715. lean_decls.py is unchanged by #716 and #723, and only the README's mutant count conflicted. Tests: 72 across test_cbz_drift, the adversarial file and the canonical-input file (#723's 68 + 4), OK in normal and -O mode. The harness kills all 58 mutants (#723's 46 + 12) by their designated assertions. The "depth ignored" locator is reconciled to the new header check, with the same meaning and the same designated test. Live federation: - No declaration list changed across 338 Lean file reads, and no declaration's own interface changed. - 5,579 of 6,069 declarations gain a context. - #723's crawl, with --fetch, finds identical findings and statistics before and after: 0 BLOCK and 0 LEAN-DRIFT, at the pins and the tips. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01SHCrxvZuVwzVNC7SDC9TAj
…ages block Two latent gaps from the #723 requalification (#723/6538582448): - An in-federation git package whose rev was HEAD, a branch, a tag, a short or uppercase SHA, or <sha>~0 resolved through cat-file and was reported only as INFO LAKE-DEP. Now any rev that is not a full 40-hex commit id is BLOCK PIN-MISSING, with the same identity binding. - A packages value that is not a list, an entry that is not an object, a package type other than git or path, and Lake's older nested format were skipped with no finding and no edge. Now each is BLOCK MALFORMED. Path packages are still skipped, as before. Neither occurs in the federation today: all 7 lake manifests at the pins and tips are version 1.2.0 lists of git and path packages, and every git rev is a full lowercase commit id. Tests: test_lake_floating_revision_blocks (7 revs) and test_unreadable_lake_packages_block (6 shapes and a path-package control). Mutants: "floating revision accepted", "unknown package shape skipped" and "unreadable packages list skipped"; the "revisionless package skipped" locator follows the new condition. 74 tests OK in normal and -O mode; the harness kills all 61 mutants by their designated assertions. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01SHCrxvZuVwzVNC7SDC9TAj
…fication P2) The self-test ran only test_cbz_drift, so 01a103c8's adversarial R1-R4 cases and #716's R3 tests never ran on hosted CI (#723/6538582448). The command now names all three modules present on this stack; #715's trigger module joins when #715 is composed. 74 tests OK in normal and -O mode; 61/61 mutants killed by designated assertions. Live crawl with --fetch: 0 BLOCK at pins and tips. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3
The slice B patch posted for composition (#684/6534866575) carried the evidence README but not the five logs it names, so #725 has the README alone. These are the exact bytes from the original slice B commit 045d0bee: the counterexample before-and-after runs, the live extraction and crawl summaries, and the 72-test runs in normal and -O mode. They record slice B as committed, before the lake-pin hardening. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01SHCrxvZuVwzVNC7SDC9TAj
Conflicts, resolved three-way from the common base #712 (15e8f68): the workflow takes #715's removal of the pull-request path filter and runs the union of both sides' test modules (#725's two and #715's one, besides the base module); DECISIONS.md keeps main's complete ledger and appends #715's single row at the end. Scientific effect: NONE. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01V3DF6ms7UTpj27UqDG4u5h
d6g8k5htny-coder
marked this pull request as ready for review
October 31, 2026 19:38
This was referenced Oct 31, 2026
Owner
Author
|
LANDED — #731 is
Generated by Claude Code |
This was referenced Oct 31, 2026
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.
Integration batch 2 for the CBZ-0 runbook, row 5 (#684/6538797729). It lands Claude017's federation drift crawler, the addendum's G7 tool, together with its CI trigger, as one composed unit on current main. Each unit's head is a parent of a merge commit here, so GitHub marks #712, #716, #723, #725 and #715 merged when this lands.
Units
da5ff070(the stack's top; its ancestry is linear)0768d66f(based on #712)Review and evidence
e666f48bby 01SHCrxv (#723/6538582448).Composition, checked natively
--no-ffonto main3dc63c7d.15e8f689):.github/workflows/cbz-federation-drift.yml: ci: run federation drift on every pull request #715's removal of the pull-requestpaths:filter, plus the union of both sides' test modules (test_cbz_drift,test_cbz_drift_adversarial_01a103c8,test_cbz_drift_canonical_input,test_cbz_drift_pr_trigger_01a11c48).DECISIONS.md: main's complete ledger, with ci: run federation drift on every pull request #715's single row appended at the end. The diff against main is exactly that one added line.test_future_topology_inputs_cannot_be_excluded_before_discoverycaught it, and the commit was amended before any push.Tests on the composed tree
All run with CPython 3.11.17.
-Omode.pinsandtips. INFO findings: PIN-STALE 4, and REGISTRY-EVOLVED 31 at pins and 32 at tips. It covered 3,039 Lean declarations in 172 files, and verified 592 registry artifacts.Not claimed
Scientific effect NONE. This is engineering integration only. It is not G7's final admission, since the lexical signatures carry the stated limits on notation and macros. It makes no CLOSED promotion and no CBZ-0 claim.
Generated by Claude Code