v4.33.0.1

• Refactor adoption into read-only action planning, component accounting, and report
  rendering. Share donor/source selection with execution and retain execution-time
  validation. Separate logical replacement, retained source/package/artifact content,
  and payload transfer. Deduplicate source objects by source identity; never add
  publication samples to measured totals. Remove the misleading aggregate published
  artifact-size headline. Report signed logical change when complete; physical disk
  recovery and peak allocation remain unknown. Add typed uncertainty and versioned
  additive JSON estimates; deprecate aggregate sample and physical-recovery scalars.

• Measure inventory completeness and local post-operation observations. Reuse one
  missing-frame validator for sparse OCI planning/pulling, deduplicate exact ranges,
  and expose remaining payload separately from config metadata read during planning.

• Correct attach/detach transaction cleanup: failed backup deletion after commit
  reports cleanup failure without attempting rollback from a partially removed backup.

• Add OCI metadata-backed artifact size references to adoption planning, with
  explicitly approximate same-repository revision fallbacks. Keep these separate
  from exact reuse/storage decisions. Summarize unknown costs and substituted
  versions in normal output; expose per-project provenance with --verbose and
  JSON. Metadata lookup never installs compilers or downloads artifact packs.

• Parallelize adoption project inspection and hashing of unique local dependency
  directories. Automatically size the planning pool from available CPUs and RAM,
  capped at eight workers; add adopt --jobs for explicit control. Deduplicate
  source hashes and repeated size inventories within each plan, preserve result
  order and worker progress, and retain fresh execution-time validation. Package
  preparation and attachment remain serialized.

• Make shared package and artifact identities cover the full normalized effective
  root graph, including dependencies introduced by overrides. This fixes an
  unsound reuse key; it does not demonstrate an incorrect Lean verdict. Bump
  shared-project identity to v4 and artifact compatibility to v3; older records
  cannot authorize artifact reuse. Unrelated graph changes now conservatively
  invalidate reuse too.

• During first adoption, retain compatible build outputs from the original local
  dependency checkout only when its recorded compiler and graph provenance match.
  Exclude linked state and path-sensitive traces; report rejected donors and the
  need to rebuild when provenance is unavailable. Source import remains separate
  from artifact migration, including for subdirectory packages.

• Revalidate every project during batch adoption instead of skipping projects
  merely because an attachment marker exists. Broken or stale links are repaired
  through normal adoption; modified local checkouts remain protected. Planning,
  adoption, and verify PROJECT share attachment validation. Project verification
  is local-only and reports subject_kind: project with null lock/environment IDs;
  it verifies attachment state, not a Lean proof verdict.

• Plan reuse with locally hashed Lean/Lake identities without installing tools.
  Report incomplete storage estimates, unknown download amounts, and unknown
  recovery instead of treating missing dependencies as zero-cost acquisitions.
  Storage figures describe materialized content, not physical disk allocation.

• Exercise Windows unit tests, macOS real-Lean integration, and clean anonymous
  Mathlib consumption of the PR checkout in CI. Add active HTTP cancellation
  and descendant-termination regressions; cancellation now checks between
  available HTTP chunks, and POSIX shutdown kills surviving descendants even
  when the direct child exits first.

• Make store lifecycle guarantees consistent across every execution path.
  Every cross-process lock now comes from one registry under <home>/.locks
  (LockPaths), so shared-project package locks and store cleanup finally
  contend; every published tree goes through one staged-publish transaction
  whose staging directory is owned by a lock while it is built, so doctor --repair only removes staging trees nobody is building; scratch cleanup
  holds the workspace lease across its rename; capsule and slim-toolchain
  replacement swaps the old tree out only once the new one is complete and
  restores it if the swap fails; a failed adopt restores the previous
  attachment record and config instead of deleting them; sparse projections
  validate the existing environment before writing into it.

• Carry cancellation and bounds end to end. All child processes (Lean, Lake,
  Git, elan, helpers) run through one internal seam with a shared timeout,
  cancel event, bounded output and observer buffering, process-tree shutdown
  and reader deadlines, and resource limits are applied without importing in
  the forked child. Sparse acquisition, capsule pulls and source fetches
  accept the cancel event; async wrappers preserve the caller's cancellation
  when a worker fails during cleanup; a failing matrix context always stops
  its running siblings.

• Validate at the boundary and keep identities stable. One portable
  relative-path policy (rejecting absolute, drive, UNC, backslash, NUL and
  .. forms) backs manifests, locks, capsules, archives and program
  inventories; locks validate packagesDir and package subdirectories at
  construction and freeze their manifest so lock_id cannot drift; provenance
  and program inventories are frozen the same way; specifications, generated
  root modules and locks all use one canonical package order; verify
  reports the path check it actually performs.

• Refresh storage status honestly: aliases, usage timestamps and object
  counts are re-read on every call while the expensive size accounting stays
  cached, and shared package builds invalidate that cache explicitly. The
  header-snapshot cache keys by the compiler binary's identity, not its
  spelling.

• Consolidate result construction: one conversion from process outcome to
  ExecutionResult, exclusive timing phases (a dependency build before a
  retried check now reports preliminary_check and build separately), a
  failed support module keeps every earlier support transcript, profile
  keeps the failing warmup, and a process killed by a signal reports the new
  crashed verdict rather than rejected.

• Progress observers are strictly observational: a failing callback is
  recorded on the emitter and never fails or rolls back an operation; the
  console renderer always shuts down; repeated counted operations with the
  same label print their checkpoints again; lean-run error messages name
  the flags the parser actually accepts.

• Extract shared primitives into internal modules (_archive, _platform,
  _sources, _project_identity, _git, _process, _transaction,
  _relpath, _results, _cancellation) so high-level modules no longer
  serve as each other's utility libraries.

• Shorten source-build environment staging names so deeply nested Mathlib
  artifacts remain below legacy MAX_PATH while leantar hydrates the cache
  on Windows. The previous PID plus full-UUID name put some artifacts at
  exactly 260 characters, where hydration failed with os error 3 and forced
  users toward a full Mathlib source build.

• Hydrate Mathlib's upstream build cache when new has no exact shared project
  or downloadable environment to seed from. The cold-start fallback previously
  opened the catalog environment without enabling the trusted URL-keyed
  accelerator, so it skipped lake exe cache get and compiled all of Mathlib
  from source.