Repository navigation
chore(dev): provision ten isolated build lanes on Extra #1795
Description
Bounded infrastructure subtask under #1197, explicitly requested by the user: provision ten independently buildable worktrees on /media/samuel/Extra for automation, probability, space, logic, classes_queue, crypto, circuits, PCP, learning and algorithms. This does not claim ownership of the broader study or activate an experiment.
Worker /root/mathlib_cache_retry_1730, coordinated by /root, will create an independent normal clone/object database with --no-hardlinks from the coordinator's private database, then snapshot the frozen clean warm checkout once. No primary-checkout edits or copies of its live outputs are allowed. Seed separate mutable build/dependency directories with the existing worktree helper and --copy-packages, at most two copies at once, skipping bootstrap during copying. Prioritize probability #1741 and automation #1734.
Acceptance: each lane has a recorded path and READY marker only after Git-control, symlink and mutable-output isolation checks; no pointer to the protected primary checkout; lane environments use Extra immutable caches and initially LEAN_NUM_THREADS=2; agents run cache ensure before their first Lean operation. Record snapshot release and the final path map. No repository-wide source changes or claim that this fixes API-memory failures.
AI assistance: OpenAI Codex performs the provisioning and checks under the user's explicit capacity request.
Activity
SamuelSchlesinger commentedon Oct 30, 2026
active — Worker
/root/mathlib_cache_retry_1730owns this provisioning-only subtask under/root, sessionextra-lanes-20261030. The independent seed clone will be.../complexitylib-codex-20261030-65g7glwh/template; ten lane branches/worktrees will be distinct. No source patch is planned. Root's warm checkout is frozen until the closed-output snapshot and its dependency Git controls are independent; copying will then proceed at most two lanes at a time.SamuelSchlesinger commentedon Oct 30, 2026
Provisioning complete — worker
/root/mathlib_cache_retry_1730delivered all ten READY lanes and notified their owners. The independent normal clone uses its own object database, official origin and no source-database hardlinks/alternates. Root's frozen warm snapshot was copied once and released after dependency-control isolation; copies then stayed at two lanes at a time, with bootstrap disabled.Each lane passed checks on 213,866 copied files (2,138,660 total), with no external mutable hardlinks, isolated dependency HEAD/index/refs/config controls, manifest-matching package HEADs and only the internal batteries README symlink. Shared immutable caches were copied once; no primary-checkout outputs or writes, Lean/source builds, experiment activation or repository-variable changes occurred. There are no Lean declaration, curated abstract or rendering changes.
The team root is
/media/samuel/Extra/complexitylib-codex-20261030-65g7glwh. Every lane istemplate/.worktrees/<lane>: automation, probability, space, logic, classes_queue, crypto, circuits, pcp, learning and algorithms.lane-paths.json,ALL_LANES_READY.jsonandreadiness/<lane>.jsoncontain the path/owner map and audit records. Probability starts at the exact frozen83be1894; other initial sources are freshly fetched7e32b1502, with private closed outputs seeded from1182e928.Owners source
env.shin each Lake/Lean shell and runscripts/cache/ensure.shbefore their first Lean operation/after switching. Lake and Mathlib cache data go to Extra;LEAN_NUM_THREADS=2is pool sizing, with heavy full builds coordinated separately. Extra has 1.6 TB free after provisioning (196 GB used). Handoff to coordinator/rootfor final disposition; the broader #1197 study remains open and inactive.SamuelSchlesinger commentedon Oct 30, 2026
Coordinator
/rootaccepts this bounded provisioning task as completed after checking the final ten-lane map and READY audit records against the issue criteria. All ten owners have their assigned checkouts; multiple lanes have now completed focused and full validation there. The worker closeout records the isolation checks and cache environment. This closes only the requested local capacity work; #1197 remains open and inactive.SamuelSchlesinger commentedon Oct 30, 2026
Follow-up: #1803 found that the local donor was a partial/promisor clone, leaving older history incomplete despite complete current source trees. The original ten lanes, refs, metadata and outputs are preserved; owners are cutting over to audited worktrees from a fresh full network clone. #1803 owns the diagnosis and migration evidence. No shared object repair, deletion or repack is being used.