Repository navigation
Atlas: prove CensusCert4 and CensusCert10 from width-100 pieces (#168) - #175
4 commits merged into
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
|
Maintainer: this PR's head Generated by Claude Code |
|
Landed through wave 3, #191, merged to Generated by Claude Code |
…0-slice2 The merged tree is main plus the slice-2 sources; generated records are regenerated next. Main moved no version field since 193cd21, so the combined semantic_ir 14, lean_backend 20, latex_backend 13 stand. The register is 414 on main plus LM-04..LM-06: 417, set by hand in README, the SPEC §31 total, repository.rs and spec_links.rs. CHANGELOG keeps both entries. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 participants
Closes #168.
CensusCert4andCensusCert10each proved a whole width-1,000 census window with oneof_decide_eq_true. Both ran out of memory on the standard runner. On main run 39054719580,CensusCert4took 1,419 s to elaborate and 2,249 s to replay, at about 15 GiB with 3.5 GiB of swap.CensusCert10reached 14.3–14.7 GiB and also swapped.This PR splits each window into ten width-100 certificates,
CensusCert40–49andCensusCert100–109, joined bygramRange_append. That is howCensusCert7is already built fromCensusCert70–79.What changes
CensusCert76with three things changed: the window start, thegramWinname, and a fresh internal name (decl1715–decl1734). Each glue module isCensusCert7with the window number changed. The statements ofCensusCert4andCensusCert10are unchanged, andCensusCompleteandAtlasimport them as before. The Atlas root also imports the twenty pieces (audit-atlas-exercise, R4)..github/verify-shards.json:cert4now elaborates the window-4 modules andcert4-replayreplays them.census-atakes the window-10 pieces besideCensusCert10. The job list inci.ymlis unchanged. The new hints come from CI.Census, which is now the module that dominates.language/orcrates/lexleanchanges, so no language identity moves.check-goldenrewrote onlyexamples/uor-atlas/expected/build.How
expected/verifywas produced. On the shared WSL, a local Atlas regeneration ran out of memory, so the records come from CI instead. A scratch branch,claude/atlas-cert4-records-scratch, held this tree plus one temporaryci.ymlcommit. That commit kept only theplanand Atlas jobs, and its join ranverify-examples --writeand uploaded the records. I ran it by hand as run 39086315289, committed its 347 records here, and deleted the branch. The records of unchanged modules are byte-identical; only the audit and probe file names differ, because they carry the semantic ID.Measured on that run (one run each, wall times depend on the runner)
cert4jobcert4-replayjobNo
Census*process swaps any more.ClosureandClosureOrbitstill do (13.5–14.8 GiB). The longest path is nowprefix(26 min) →census-c(18.6 min, mostly the 970 s replay ofCensus) →closure→pairs-*→join. Two possible follow-ups, not in this PR.atlas-closurewaits for the wholeatlas-l1matrix, includingcensus-c, although its plan needs onlycert4,census-aandcensus-b. AndCensusCert11peaks at 11.6 GiB, the next window close to the memory line.Checks run locally, none of which need Lean: fmt, clippy
-D warnings,check-golden,validate-model(Atlas audits: 86 modules, 5,557 declarations),validate-spec-links,check-test-inventory,ci-shards, and AU-09, AU-10, RP-07, RP-11, RP-13, RP-14 and VR-19. VR-23 and the full gate run on this PR's ready run.The PR stays a draft until its head is final and contains
main.🤖 Generated with Claude Code