Repository navigation
Wave 3: fast certificate data builders (#177), release follow-ups (#187), and the Census windows as width-100 pieces (#168) - #191
Merged
Merged
Conversation
CensusCert4 (gramRange 4000 1000 = true) and CensusCert10 (gramRange 10000 1000 = true) were each one of_decide_eq_true over the whole window. Each is now proved from ten width-100 certificates, CensusCert40..49 and CensusCert100..109, joined by gramRange_append exactly as CensusCert7 is from CensusCert70..79. The pieces are CensusCert76 with the window start, the gramWin name and a fresh internal name changed; the glue is CensusCert7 with the window number changed. Statements and importers are unchanged; the Atlas root imports the twenty pieces (audit-atlas-exercise, R4). The cert4 shard elaborates the window-4 modules and cert4-replay replays them; census-a takes the window-10 pieces beside CensusCert10. The join compares 327 normalized records (was 267). RP-14's hint check names Census, the module that now dominates the verification. Atlas expected/build regenerated (check-golden --write). expected/verify follows in its own commit. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
expected/verify is what the join of run 39086315289 wrote for this tree's sources (a run of the Atlas jobs of ci.yml on a scratch branch whose join ran `verify-examples --write`): 347 normalized records, four for each of the twenty new modules beside the 267 before. The records of every unchanged module are byte-identical apart from the audit and probe names, which carry the new semantic ID. The hints of the 22 changed and new modules are that run's. The join's record count is 347, not the 327 the previous commit counted. VERIFICATION.md records the measurement: windows 4 and 10 elaborate in 111.5 s and 118.1 s and replay in 117.6 s and 115.4 s, at most 5.6 GiB per piece, with no Census process in swap. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
# Conflicts: # VERIFICATION.md
… and coverage (#187)
Precompute match arm terms and suffix lists in O(n) in certificate A's Writer::prepare_arms instead of rebuilding the arm suffix list across every arm_hit and arm_miss application. Propagate meta-cleanliness, loose-variable bounds, and minimum free-variable IDs bottom-up in Builder::push so resolve, abstract_over, lift, instantiate, instantiate_beta, substitute, and has_placeholder short-circuit closed/clean sub-DAGs in O(1). Scan match arms with a reverse cursor in Certificate B's Aligner::m, print certificate records directly via surface::core::print_module without round-tripping through canonical JSON, and reuse the cached native preservation library in correspondence_rules(). Restore the host-matrix timeout-minutes to 120.
# Conflicts: # VERIFICATION.md
…S-02 beside the stress arithmetic #189 restored the pre-train 120 minutes. Since then BS-02's differential runs in `cargo test --workspace` on every host (#190): the Intel macOS host took 140 minutes on wave 2's gate run. The comment's rule, twice the slowest observed time, gives 240 until this wave's run measures the host times with #177's fix in; the limit then follows them down. RP-14 exempts the host matrix from the gate-job limits, so no gate reads the number. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY
This was referenced Oct 18, 2026
Closed
This was referenced Oct 18, 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
3 participants
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.
Closes #177
Closes #187
Closes #168
Wave 3 after the train (#167) and wave 2 (#171): the three ready PRs that move no language identity and no compiler record, integrated on
main(d51d9f223) so that the gate runs once for the three. Each member's own gate was green on its own head; this head is theirs merged, with one resolved overlap and one hand change.Members
sp_021,374 s → 129 s,sp_08~1,600 s → 295 s,tc_05307 s → 53 s on the author's host; no test, assertion or certificate thinned, no record moves838b47c6bmerged; closes #177 on this run's host times (recorded there); #189 to be closed by hand with a pointercertificate-generation-limitfixture's peak size recorded; the threeLEXLEAN_AXDBG/LEXLEAN_SHOW*hooks are deleted andCL-17refuses any environment read outside §23.1 (planted); the leftover text and coverage of the train's member reviews (COSTS_B's derivation, binder hygiene for_root_.byte literals,MD-02reads all 8 artifact byte definitions,MD-13's unsigned 64-bit branch,SM-32'swidenWideroot at 2^63, the CHANGELOG counts)1e1a375d3merged; closes #187; #188 to be closed by hand with a pointerCensusCert4andCensusCert10proved from ten width-100 pieces each, joined bygramRange_append; statements unchanged; Atlas records from CI run 39086315289;cert425 → 2.7 min, Atlas 198 → 152 runner-minutes, noCensus*process swapsaf9f2638emerged; closes #168; #175 to be closed by hand with a pointerChanged at integration, by hand
VERIFICATION.md: Complete #167 release follow-ups: generation bounds, env audit, text, and coverage (#187) #188 rewrote the sentence on the SP-02 generation-bound record that Atlas: prove CensusCert4 and CensusCert10 from width-100 pieces (#168) #175's text still carried as context; the resolution keeps Complete #167 release follow-ups: generation bounds, env audit, text, and coverage (#187) #188's sentence and appends Atlas: prove CensusCert4 and CensusCert10 from width-100 pieces (#168) #175's section (## Census windows 4 and 10 as width-100 certificates) after Complete #167 release follow-ups: generation bounds, env audit, text, and coverage (#187) #188's new subsections..github/workflows/ci.yml, host matrixtimeout-minutes: Optimize certificate data builders and restore host-matrix timeout (#177) #189 restored 120 (the pre-train value, from 51–61 minutes observed). Since thenBS-02's differential runs on every host (BS-02's differential runs on every host of the matrix and costs the gate about 140 runner-minutes #190): the Intel macOS host took 140 minutes on wave 2's run. The limit is 240 on this PR, twice the slowest observed time as the comment's rule says; this run measures the new slowest time with [v0.4] Certificates as kernel data tripled the non-Lean conformance suite on every host: run the stress arithmetic once, or make the data builders fast #177's fix in, and the limit follows it down in the next PR that touches the workflow. RP-14 exempts the host matrix from the gate-job limits, so no gate reads the number.Checked locally on this head
cargo fmt --check,clippy -D warnings,validate-model,validate-spec-links,check-test-inventory,ci-shards,check-golden, thelexlean(200) andxtaskunit tests, and the members' cases:cl_17,md_02,md_13,sm_32,sp_02(1,707 s on this host, against 7,951 s for the train's tree on the same host),sp_08(1,466 s),sp_10,sp_12,tc_05,rp_14,au_09,au_10,vr_19. The whole gate runs in CI on this head; its host times are the acceptance measurement of #177.How this merges
The head contains
main(d51d9f223). It is ready on its final head; the merge is a merge commit pinned to it, and the push run onmainruns nothing when this PR's run passed every job (#166). Merged by the maintainer on the owner's rule: green gate and the linked issues' DoD met.Generated by Claude Code